refactor(Probability): change stopping times to take values in WithTop (#29430)

This PR changes stopping times to have type `Ω → WithTop ι` instead of `Ω → ι`.
Previously, a stopping time for a filtration indexed by Nat had to have value in Nat. That's not representative of the way stopping times are used in probability. A typical stopping time is the first time at which we see a head in an infinite sequence of coin flips. That time could be infinite (although it is almost surely finite). We can't represent it with a `Ω → Nat` stopping time: if we choose an arbitrary value in Nat for the event that it is infinite, we destroy the stopping time property.
We faced that issue in the `BorelCantelli` file, in which we avoided such a possibly infinite stopping time by introducing a sequence of bounded stopping times. We had to prove additional lemmas about them since we could not directly use the API for stopped processes. With the new type, that file is greatly simplified as the API is directly usable, and we can write the proof as we would on paper.

The issue with the previous stopping time implementation was noted in [Ying and Degenne, A Formalization of Doob’s Martingale Convergence Theorems in mathlib, CPP 2023, https://dl.acm.org/doi/pdf/10.1145/3573105.3575675].

Other changes:
- the sigma-algebra generated by a stopping time is now a sub-sigma algebra by definition
-  `measurableSet_eq_stopping_time` is generalized and the now useless `measurableSet_eq_stopping_time_of_countable` is removed
- `hitting` is renamed to `hittingBtwn`
- a new `hittingAfter` is introduced and used in the Borel-Cantelli proof. That proof is now much simpler since we can use a stopped process as intended instead of going around the limitations of the previous stopping time implementation.

Co-authored-by: Remy Degenne <remydegenne@gmail.com>

Author: RemyDegenne

Mathlib/Order/WithBot.lean

@@ -868,8 +868,31 @@ protected theorem _root_.IsMin.withTop (h : IsMin a) : IsMin (a : WithTop α) :=
 
 lemma untop_le_iff (hx : x ≠ ⊤) : untop x hx ≤ b ↔ x ≤ b := by lift x to α using id hx; simp
 lemma le_untop_iff (hy : y ≠ ⊤) : a ≤ untop y hy ↔ a ≤ y := by lift y to α using id hy; simp
+
+lemma untopD_le_iff (hy : y ≠ ⊤) : y.untopD a ≤ b ↔ y ≤ b := by lift y to α using id hy; simp
 lemma le_untopD_iff (hy : y = ⊤ → a ≤ b) : a ≤ y.untopD b ↔ a ≤ y := by cases y <;> simp [hy]
 
+lemma untopA_le_iff [Nonempty α] (hy : y ≠ ⊤) : y.untopA ≤ b ↔ y ≤ b := untopD_le_iff hy
+lemma le_untopA_iff [Nonempty α] (hy : y ≠ ⊤) : a ≤ y.untopA ↔ a ≤ y := by
+  lift y to α using id hy; simp
+
+lemma untop_mono (hx : x ≠ ⊤) (hy : y ≠ ⊤) (h : x ≤ y) :
+    x.untop hx ≤ y.untop hy := by
+  lift x to α using id hx
+  lift y to α using id hy
+  simp only [untop_coe]
+  exact mod_cast h
+
+lemma untopD_mono (hy : y ≠ ⊤) (h : x ≤ y) :
+    x.untopD a ≤ y.untopD a := by
+  lift y to α using hy
+  cases x with
+  | top => simp at h
+  | coe a => simp only [WithTop.untopD_coe]; exact mod_cast h
+
+lemma untopA_mono [Nonempty α] (hy : y ≠ ⊤) (h : x ≤ y) :
+    x.untopA ≤ y.untopA := untopD_mono hy h
+
 end LE
 
 section LT
@@ -902,7 +925,14 @@ protected lemma lt_top_iff_ne_top : x < ⊤ ↔ x ≠ ⊤ := by cases x <;> simp
 
 @[simp] lemma lt_untop_iff (hy : y ≠ ⊤) : a < y.untop hy ↔ a < y := by lift y to α using id hy; simp
 @[simp] lemma untop_lt_iff (hx : x ≠ ⊤) : x.untop hx < b ↔ x < b := by lift x to α using id hx; simp
+
 lemma lt_untopD_iff (hy : y = ⊤ → a < b) : a < y.untopD b ↔ a < y := by cases y <;> simp [hy]
+lemma untopD_lt_iff (hx : x ≠ ⊤) : x.untopD a < b ↔ x < b := by
+  lift x to α using id hx; simp
+
+lemma lt_untopA_iff [Nonempty α] (hy : y ≠ ⊤) : a < y.untopA ↔ a < y := by
+  lift y to α using id hy; simp
+lemma untopA_lt_iff [Nonempty α] (hx : x ≠ ⊤) : x.untopA < b ↔ x < b := untopD_lt_iff hx
 
 end LT
 
@@ -975,7 +1005,15 @@ lemma forall_coe_le_iff_le [NoTopOrder α] : (∀ a : α, a ≤ x → a ≤ y) 
 end Preorder
 
 section PartialOrder
-variable [PartialOrder α] [NoTopOrder α] {x y : WithTop α}
+variable [PartialOrder α] {x y : WithTop α}
+
+lemma untopD_le (hy : y ≤ b) : y.untopD a ≤ b := by
+  rwa [untopD_le_iff]
+  exact ne_top_of_le_ne_top (by simp) hy
+
+lemma untopA_le [Nonempty α] (hy : y ≤ b) : y.untopA ≤ b := untopD_le hy
+
+variable [NoTopOrder α]
 
 lemma eq_of_forall_coe_le_iff (h : ∀ a : α, a ≤ x ↔ a ≤ y) : x = y :=
   WithBot.eq_of_forall_le_coe_iff (α := αᵒᵈ) h

Mathlib/Probability/Martingale/Basic.lean

@@ -446,7 +446,7 @@ theorem Martingale.eq_zero_of_predictable [SigmaFiniteFiltration μ 𝒢] {f : 
 namespace Submartingale
 
 protected theorem integrable_stoppedValue [LE E] {f : ℕ → Ω → E} (hf : Submartingale f 𝒢 μ)
-    {τ : Ω → ℕ} (hτ : IsStoppingTime 𝒢 τ) {N : ℕ} (hbdd : ∀ ω, τ ω ≤ N) :
+    {τ : Ω → ℕ∞} (hτ : IsStoppingTime 𝒢 τ) {N : ℕ} (hbdd : ∀ ω, τ ω ≤ N) :
     Integrable (stoppedValue f τ) μ :=
   integrable_stoppedValue ℕ hτ hf.integrable hbdd
 

Mathlib/Probability/Martingale/BorelCantelli.lean

@@ -45,122 +45,93 @@ variable {Ω : Type*} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {ℱ : Filtrat
 ### One sided martingale bound
 -/
 
+/-- `leastGE f r` is the stopping time corresponding to the first time `f ≥ r`. -/
+noncomputable def leastGE (f : ℕ → Ω → ℝ) (r : ℝ) : Ω → ℕ∞ :=
+  hittingAfter f (Set.Ici r) 0
 
--- TODO: `leastGE` should be defined taking values in `WithTop ℕ` once the `stoppedProcess`
--- refactor is complete
-/-- `leastGE f r n` is the stopping time corresponding to the first time `f ≥ r`. -/
-noncomputable def leastGE (f : ℕ → Ω → ℝ) (r : ℝ) (n : ℕ) :=
-  hitting f (Set.Ici r) 0 n
-
-theorem Adapted.isStoppingTime_leastGE (r : ℝ) (n : ℕ) (hf : Adapted ℱ f) :
-    IsStoppingTime ℱ (leastGE f r n) :=
-  hitting_isStoppingTime hf measurableSet_Ici
-
-theorem leastGE_le {i : ℕ} {r : ℝ} (ω : Ω) : leastGE f r i ω ≤ i :=
-  hitting_le ω
-
--- The following four lemmas shows `leastGE` behaves like a stopped process. Ideally we should
--- define `leastGE` as a stopping time and take its stopped process. However, we can't do that
--- with our current definition since a stopping time takes only finite indices. An upcoming
--- refactor should hopefully make it possible to have stopping times taking infinity as a value
-theorem leastGE_mono {n m : ℕ} (hnm : n ≤ m) (r : ℝ) (ω : Ω) : leastGE f r n ω ≤ leastGE f r m ω :=
-  hitting_mono hnm
-
-theorem leastGE_eq_min (π : Ω → ℕ) (r : ℝ) (ω : Ω) {n : ℕ} (hπn : ∀ ω, π ω ≤ n) :
-    leastGE f r (π ω) ω = min (π ω) (leastGE f r n ω) := by
-  classical
-  refine le_antisymm (le_min (leastGE_le _) (leastGE_mono (hπn ω) r ω)) ?_
-  by_cases hle : π ω ≤ leastGE f r n ω
-  · rw [min_eq_left hle, leastGE]
-    by_cases h : ∃ j ∈ Set.Icc 0 (π ω), f j ω ∈ Set.Ici r
-    · refine hle.trans (Eq.le ?_)
-      rw [leastGE, ← hitting_eq_hitting_of_exists (hπn ω) h]
-    · simp only [hitting, if_neg h, le_rfl]
-  · rw [min_eq_right (not_le.1 hle).le, leastGE, leastGE, ←
-      hitting_eq_hitting_of_exists (hπn ω) _]
-    rw [not_le, leastGE, hitting_lt_iff _ (hπn ω)] at hle
-    exact
-      let ⟨j, hj₁, hj₂⟩ := hle
-      ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩
-
-theorem stoppedValue_stoppedValue_leastGE (f : ℕ → Ω → ℝ) (π : Ω → ℕ) (r : ℝ) {n : ℕ}
-    (hπn : ∀ ω, π ω ≤ n) : stoppedValue (fun i => stoppedValue f (leastGE f r i)) π =
-      stoppedValue (stoppedProcess f (leastGE f r n)) π := by
-  ext1 ω
-  simp +unfoldPartialApp only [stoppedProcess, stoppedValue]
-  rw [leastGE_eq_min _ _ _ hπn]
-
-theorem Submartingale.stoppedValue_leastGE [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ) (r : ℝ) :
-    Submartingale (fun i => stoppedValue f (leastGE f r i)) ℱ μ := by
-  rw [submartingale_iff_expected_stoppedValue_mono]
-  · intro σ π hσ hπ hσ_le_π hπ_bdd
-    obtain ⟨n, hπ_le_n⟩ := hπ_bdd
-    simp_rw [stoppedValue_stoppedValue_leastGE f σ r fun i => (hσ_le_π i).trans (hπ_le_n i)]
-    simp_rw [stoppedValue_stoppedValue_leastGE f π r hπ_le_n]
-    refine hf.expected_stoppedValue_mono ?_ ?_ ?_ fun ω => (min_le_left _ _).trans (hπ_le_n ω)
-    · exact hσ.min (hf.adapted.isStoppingTime_leastGE _ _)
-    · exact hπ.min (hf.adapted.isStoppingTime_leastGE _ _)
-    · exact fun ω => min_le_min (hσ_le_π ω) le_rfl
-  · exact fun i => stronglyMeasurable_stoppedValue_of_le hf.adapted.progMeasurable_of_discrete
-      (hf.adapted.isStoppingTime_leastGE _ _) leastGE_le
-  · exact fun i => integrable_stoppedValue _ (hf.adapted.isStoppingTime_leastGE _ _) hf.integrable
-      leastGE_le
+theorem Adapted.isStoppingTime_leastGE (r : ℝ) (hf : Adapted ℱ f) :
+    IsStoppingTime ℱ (leastGE f r) :=
+  hittingAfter_isStoppingTime hf measurableSet_Ici
+
+/-- The stopped process of `f` above `r` is the process that is equal to `f` until `leastGE f r`
+(the first time `f` passes above `r`), and then is constant afterwards. -/
+noncomputable def stoppedAbove (f : ℕ → Ω → ℝ) (r : ℝ) : ℕ → Ω → ℝ :=
+  stoppedProcess f (leastGE f r)
+
+protected lemma Submartingale.stoppedAbove [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ) (r : ℝ) :
+    Submartingale (stoppedAbove f r) ℱ μ :=
+  hf.stoppedProcess (hf.adapted.isStoppingTime_leastGE r)
+
+@[deprecated (since := "2025-10-25")] alias Submartingale.stoppedValue_leastGE :=
+  Submartingale.stoppedAbove
 
 variable {r : ℝ} {R : ℝ≥0}
 
-theorem norm_stoppedValue_leastGE_le (hr : 0 ≤ r) (hf0 : f 0 = 0)
+theorem stoppedAbove_le (hr : 0 ≤ r) (hf0 : f 0 = 0)
     (hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) (i : ℕ) :
-    ∀ᵐ ω ∂μ, stoppedValue f (leastGE f r i) ω ≤ r + R := by
+    ∀ᵐ ω ∂μ, stoppedAbove f r i ω ≤ r + R := by
   filter_upwards [hbdd] with ω hbddω
-  change f (leastGE f r i ω) ω ≤ r + R
-  by_cases heq : leastGE f r i ω = 0
-  · rw [heq, hf0, Pi.zero_apply]
-    exact add_nonneg hr R.coe_nonneg
-  · obtain ⟨k, hk⟩ := Nat.exists_eq_succ_of_ne_zero heq
-    rw [hk, add_comm, ← sub_le_iff_le_add]
-    have := notMem_of_lt_hitting (hk.symm ▸ k.lt_succ_self : k < leastGE f r i ω) (zero_le _)
-    simp only [Set.mem_Ici, not_le] at this
+  rw [stoppedAbove, stoppedProcess, ENat.some_eq_coe]
+  by_cases h_zero : (min (i : ℕ∞) (leastGE f r ω)).untopA = 0
+  · simp only [h_zero, hf0, Pi.zero_apply]
+    positivity
+  obtain ⟨k, hk⟩ := Nat.exists_eq_add_one_of_ne_zero h_zero
+  rw [hk, add_comm r, ← sub_le_iff_le_add]
+  have := notMem_of_lt_hittingAfter (?_ : k < leastGE f r ω)
+  · simp only [zero_le, Set.mem_Ici, not_le, forall_const] at this
     exact (sub_lt_sub_left this _).le.trans ((le_abs_self _).trans (hbddω _))
+  · suffices (k : ℕ∞) < min (i : ℕ∞) (leastGE f r ω) from this.trans_le (min_le_right _ _)
+    have h_top : min (i : ℕ∞) (leastGE f r ω) ≠ ⊤ :=
+      ne_top_of_le_ne_top (by simp) (min_le_left _ _)
+    lift min (i : ℕ∞) (leastGE f r ω) to ℕ using h_top with p
+    simp only [untopD_coe_enat, Nat.cast_lt, gt_iff_lt] at *
+    omega
 
-theorem Submartingale.stoppedValue_leastGE_eLpNorm_le [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ)
+@[deprecated (since := "2025-10-25")] alias norm_stoppedValue_leastGE_le := stoppedAbove_le
+
+theorem Submartingale.eLpNorm_stoppedAbove_le [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ)
     (hr : 0 ≤ r) (hf0 : f 0 = 0) (hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) (i : ℕ) :
-    eLpNorm (stoppedValue f (leastGE f r i)) 1 μ ≤ 2 * μ Set.univ * ENNReal.ofReal (r + R) := by
-  refine eLpNorm_one_le_of_le' ((hf.stoppedValue_leastGE r).integrable _) ?_
-    (norm_stoppedValue_leastGE_le hr hf0 hbdd i)
+    eLpNorm (stoppedAbove f r i) 1 μ ≤ 2 * μ Set.univ * ENNReal.ofReal (r + R) := by
+  refine eLpNorm_one_le_of_le' ((hf.stoppedAbove r).integrable _) ?_
+    (stoppedAbove_le hr hf0 hbdd i)
   rw [← setIntegral_univ]
-  refine le_trans ?_ ((hf.stoppedValue_leastGE r).setIntegral_le (zero_le _) MeasurableSet.univ)
-  simp_rw [stoppedValue, leastGE, hitting_of_le le_rfl, hf0, integral_zero', le_rfl]
+  refine le_trans ?_ ((hf.stoppedAbove r).setIntegral_le (zero_le _) MeasurableSet.univ)
+  simp [stoppedAbove, stoppedProcess, hf0]
+
+@[deprecated (since := "2025-10-25")] alias Submartingale.stoppedValue_leastGE_eLpNorm_le :=
+  Submartingale.eLpNorm_stoppedAbove_le
 
-theorem Submartingale.stoppedValue_leastGE_eLpNorm_le' [IsFiniteMeasure μ]
+theorem Submartingale.eLpNorm_stoppedAbove_le' [IsFiniteMeasure μ]
     (hf : Submartingale f ℱ μ) (hr : 0 ≤ r) (hf0 : f 0 = 0)
     (hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) (i : ℕ) :
-    eLpNorm (stoppedValue f (leastGE f r i)) 1 μ ≤
-      ENNReal.toNNReal (2 * μ Set.univ * ENNReal.ofReal (r + R)) := by
-  refine (hf.stoppedValue_leastGE_eLpNorm_le hr hf0 hbdd i).trans ?_
+    eLpNorm (stoppedAbove f r i) 1 μ
+      ≤ ENNReal.toNNReal (2 * μ Set.univ * ENNReal.ofReal (r + R)) := by
+  refine (hf.eLpNorm_stoppedAbove_le hr hf0 hbdd i).trans ?_
   simp [ENNReal.coe_toNNReal (measure_ne_top μ _), ENNReal.coe_toNNReal]
 
+@[deprecated (since := "2025-10-25")] alias Submartingale.stoppedValue_leastGE_eLpNorm_le' :=
+  Submartingale.eLpNorm_stoppedAbove_le'
+
 /-- This lemma is superseded by `Submartingale.bddAbove_iff_exists_tendsto`. -/
 theorem Submartingale.exists_tendsto_of_abs_bddAbove_aux [IsFiniteMeasure μ]
     (hf : Submartingale f ℱ μ) (hf0 : f 0 = 0) (hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) :
     ∀ᵐ ω ∂μ, BddAbove (Set.range fun n => f n ω) → ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) := by
-  have ht :
-    ∀ᵐ ω ∂μ, ∀ i : ℕ, ∃ c, Tendsto (fun n => stoppedValue f (leastGE f i n) ω) atTop (𝓝 c) := by
+  have ht : ∀ᵐ ω ∂μ, ∀ i : ℕ, ∃ c, Tendsto (fun n => stoppedAbove f i n ω) atTop (𝓝 c) := by
     rw [ae_all_iff]
-    exact fun i => Submartingale.exists_ae_tendsto_of_bdd (hf.stoppedValue_leastGE i)
-      (hf.stoppedValue_leastGE_eLpNorm_le' i.cast_nonneg hf0 hbdd)
+    exact fun i ↦ Submartingale.exists_ae_tendsto_of_bdd (hf.stoppedAbove i)
+      (hf.eLpNorm_stoppedAbove_le' i.cast_nonneg hf0 hbdd)
   filter_upwards [ht] with ω hω hωb
   rw [BddAbove] at hωb
   obtain ⟨i, hi⟩ := exists_nat_gt hωb.some
   have hib : ∀ n, f n ω < i := by
     intro n
     exact lt_of_le_of_lt ((mem_upperBounds.1 hωb.some_mem) _ ⟨n, rfl⟩) hi
-  have heq : ∀ n, stoppedValue f (leastGE f i n) ω = f n ω := by
+  have heq : ∀ n, stoppedAbove f i n ω = f n ω := by
     intro n
-    rw [leastGE]; unfold hitting; rw [stoppedValue]
-    rw [if_neg]
-    simp only [Set.mem_Icc, Set.mem_Ici]
-    push_neg
-    exact fun j _ => hib j
+    rw [stoppedAbove, stoppedProcess, leastGE, hittingAfter_eq_top_iff.mpr]
+    · simp only [le_top, inf_of_le_left]
+      congr
+    · simp [hib]
   simp only [← heq, hω i]
 
 theorem Submartingale.bddAbove_iff_exists_tendsto_aux [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ)

Mathlib/Probability/Martingale/OptionalSampling.lean

@@ -43,11 +43,10 @@ variable {Ω E : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCom
 section FirstCountableTopology
 
 variable {ι : Type*} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι]
-  [FirstCountableTopology ι] {ℱ : Filtration ι m} [SigmaFiniteFiltration μ ℱ] {τ σ : Ω → ι}
+  [FirstCountableTopology ι] {ℱ : Filtration ι m} [SigmaFiniteFiltration μ ℱ] {τ σ : Ω → WithTop ι}
   {f : ι → Ω → E} {i n : ι}
 
-theorem condExp_stopping_time_ae_eq_restrict_eq_const
-    [(Filter.atTop : Filter ι).IsCountablyGenerated] (h : Martingale f ℱ μ)
+theorem condExp_stopping_time_ae_eq_restrict_eq_const (h : Martingale f ℱ μ)
     (hτ : IsStoppingTime ℱ τ) [SigmaFinite (μ.trim hτ.measurableSpace_le)] (hin : i ≤ n) :
     μ[f n|hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = i}] f i := by
   refine Filter.EventuallyEq.trans ?_ (ae_restrict_of_ae (h.condExp_ae_eq hin))
@@ -67,8 +66,10 @@ theorem condExp_stopping_time_ae_eq_restrict_eq_const_of_le_const (h : Martingal
   · suffices {x : Ω | τ x = i} = ∅ by simp [this]; norm_cast
     ext1 x
     simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false]
-    rintro rfl
-    exact hin (hτ_le x)
+    contrapose! hin
+    exact_mod_cast hin ▸ hτ_le x
+
+variable [Nonempty ι]
 
 theorem stoppedValue_ae_eq_restrict_eq (h : Martingale f ℱ μ) (hτ : IsStoppingTime ℱ τ)
     (hτ_le : ∀ x, τ x ≤ n) [SigmaFinite (μ.trim (hτ.measurableSpace_le_of_le hτ_le))] (i : ι) :
@@ -78,7 +79,7 @@ theorem stoppedValue_ae_eq_restrict_eq (h : Martingale f ℱ μ) (hτ : IsStoppi
   rw [Filter.EventuallyEq, ae_restrict_iff' (ℱ.le _ _ (hτ.measurableSet_eq i))]
   refine Filter.Eventually.of_forall fun x hx => ?_
   rw [Set.mem_setOf_eq] at hx
-  simp_rw [stoppedValue, hx]
+  simp [stoppedValue, hx]
 
 /-- The value of a martingale `f` at a stopping time `τ` bounded by `n` is the conditional
 expectation of `f n` with respect to the σ-algebra generated by `τ`. -/
@@ -92,7 +93,14 @@ theorem stoppedValue_ae_eq_condExp_of_le_const_of_countable_range (h : Martingal
       Set.mem_iUnion, Set.mem_setOf_eq, exists_apply_eq_apply']
   nth_rw 1 [← @Measure.restrict_univ Ω _ μ]
   rw [this, ae_eq_restrict_biUnion_iff _ h_countable_range]
-  exact fun i _ => stoppedValue_ae_eq_restrict_eq h _ hτ_le i
+  intro i hi
+  have h_top : i ≠ ⊤ := fun h ↦ by
+    simp only [h, Set.mem_range] at hi
+    obtain ⟨ω , hω⟩ := hi
+    specialize hτ_le ω
+    simp [hω] at hτ_le
+  lift i to ι using h_top with i
+  exact stoppedValue_ae_eq_restrict_eq h _ hτ_le i
 
 /-- The value of a martingale `f` at a stopping time `τ` bounded by `n` is the conditional
 expectation of `f n` with respect to the σ-algebra generated by `τ`. -/
@@ -143,7 +151,7 @@ and is a measurable space with the Borel σ-algebra. -/
 
 variable {ι : Type*} [LinearOrder ι] [LocallyFiniteOrder ι] [OrderBot ι] [TopologicalSpace ι]
   [DiscreteTopology ι] [MeasurableSpace ι] [BorelSpace ι] [MeasurableSpace E] [BorelSpace E]
-  [SecondCountableTopology E] {ℱ : Filtration ι m} {τ σ : Ω → ι} {f : ι → Ω → E} {i : ι}
+  [SecondCountableTopology E] {ℱ : Filtration ι m} {τ σ : Ω → WithTop ι} {f : ι → Ω → E} {i : ι}
 
 theorem condExp_stoppedValue_stopping_time_ae_eq_restrict_le (h : Martingale f ℱ μ)
     (hτ : IsStoppingTime ℱ τ) (hσ : IsStoppingTime ℱ σ) [SigmaFinite (μ.trim hσ.measurableSpace_le)]