From 3f1d674220f7114ea4f8501c3258371ec454be7c Mon Sep 17 00:00:00 2001
From: Joris van Winden <j.vanwinden@student.tudelft.nl>
Date: Sun, 19 Apr 2026 15:13:49 +0200
Subject: [PATCH 01/17] rename IsPredictable to IsStronglyPredictable

---
 Mathlib/Probability/Martingale/Basic.lean    |  6 +++---
 Mathlib/Probability/Process/Predictable.lean | 20 ++++++++++----------
 2 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/Mathlib/Probability/Martingale/Basic.lean b/Mathlib/Probability/Martingale/Basic.lean
index 4bbcc232e26c77..277947191a2ef0 100644
--- a/Mathlib/Probability/Martingale/Basic.lean
+++ b/Mathlib/Probability/Martingale/Basic.lean
@@ -520,7 +520,7 @@ In contrast to the non-primed version, this result requires second countability
 `StronglyAdapted` is defined using strong measurability while `IsPredictable` only provides
 measurable. -/
 theorem Submartingale.zero_le_of_predictable' [Preorder E] [SigmaFiniteFiltration μ 𝒢]
-    {f : ℕ → Ω → E} (hfmgle : Submartingale f 𝒢 μ) (hf : IsPredictable 𝒢 f) (n : ℕ) :
+    {f : ℕ → Ω → E} (hfmgle : Submartingale f 𝒢 μ) (hf : IsStronglyPredictable 𝒢 f) (n : ℕ) :
     f 0 ≤ᵐ[μ] f n :=
   zero_le_of_predictable hfmgle (fun _ ↦ (hf.measurable_add_one _).stronglyMeasurable) n
 
@@ -529,7 +529,7 @@ theorem Submartingale.zero_le_of_predictable' [Preorder E] [SigmaFiniteFiltratio
 In contrast to the non-primed version, this result requires second countability as `StronglyAdapted`
 is defined using strong measurability while `IsPredictable` only provides measurable. -/
 theorem Supermartingale.le_zero_of_predictable' [Preorder E] [SigmaFiniteFiltration μ 𝒢]
-    {f : ℕ → Ω → E} (hfmgle : Supermartingale f 𝒢 μ) (hfadp : IsPredictable 𝒢 f)
+    {f : ℕ → Ω → E} (hfmgle : Supermartingale f 𝒢 μ) (hfadp : IsStronglyPredictable 𝒢 f)
     (n : ℕ) : f n ≤ᵐ[μ] f 0 :=
   le_zero_of_predictable hfmgle (fun _ ↦ (hfadp.measurable_add_one _).stronglyMeasurable) n
 
@@ -538,7 +538,7 @@ theorem Supermartingale.le_zero_of_predictable' [Preorder E] [SigmaFiniteFiltrat
 In contrast to the non-primed version, this result requires second countability as `StronglyAdapted`
 is defined using strong measurability while `IsPredictable` only provides measurable. -/
 theorem Martingale.eq_zero_of_predictable' [SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E}
-    (hfmgle : Martingale f 𝒢 μ) (hfadp : IsPredictable 𝒢 f) (n : ℕ) : f n =ᵐ[μ] f 0 :=
+    (hfmgle : Martingale f 𝒢 μ) (hfadp : IsStronglyPredictable 𝒢 f) (n : ℕ) : f n =ᵐ[μ] f 0 :=
   eq_zero_of_predictable hfmgle (fun _ ↦ (hfadp.measurable_add_one _).stronglyMeasurable) n
 
 end IsPredictable
diff --git a/Mathlib/Probability/Process/Predictable.lean b/Mathlib/Probability/Process/Predictable.lean
index b6e8240c02f665..6c6fb90358577f 100644
--- a/Mathlib/Probability/Process/Predictable.lean
+++ b/Mathlib/Probability/Process/Predictable.lean
@@ -60,7 +60,7 @@ end Filtration
 
 /-- A process is said to be predictable if it is measurable with respect to the predictable
 σ-algebra. -/
-def IsPredictable (𝓕 : Filtration ι m) (u : ι → Ω → E) :=
+def IsStronglyPredictable (𝓕 : Filtration ι m) (u : ι → Ω → E) :=
   StronglyMeasurable[𝓕.predictable] <| Function.uncurry u
 
 end
@@ -97,7 +97,7 @@ lemma measurableSpace_le_predictable_of_measurableSet [Preorder ι] [OrderBot ι
   · exact hm'bot A hA
   · exact hm' i A hA
 
-namespace IsPredictable
+namespace IsStronglyPredictable
 
 open Filtration
 
@@ -106,10 +106,10 @@ variable [LinearOrder ι] [OrderBot ι] [MeasurableSpace ι] [TopologicalSpace 
     [MetrizableSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
 
 /-- A predictable process is progressively measurable. -/
-lemma progMeasurable {𝓕 : Filtration ι m} {u : ι → Ω → E} (h𝓕 : IsPredictable 𝓕 u) :
+lemma progMeasurable {𝓕 : Filtration ι m} {u : ι → Ω → E} (h𝓕 : IsStronglyPredictable 𝓕 u) :
     ProgMeasurable 𝓕 u := by
   refine fun i ↦ Measurable.stronglyMeasurable ?_
-  rw [IsPredictable, stronglyMeasurable_iff_measurable, measurable_iff_comap_le] at h𝓕
+  rw [IsStronglyPredictable, stronglyMeasurable_iff_measurable, measurable_iff_comap_le] at h𝓕
   rw [measurable_iff_comap_le, (by aesop : (fun (p : Set.Iic i × Ω) ↦ u (p.1) p.2)
       = Function.uncurry u ∘ (fun p ↦ (p.1, p.2))), ← MeasurableSpace.comap_comp]
   refine (MeasurableSpace.comap_mono h𝓕).trans <| MeasurableSpace.comap_le_iff_le_map.2 <|
@@ -127,7 +127,7 @@ lemma progMeasurable {𝓕 : Filtration ι m} {u : ι → Ω → E} (h𝓕 : IsP
     · simp [(by grind : (fun (p : Set.Iic i × Ω) ↦ ((p.1 : ι), p.2)) ⁻¹' Set.Ioi j ×ˢ A = ∅)]
 
 /-- A predictable process is adapted. -/
-lemma adapted {𝓕 : Filtration ι m} {u : ι → Ω → E} (h𝓕 : IsPredictable 𝓕 u) :
+lemma adapted {𝓕 : Filtration ι m} {u : ι → Ω → E} (h𝓕 : IsStronglyPredictable 𝓕 u) :
     StronglyAdapted 𝓕 u :=
   h𝓕.progMeasurable.stronglyAdapted
 
@@ -170,13 +170,13 @@ lemma measurableSet_prodMk_add_one_of_predictable {𝓕 : Filtration ℕ m} {s :
 
 omit [SecondCountableTopology E] in
 /-- If `u` is a discrete predictable process, then `u (n + 1)` is `𝓕 n`-measurable. -/
-lemma measurable_add_one {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E} (h𝓕 : IsPredictable 𝓕 u) (n : ℕ) :
-    Measurable[𝓕 n] (u (n + 1)) := by
+lemma measurable_add_one {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E} (h𝓕 : IsStronglyPredictable 𝓕 u)
+    (n : ℕ) : Measurable[𝓕 n] (u (n + 1)) := by
   intro s hs
   rw [(by aesop : u (n + 1) ⁻¹' s = {ω | (n + 1, ω) ∈ (Function.uncurry u) ⁻¹' s})]
   exact measurableSet_prodMk_add_one_of_predictable (h𝓕.measurable hs) n
 
-end IsPredictable
+end IsStronglyPredictable
 
 section
 
@@ -194,7 +194,7 @@ lemma measurableSet_predictable_singleton_prod
 lemma isPredictable_of_measurable_add_one [SecondCountableTopology E]
     {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E}
     (h₀ : Measurable[𝓕 0] (u 0)) (h : ∀ n, Measurable[𝓕 n] (u (n + 1))) :
-    IsPredictable 𝓕 u := by
+    IsStronglyPredictable 𝓕 u := by
   refine Measurable.stronglyMeasurable ?_
   intro s hs
   rw [(by aesop : Function.uncurry u ⁻¹' s = ⋃ n : ℕ, {n} ×ˢ (u n ⁻¹' s))]
@@ -208,7 +208,7 @@ lemma isPredictable_of_measurable_add_one [SecondCountableTopology E]
 `u 0` is `𝓕 0`-measurable. -/
 lemma isPredictable_iff_measurable_add_one [SecondCountableTopology E]
     {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E} :
-    IsPredictable 𝓕 u ↔ Measurable[𝓕 0] (u 0) ∧ ∀ n, Measurable[𝓕 n] (u (n + 1)) :=
+    IsStronglyPredictable 𝓕 u ↔ Measurable[𝓕 0] (u 0) ∧ ∀ n, Measurable[𝓕 n] (u (n + 1)) :=
   ⟨fun h𝓕 ↦ ⟨(h𝓕.adapted 0).measurable, fun n ↦ h𝓕.measurable_add_one (n)⟩,
     fun h ↦ isPredictable_of_measurable_add_one h.1 h.2⟩
 

From 044b696397b26ee95f401b5745acfa4fafc86b0d Mon Sep 17 00:00:00 2001
From: Joris van Winden <j.vanwinden@student.tudelft.nl>
Date: Sun, 19 Apr 2026 15:21:33 +0200
Subject: [PATCH 02/17] rename lemmas relating to IsStronglyPredictable

---
 Mathlib/Probability/Martingale/Basic.lean    |  4 ++--
 Mathlib/Probability/Process/Predictable.lean | 16 ++++++++--------
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/Mathlib/Probability/Martingale/Basic.lean b/Mathlib/Probability/Martingale/Basic.lean
index 277947191a2ef0..b8b0015f292aa1 100644
--- a/Mathlib/Probability/Martingale/Basic.lean
+++ b/Mathlib/Probability/Martingale/Basic.lean
@@ -509,7 +509,7 @@ theorem Martingale.eq_zero_of_predictable [SigmaFiniteFiltration μ 𝒢] {f : 
     exact ((Germ.coe_eq.mp (congr_arg Germ.ofFun <| condExp_of_stronglyMeasurable (𝒢.le _) (hfadp _)
       (hfmgle.integrable _))).symm.trans (hfmgle.2 k (k + 1) k.le_succ)).trans ih
 
-section IsPredictable
+section IsStronglyPredictable
 
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
     [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
@@ -541,7 +541,7 @@ theorem Martingale.eq_zero_of_predictable' [SigmaFiniteFiltration μ 𝒢] {f :
     (hfmgle : Martingale f 𝒢 μ) (hfadp : IsStronglyPredictable 𝒢 f) (n : ℕ) : f n =ᵐ[μ] f 0 :=
   eq_zero_of_predictable hfmgle (fun _ ↦ (hfadp.measurable_add_one _).stronglyMeasurable) n
 
-end IsPredictable
+end IsStronglyPredictable
 
 namespace Submartingale
 
diff --git a/Mathlib/Probability/Process/Predictable.lean b/Mathlib/Probability/Process/Predictable.lean
index 6c6fb90358577f..4455fe86f2f2be 100644
--- a/Mathlib/Probability/Process/Predictable.lean
+++ b/Mathlib/Probability/Process/Predictable.lean
@@ -17,13 +17,13 @@ and adapted. We also give an equivalent characterization of predictability for d
 ## Main definitions
 
 * `Filtration.predictable` : The predictable σ-algebra associated to a filtration.
-* `IsPredictable` : A process is predictable if it is measurable with respect to the
+* `IsStronglyPredictable` : A process is predictable if it is measurable with respect to the
   predictable σ-algebra.
 
 ## Main results
 
-* `IsPredictable.progMeasurable` : A predictable process is progressively measurable.
-* `isPredictable_iff_measurable_add_one` : `u` is a discrete predictable process iff
+* `IsStronglyPredictable.progMeasurable` : A predictable process is progressively measurable.
+* `isStronglyPredictable_iff_measurable_add_one` : `u` is a discrete predictable process iff
   `u (n + 1)` is `𝓕 n`-measurable and `u 0` is `𝓕 0`-measurable.
 
 ## Tags
@@ -127,7 +127,7 @@ lemma progMeasurable {𝓕 : Filtration ι m} {u : ι → Ω → E} (h𝓕 : IsS
     · simp [(by grind : (fun (p : Set.Iic i × Ω) ↦ ((p.1 : ι), p.2)) ⁻¹' Set.Ioi j ×ˢ A = ∅)]
 
 /-- A predictable process is adapted. -/
-lemma adapted {𝓕 : Filtration ι m} {u : ι → Ω → E} (h𝓕 : IsStronglyPredictable 𝓕 u) :
+lemma stronglyAdapted {𝓕 : Filtration ι m} {u : ι → Ω → E} (h𝓕 : IsStronglyPredictable 𝓕 u) :
     StronglyAdapted 𝓕 u :=
   h𝓕.progMeasurable.stronglyAdapted
 
@@ -191,7 +191,7 @@ lemma measurableSet_predictable_singleton_prod
     simp only [Set.mem_singleton_iff, Set.mem_Ioc]
     lia
 
-lemma isPredictable_of_measurable_add_one [SecondCountableTopology E]
+lemma isStronglyPredictable_of_measurable_add_one [SecondCountableTopology E]
     {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E}
     (h₀ : Measurable[𝓕 0] (u 0)) (h : ∀ n, Measurable[𝓕 n] (u (n + 1))) :
     IsStronglyPredictable 𝓕 u := by
@@ -206,11 +206,11 @@ lemma isPredictable_of_measurable_add_one [SecondCountableTopology E]
 
 /-- A discrete process `u` is predictable iff `u (n + 1)` is `𝓕 n`-measurable for all `n` and
 `u 0` is `𝓕 0`-measurable. -/
-lemma isPredictable_iff_measurable_add_one [SecondCountableTopology E]
+lemma isStronglyPredictable_iff_measurable_add_one [SecondCountableTopology E]
     {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E} :
     IsStronglyPredictable 𝓕 u ↔ Measurable[𝓕 0] (u 0) ∧ ∀ n, Measurable[𝓕 n] (u (n + 1)) :=
-  ⟨fun h𝓕 ↦ ⟨(h𝓕.adapted 0).measurable, fun n ↦ h𝓕.measurable_add_one (n)⟩,
-    fun h ↦ isPredictable_of_measurable_add_one h.1 h.2⟩
+  ⟨fun h𝓕 ↦ ⟨(h𝓕.stronglyAdapted 0).measurable, fun n ↦ h𝓕.measurable_add_one (n)⟩,
+    fun h ↦ isStronglyPredictable_of_measurable_add_one h.1 h.2⟩
 
 end
 

From b28f45c45ded8134ea8d96395f2366caff71e15b Mon Sep 17 00:00:00 2001
From: Joris van Winden <j.vanwinden@student.tudelft.nl>
Date: Sun, 19 Apr 2026 16:34:20 +0200
Subject: [PATCH 03/17] remove typeclasses from predictability lemmas with
 discrete filtration

---
 Mathlib/Probability/Martingale/Basic.lean    |  9 ++-
 Mathlib/Probability/Process/Predictable.lean | 63 +++++++++++---------
 2 files changed, 40 insertions(+), 32 deletions(-)

diff --git a/Mathlib/Probability/Martingale/Basic.lean b/Mathlib/Probability/Martingale/Basic.lean
index b8b0015f292aa1..6c4986ff7e455e 100644
--- a/Mathlib/Probability/Martingale/Basic.lean
+++ b/Mathlib/Probability/Martingale/Basic.lean
@@ -511,8 +511,7 @@ theorem Martingale.eq_zero_of_predictable [SigmaFiniteFiltration μ 𝒢] {f : 
 
 section IsStronglyPredictable
 
-variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
-    [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
 
 /-- A predictable submartingale is a.e. greater than or equal to its initial state.
 
@@ -522,7 +521,7 @@ measurable. -/
 theorem Submartingale.zero_le_of_predictable' [Preorder E] [SigmaFiniteFiltration μ 𝒢]
     {f : ℕ → Ω → E} (hfmgle : Submartingale f 𝒢 μ) (hf : IsStronglyPredictable 𝒢 f) (n : ℕ) :
     f 0 ≤ᵐ[μ] f n :=
-  zero_le_of_predictable hfmgle (fun _ ↦ (hf.measurable_add_one _).stronglyMeasurable) n
+  zero_le_of_predictable hfmgle hf.measurable_add_one n
 
 /-- A predictable supermartingale is a.e. less than or equal to its initial state.
 
@@ -531,7 +530,7 @@ is defined using strong measurability while `IsPredictable` only provides measur
 theorem Supermartingale.le_zero_of_predictable' [Preorder E] [SigmaFiniteFiltration μ 𝒢]
     {f : ℕ → Ω → E} (hfmgle : Supermartingale f 𝒢 μ) (hfadp : IsStronglyPredictable 𝒢 f)
     (n : ℕ) : f n ≤ᵐ[μ] f 0 :=
-  le_zero_of_predictable hfmgle (fun _ ↦ (hfadp.measurable_add_one _).stronglyMeasurable) n
+  le_zero_of_predictable hfmgle hfadp.measurable_add_one n
 
 /-- A predictable martingale is a.e. equal to its initial state.
 
@@ -539,7 +538,7 @@ In contrast to the non-primed version, this result requires second countability
 is defined using strong measurability while `IsPredictable` only provides measurable. -/
 theorem Martingale.eq_zero_of_predictable' [SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E}
     (hfmgle : Martingale f 𝒢 μ) (hfadp : IsStronglyPredictable 𝒢 f) (n : ℕ) : f n =ᵐ[μ] f 0 :=
-  eq_zero_of_predictable hfmgle (fun _ ↦ (hfadp.measurable_add_one _).stronglyMeasurable) n
+  eq_zero_of_predictable hfmgle hfadp.measurable_add_one n
 
 end IsStronglyPredictable
 
diff --git a/Mathlib/Probability/Process/Predictable.lean b/Mathlib/Probability/Process/Predictable.lean
index 4455fe86f2f2be..4ea7407c77aa86 100644
--- a/Mathlib/Probability/Process/Predictable.lean
+++ b/Mathlib/Probability/Process/Predictable.lean
@@ -131,7 +131,19 @@ lemma stronglyAdapted {𝓕 : Filtration ι m} {u : ι → Ω → E} (h𝓕 : Is
     StronglyAdapted 𝓕 u :=
   h𝓕.progMeasurable.stronglyAdapted
 
-omit [SecondCountableTopology E] in
+end IsStronglyPredictable
+
+section Discrete
+
+lemma measurableSet_predictable_singleton_prod
+    {𝓕 : Filtration ℕ m} {n : ℕ} {s : Set Ω} (hs : MeasurableSet[𝓕 n] s) :
+    MeasurableSet[𝓕.predictable] <| {n + 1} ×ˢ s := by
+  rw [(_ : {n + 1} = Set.Ioc n (n + 1))]
+  · exact measurableSet_predictable_Ioc_prod _ _ hs
+  · ext m
+    simp only [Set.mem_singleton_iff, Set.mem_Ioc]
+    lia
+
 lemma measurableSet_prodMk_add_one_of_predictable {𝓕 : Filtration ℕ m} {s : Set (ℕ × Ω)}
     (hs : MeasurableSet[𝓕.predictable] s) (n : ℕ) :
     MeasurableSet[𝓕 n] {ω | (n + 1, ω) ∈ s} := by
@@ -168,30 +180,27 @@ lemma measurableSet_prodMk_add_one_of_predictable {𝓕 : Filtration ℕ m} {s :
         rw [p.1.2]
         exact ⟨fun _ ↦ by aesop, fun _ ↦ lt_add_one_iff.2 hin⟩
 
-omit [SecondCountableTopology E] in
 /-- If `u` is a discrete predictable process, then `u (n + 1)` is `𝓕 n`-measurable. -/
-lemma measurable_add_one {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E} (h𝓕 : IsStronglyPredictable 𝓕 u)
-    (n : ℕ) : Measurable[𝓕 n] (u (n + 1)) := by
-  intro s hs
-  rw [(by aesop : u (n + 1) ⁻¹' s = {ω | (n + 1, ω) ∈ (Function.uncurry u) ⁻¹' s})]
-  exact measurableSet_prodMk_add_one_of_predictable (h𝓕.measurable hs) n
-
-end IsStronglyPredictable
-
-section
-
-variable [MetrizableSpace E] [MeasurableSpace E] [BorelSpace E]
-
-lemma measurableSet_predictable_singleton_prod
-    {𝓕 : Filtration ℕ m} {n : ℕ} {s : Set Ω} (hs : MeasurableSet[𝓕 n] s) :
-    MeasurableSet[𝓕.predictable] <| {n + 1} ×ˢ s := by
-  rw [(_ : {n + 1} = Set.Ioc n (n + 1))]
-  · exact measurableSet_predictable_Ioc_prod _ _ hs
-  · ext m
-    simp only [Set.mem_singleton_iff, Set.mem_Ioc]
-    lia
-
-lemma isStronglyPredictable_of_measurable_add_one [SecondCountableTopology E]
+lemma IsStronglyPredictable.measurable_add_one {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E}
+    (h𝓕 : IsStronglyPredictable 𝓕 u) (n : ℕ) : StronglyMeasurable[𝓕 n] (u (n + 1)) := by
+  -- approximating sequence
+  let Y k := (Function.curry @(h𝓕.approx k).toFun (n + 1))
+  use (fun k ↦ @SimpleFunc.mk _ (𝓕 n) _ (Y k) ?_ ?_)
+  · exact fun ω ↦ h𝓕.tendsto_approx ⟨(n + 1), ω⟩
+  · intro s
+    have : Y k ⁻¹' {s} = {ω | (n + 1, ω) ∈ @(h𝓕.approx k).toFun ⁻¹' {s}} := by
+      aesop
+    rw [this]
+    apply measurableSet_prodMk_add_one_of_predictable
+    apply @(h𝓕.approx k).measurableSet_fiber
+  · have := @(h𝓕.approx k).finite_range
+    apply this.subset
+    rw [Set.range_subset_iff]
+    aesop
+
+variable [MetrizableSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
+
+lemma isStronglyPredictable_of_measurable_add_one
     {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E}
     (h₀ : Measurable[𝓕 0] (u 0)) (h : ∀ n, Measurable[𝓕 n] (u (n + 1))) :
     IsStronglyPredictable 𝓕 u := by
@@ -206,12 +215,12 @@ lemma isStronglyPredictable_of_measurable_add_one [SecondCountableTopology E]
 
 /-- A discrete process `u` is predictable iff `u (n + 1)` is `𝓕 n`-measurable for all `n` and
 `u 0` is `𝓕 0`-measurable. -/
-lemma isStronglyPredictable_iff_measurable_add_one [SecondCountableTopology E]
+lemma IsStronglyPredictable.isStronglyPredictable_iff_measurable_add_one
     {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E} :
     IsStronglyPredictable 𝓕 u ↔ Measurable[𝓕 0] (u 0) ∧ ∀ n, Measurable[𝓕 n] (u (n + 1)) :=
-  ⟨fun h𝓕 ↦ ⟨(h𝓕.stronglyAdapted 0).measurable, fun n ↦ h𝓕.measurable_add_one (n)⟩,
+  ⟨fun h𝓕 ↦ ⟨(h𝓕.stronglyAdapted 0).measurable, fun n ↦ (h𝓕.measurable_add_one n).measurable⟩,
     fun h ↦ isStronglyPredictable_of_measurable_add_one h.1 h.2⟩
 
-end
+end Discrete
 
 end MeasureTheory

From 4c96cd31dcfe66715ed2741c32e5d8df94538a97 Mon Sep 17 00:00:00 2001
From: Joris van Winden <j.vanwinden@student.tudelft.nl>
Date: Sun, 19 Apr 2026 16:39:37 +0200
Subject: [PATCH 04/17] golf proof

---
 Mathlib/Probability/Process/Predictable.lean | 13 ++++---------
 1 file changed, 4 insertions(+), 9 deletions(-)

diff --git a/Mathlib/Probability/Process/Predictable.lean b/Mathlib/Probability/Process/Predictable.lean
index 4ea7407c77aa86..f7bedcc82510a3 100644
--- a/Mathlib/Probability/Process/Predictable.lean
+++ b/Mathlib/Probability/Process/Predictable.lean
@@ -183,18 +183,13 @@ lemma measurableSet_prodMk_add_one_of_predictable {𝓕 : Filtration ℕ m} {s :
 /-- If `u` is a discrete predictable process, then `u (n + 1)` is `𝓕 n`-measurable. -/
 lemma IsStronglyPredictable.measurable_add_one {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E}
     (h𝓕 : IsStronglyPredictable 𝓕 u) (n : ℕ) : StronglyMeasurable[𝓕 n] (u (n + 1)) := by
-  -- approximating sequence
-  let Y k := (Function.curry @(h𝓕.approx k).toFun (n + 1))
-  use (fun k ↦ @SimpleFunc.mk _ (𝓕 n) _ (Y k) ?_ ?_)
-  · exact fun ω ↦ h𝓕.tendsto_approx ⟨(n + 1), ω⟩
+  let X k := (Function.curry @(h𝓕.approx k).toFun (n + 1))
+  refine ⟨(fun k ↦ @SimpleFunc.mk _ (𝓕 n) _ (X k) ?_ ?_), (fun ω ↦ h𝓕.tendsto_approx ⟨(n + 1), ω⟩)⟩
   · intro s
-    have : Y k ⁻¹' {s} = {ω | (n + 1, ω) ∈ @(h𝓕.approx k).toFun ⁻¹' {s}} := by
-      aesop
-    rw [this]
+    rw [(by aesop : X k ⁻¹' {s} = {ω | (n + 1, ω) ∈ @(h𝓕.approx k).toFun ⁻¹' {s}})]
     apply measurableSet_prodMk_add_one_of_predictable
     apply @(h𝓕.approx k).measurableSet_fiber
-  · have := @(h𝓕.approx k).finite_range
-    apply this.subset
+  · apply (@(h𝓕.approx k).finite_range).subset
     rw [Set.range_subset_iff]
     aesop
 

From 3ec1da865652201fba9f12001e609261a86aa90a Mon Sep 17 00:00:00 2001
From: Joris van Winden <j.vanwinden@student.tudelft.nl>
Date: Sun, 19 Apr 2026 16:41:32 +0200
Subject: [PATCH 05/17] remove outdated comments

---
 Mathlib/Probability/Martingale/Basic.lean | 16 +++-------------
 1 file changed, 3 insertions(+), 13 deletions(-)

diff --git a/Mathlib/Probability/Martingale/Basic.lean b/Mathlib/Probability/Martingale/Basic.lean
index 6c4986ff7e455e..30a8e8a2209760 100644
--- a/Mathlib/Probability/Martingale/Basic.lean
+++ b/Mathlib/Probability/Martingale/Basic.lean
@@ -513,29 +513,19 @@ section IsStronglyPredictable
 
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
 
-/-- A predictable submartingale is a.e. greater than or equal to its initial state.
-
-In contrast to the non-primed version, this result requires second countability as
-`StronglyAdapted` is defined using strong measurability while `IsPredictable` only provides
-measurable. -/
+/-- A predictable submartingale is a.e. greater than or equal to its initial state. -/
 theorem Submartingale.zero_le_of_predictable' [Preorder E] [SigmaFiniteFiltration μ 𝒢]
     {f : ℕ → Ω → E} (hfmgle : Submartingale f 𝒢 μ) (hf : IsStronglyPredictable 𝒢 f) (n : ℕ) :
     f 0 ≤ᵐ[μ] f n :=
   zero_le_of_predictable hfmgle hf.measurable_add_one n
 
-/-- A predictable supermartingale is a.e. less than or equal to its initial state.
-
-In contrast to the non-primed version, this result requires second countability as `StronglyAdapted`
-is defined using strong measurability while `IsPredictable` only provides measurable. -/
+/-- A predictable supermartingale is a.e. less than or equal to its initial state. -/
 theorem Supermartingale.le_zero_of_predictable' [Preorder E] [SigmaFiniteFiltration μ 𝒢]
     {f : ℕ → Ω → E} (hfmgle : Supermartingale f 𝒢 μ) (hfadp : IsStronglyPredictable 𝒢 f)
     (n : ℕ) : f n ≤ᵐ[μ] f 0 :=
   le_zero_of_predictable hfmgle hfadp.measurable_add_one n
 
-/-- A predictable martingale is a.e. equal to its initial state.
-
-In contrast to the non-primed version, this result requires second countability as `StronglyAdapted`
-is defined using strong measurability while `IsPredictable` only provides measurable. -/
+/-- A predictable martingale is a.e. equal to its initial state. -/
 theorem Martingale.eq_zero_of_predictable' [SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E}
     (hfmgle : Martingale f 𝒢 μ) (hfadp : IsStronglyPredictable 𝒢 f) (n : ℕ) : f n =ᵐ[μ] f 0 :=
   eq_zero_of_predictable hfmgle hfadp.measurable_add_one n

From 7c5b09a99917565ac980f8a2a3bfafb34a8db3b3 Mon Sep 17 00:00:00 2001
From: Joris van Winden <j.vanwinden@student.tudelft.nl>
Date: Mon, 20 Apr 2026 09:49:54 +0200
Subject: [PATCH 06/17] clean up proof using letI

---
 Mathlib/Probability/Process/Predictable.lean | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Probability/Process/Predictable.lean b/Mathlib/Probability/Process/Predictable.lean
index f7bedcc82510a3..0ca5cff2e7a53b 100644
--- a/Mathlib/Probability/Process/Predictable.lean
+++ b/Mathlib/Probability/Process/Predictable.lean
@@ -183,13 +183,15 @@ lemma measurableSet_prodMk_add_one_of_predictable {𝓕 : Filtration ℕ m} {s :
 /-- If `u` is a discrete predictable process, then `u (n + 1)` is `𝓕 n`-measurable. -/
 lemma IsStronglyPredictable.measurable_add_one {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E}
     (h𝓕 : IsStronglyPredictable 𝓕 u) (n : ℕ) : StronglyMeasurable[𝓕 n] (u (n + 1)) := by
-  let X k := (Function.curry @(h𝓕.approx k).toFun (n + 1))
-  refine ⟨(fun k ↦ @SimpleFunc.mk _ (𝓕 n) _ (X k) ?_ ?_), (fun ω ↦ h𝓕.tendsto_approx ⟨(n + 1), ω⟩)⟩
+  letI : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
+  letI : MeasurableSpace Ω := 𝓕 n
+  let X k := (Function.curry (h𝓕.approx k) (n + 1))
+  refine ⟨(fun k ↦ SimpleFunc.mk (X k) ?_ ?_), (fun ω ↦ h𝓕.tendsto_approx ⟨(n + 1), ω⟩)⟩
   · intro s
-    rw [(by aesop : X k ⁻¹' {s} = {ω | (n + 1, ω) ∈ @(h𝓕.approx k).toFun ⁻¹' {s}})]
+    rw [(by aesop : X k ⁻¹' {s} = {ω | (n + 1, ω) ∈ h𝓕.approx k ⁻¹' {s}})]
     apply measurableSet_prodMk_add_one_of_predictable
-    apply @(h𝓕.approx k).measurableSet_fiber
-  · apply (@(h𝓕.approx k).finite_range).subset
+    apply (h𝓕.approx k).measurableSet_fiber
+  · apply (h𝓕.approx k).finite_range.subset
     rw [Set.range_subset_iff]
     aesop
 

From e90d526bdc17e790507386b22d6cfe954bc8d9ff Mon Sep 17 00:00:00 2001
From: Joris van Winden <j.vanwinden@student.tudelft.nl>
Date: Mon, 20 Apr 2026 12:25:21 +0200
Subject: [PATCH 07/17] reorganize, partially remove typeclasses from
 ispredictable_of_measurable_add_one

---
 Mathlib/Probability/Process/Predictable.lean | 166 ++++++++++++-------
 1 file changed, 110 insertions(+), 56 deletions(-)

diff --git a/Mathlib/Probability/Process/Predictable.lean b/Mathlib/Probability/Process/Predictable.lean
index 0ca5cff2e7a53b..fb784e02177c31 100644
--- a/Mathlib/Probability/Process/Predictable.lean
+++ b/Mathlib/Probability/Process/Predictable.lean
@@ -40,31 +40,22 @@ open scoped MeasureTheory NNReal ENNReal Topology
 
 namespace MeasureTheory
 
-variable {Ω ι : Type*} {m : MeasurableSpace Ω} {E : Type*} [TopologicalSpace E]
+variable {Ω ι : Type*} {m : MeasurableSpace Ω} {E : Type*}
 
 section
 
-variable [Preorder ι] [OrderBot ι]
-
 namespace Filtration
 
 /-- Given a filtration `𝓕`, the predictable σ-algebra is the σ-algebra on `ι × Ω` generated by
 sets of the form `(t, ∞) × A` for `t ∈ ι` and `A ∈ 𝓕 t` and `{⊥} × A` for `A ∈ 𝓕 ⊥`. -/
 @[implicit_reducible]
-def predictable (𝓕 : Filtration ι m) : MeasurableSpace (ι × Ω) :=
+def predictable [Preorder ι] [OrderBot ι] (𝓕 : Filtration ι m) : MeasurableSpace (ι × Ω) :=
   MeasurableSpace.generateFrom <|
     {s | ∃ A, MeasurableSet[𝓕 ⊥] A ∧ s = {⊥} ×ˢ A} ∪
     {s | ∃ i A, MeasurableSet[𝓕 i] A ∧ s = Set.Ioi i ×ˢ A}
 
 end Filtration
 
-/-- A process is said to be predictable if it is measurable with respect to the predictable
-σ-algebra. -/
-def IsStronglyPredictable (𝓕 : Filtration ι m) (u : ι → Ω → E) :=
-  StronglyMeasurable[𝓕.predictable] <| Function.uncurry u
-
-end
-
 lemma measurableSet_predictable_singleton_bot_prod [LinearOrder ι] [OrderBot ι]
     {𝓕 : Filtration ι m} {s : Set Ω} (hs : MeasurableSet[𝓕 ⊥] s) :
     MeasurableSet[𝓕.predictable] <| {⊥} ×ˢ s :=
@@ -87,6 +78,51 @@ lemma measurableSet_predictable_Ioc_prod [LinearOrder ι] [OrderBot ι]
     exact (measurableSet_predictable_Ioi_prod hs).diff
       (measurableSet_predictable_Ioi_prod <| 𝓕.mono hij _ hs)
 
+lemma measurableSet_predictable_singleton_prod
+    {𝓕 : Filtration ℕ m} {n : ℕ} {s : Set Ω} (hs : MeasurableSet[𝓕 n] s) :
+    MeasurableSet[𝓕.predictable] <| {n + 1} ×ˢ s := by
+  rw [(_ : {n + 1} = Set.Ioc n (n + 1))]
+  · exact measurableSet_predictable_Ioc_prod _ _ hs
+  · ext m
+    simp only [Set.mem_singleton_iff, Set.mem_Ioc]
+    lia
+
+lemma measurableSet_prodMk_add_one_of_predictable {𝓕 : Filtration ℕ m} {s : Set (ℕ × Ω)}
+    (hs : MeasurableSet[𝓕.predictable] s) (n : ℕ) :
+    MeasurableSet[𝓕 n] {ω | (n + 1, ω) ∈ s} := by
+  rw [(by aesop : {ω | (n + 1, ω) ∈ s} = (Prod.mk (α := Set.singleton (n + 1)) (β := Ω)
+      ⟨n + 1, rfl⟩) ⁻¹' ((fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' s))]
+  refine measurableSet_preimage (mβ := Subtype.instMeasurableSpace.prod (𝓕 n))
+    measurable_prodMk_left <| measurableSet_preimage ?_ hs
+  rw [measurable_iff_comap_le, MeasurableSpace.comap_le_iff_le_map]
+  refine MeasurableSpace.generateFrom_le ?_
+  rintro - (⟨A, hA, rfl⟩ | ⟨i, A, hA, rfl⟩)
+  · rw [MeasurableSpace.map_def,
+      (_ : (fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' ({⊥} ×ˢ A) = ∅)]
+    · simp
+    · ext p
+      simp only [Nat.bot_eq_zero, Set.mem_preimage, Set.mem_prod, Set.mem_singleton_iff,
+        Set.mem_empty_iff_false, iff_false, not_and]
+      exact fun hp1 ↦ False.elim <| Nat.succ_ne_zero n (hp1 ▸ p.1.2.symm)
+  · rw [MeasurableSpace.map_def]
+    obtain hni | hin := lt_or_ge n i
+    · rw [(_ : (fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' (Set.Ioi i ×ˢ A) = ∅)]
+      · simp
+      · ext p
+        simp only [Set.mem_preimage, Set.mem_prod, Set.mem_Ioi, Set.mem_empty_iff_false,
+          iff_false, not_and]
+        rw [p.1.2]
+        grind
+    · rw [(_ : (fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' (Set.Ioi i ×ˢ A)
+          = {⟨n + 1, rfl⟩} ×ˢ A)]
+      · exact MeasurableSet.prod (MeasurableSet.of_subtype_image trivial) (𝓕.mono hin _ hA)
+      · ext p
+        simp only [Set.mem_preimage, Set.mem_prod, Set.mem_Ioi, Set.mem_singleton_iff,
+          and_congr_left_iff]
+        intro hp2
+        rw [p.1.2]
+        exact ⟨fun _ ↦ by aesop, fun _ ↦ lt_add_one_iff.2 hin⟩
+
 lemma measurableSpace_le_predictable_of_measurableSet [Preorder ι] [OrderBot ι]
     {𝓕 : Filtration ι m} {m' : MeasurableSpace (ι × Ω)}
     (hm'bot : ∀ A, MeasurableSet[𝓕 ⊥] A → MeasurableSet[m'] ({⊥} ×ˢ A))
@@ -97,6 +133,17 @@ lemma measurableSpace_le_predictable_of_measurableSet [Preorder ι] [OrderBot ι
   · exact hm'bot A hA
   · exact hm' i A hA
 
+end
+
+section StronglyPredictable
+
+variable [TopologicalSpace E]
+
+/-- A process is said to be predictable if it is measurable with respect to the predictable
+σ-algebra. -/
+def IsStronglyPredictable [Preorder ι] [OrderBot ι] (𝓕 : Filtration ι m) (u : ι → Ω → E) :=
+  StronglyMeasurable[𝓕.predictable] <| Function.uncurry u
+
 namespace IsStronglyPredictable
 
 open Filtration
@@ -135,51 +182,6 @@ end IsStronglyPredictable
 
 section Discrete
 
-lemma measurableSet_predictable_singleton_prod
-    {𝓕 : Filtration ℕ m} {n : ℕ} {s : Set Ω} (hs : MeasurableSet[𝓕 n] s) :
-    MeasurableSet[𝓕.predictable] <| {n + 1} ×ˢ s := by
-  rw [(_ : {n + 1} = Set.Ioc n (n + 1))]
-  · exact measurableSet_predictable_Ioc_prod _ _ hs
-  · ext m
-    simp only [Set.mem_singleton_iff, Set.mem_Ioc]
-    lia
-
-lemma measurableSet_prodMk_add_one_of_predictable {𝓕 : Filtration ℕ m} {s : Set (ℕ × Ω)}
-    (hs : MeasurableSet[𝓕.predictable] s) (n : ℕ) :
-    MeasurableSet[𝓕 n] {ω | (n + 1, ω) ∈ s} := by
-  rw [(by aesop : {ω | (n + 1, ω) ∈ s} = (Prod.mk (α := Set.singleton (n + 1)) (β := Ω)
-      ⟨n + 1, rfl⟩) ⁻¹' ((fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' s))]
-  refine measurableSet_preimage (mβ := Subtype.instMeasurableSpace.prod (𝓕 n))
-    measurable_prodMk_left <| measurableSet_preimage ?_ hs
-  rw [measurable_iff_comap_le, MeasurableSpace.comap_le_iff_le_map]
-  refine MeasurableSpace.generateFrom_le ?_
-  rintro - (⟨A, hA, rfl⟩ | ⟨i, A, hA, rfl⟩)
-  · rw [MeasurableSpace.map_def,
-      (_ : (fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' ({⊥} ×ˢ A) = ∅)]
-    · simp
-    · ext p
-      simp only [Nat.bot_eq_zero, Set.mem_preimage, Set.mem_prod, Set.mem_singleton_iff,
-        Set.mem_empty_iff_false, iff_false, not_and]
-      exact fun hp1 ↦ False.elim <| Nat.succ_ne_zero n (hp1 ▸ p.1.2.symm)
-  · rw [MeasurableSpace.map_def]
-    obtain hni | hin := lt_or_ge n i
-    · rw [(_ : (fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' (Set.Ioi i ×ˢ A) = ∅)]
-      · simp
-      · ext p
-        simp only [Set.mem_preimage, Set.mem_prod, Set.mem_Ioi, Set.mem_empty_iff_false,
-          iff_false, not_and]
-        rw [p.1.2]
-        grind
-    · rw [(_ : (fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' (Set.Ioi i ×ˢ A)
-          = {⟨n + 1, rfl⟩} ×ˢ A)]
-      · exact MeasurableSet.prod (MeasurableSet.of_subtype_image trivial) (𝓕.mono hin _ hA)
-      · ext p
-        simp only [Set.mem_preimage, Set.mem_prod, Set.mem_Ioi, Set.mem_singleton_iff,
-          and_congr_left_iff]
-        intro hp2
-        rw [p.1.2]
-        exact ⟨fun _ ↦ by aesop, fun _ ↦ lt_add_one_iff.2 hin⟩
-
 /-- If `u` is a discrete predictable process, then `u (n + 1)` is `𝓕 n`-measurable. -/
 lemma IsStronglyPredictable.measurable_add_one {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E}
     (h𝓕 : IsStronglyPredictable 𝓕 u) (n : ℕ) : StronglyMeasurable[𝓕 n] (u (n + 1)) := by
@@ -195,6 +197,56 @@ lemma IsStronglyPredictable.measurable_add_one {𝓕 : Filtration ℕ m} {u : 
     rw [Set.range_subset_iff]
     aesop
 
+lemma isStronglyPredictable_of_measurable_add_one'
+    {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E}
+    (h₀ : StronglyMeasurable[𝓕 0] (u 0)) (h : ∀ n, StronglyMeasurable[𝓕 n] (u (n + 1))) :
+    IsStronglyPredictable 𝓕 u := by
+  letI : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
+  -- first layer of approximation
+  let X m (x : ℕ × Ω) := match x.1 with
+    | 0 => h₀.approx m x.2
+    | n + 1 => (h n).approx m x.2
+  -- second layer of approximation (to ensure Y has finite range as a process)
+  let Y m (x : ℕ × Ω) := if x.1 ≤ m then X m x else X m ⟨0, x.2⟩
+  use fun m ↦ SimpleFunc.mk (Y m) ?_ ?_
+  · intro ⟨n, ω⟩
+    rw [tendsto_congr' (f₂ := fun m ↦ X m ⟨n, ω⟩)]
+    · rcases n with rfl | k
+      · exact h₀.tendsto_approx ω
+      · exact (h k).tendsto_approx ω
+    · filter_upwards [eventually_ge_atTop n] with m hm using by simp; grind
+  · intro s
+    rw [(by aesop : Y m ⁻¹' {s} = ⋃ n : ℕ, {n} ×ˢ ((Function.curry (Y m) n) ⁻¹' {s}))]
+    refine MeasurableSet.iUnion <| fun n ↦ ?_
+    rcases n with rfl | k
+    · apply measurableSet_predictable_singleton_bot_prod
+      letI : MeasurableSpace Ω := 𝓕 0
+      exact (h₀.approx m).measurableSet_fiber s
+    · apply measurableSet_predictable_singleton_prod
+      by_cases! hmk : k + 1 ≤ m
+      · rw [(by aesop : Function.curry (Y m) (k + 1) = Function.curry (X m) (k + 1))]
+        letI : MeasurableSpace Ω := 𝓕 k
+        exact ((h k).approx m).measurableSet_fiber s
+      · rw [(by aesop : Function.curry (Y m) (k + 1) = Function.curry (X m) 0)]
+        letI : MeasurableSpace Ω := 𝓕 0
+        have := (h₀.approx m).measurableSet_fiber s
+        -- first shrink sigma field to 𝓕 0
+        -- then apply this (h₀.approx m).measurableSet_fiber s
+        sorry -- split into cases and use that filtration is increasing
+      --exact ((h k).approx m).measurableSet_fiber s
+  · apply Set.Finite.subset (s := ⋃ n ∈ Finset.range (m + 1), Set.range (Function.curry (X m) n))
+    · refine Set.Finite.biUnion' (by aesop) ?_
+      intro k hk
+      rcases k with rfl | k
+      · exact @(h₀.approx m).finite_range
+      · exact @((h k).approx m).finite_range
+    · intro e he
+      obtain ⟨⟨k, ω⟩, he'⟩ := Set.mem_range.mp he
+      simp_rw [Set.mem_iUnion, Set.mem_range]
+      by_cases! h' : k ≤ m
+      · exact ⟨k, by aesop⟩
+      · exact ⟨0, by aesop, ω, by aesop⟩
+
 variable [MetrizableSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
 
 lemma isStronglyPredictable_of_measurable_add_one
@@ -220,4 +272,6 @@ lemma IsStronglyPredictable.isStronglyPredictable_iff_measurable_add_one
 
 end Discrete
 
+end StronglyPredictable
+
 end MeasureTheory

From 96d0711ddf7a54dc1a66241df87fef27fe34db16 Mon Sep 17 00:00:00 2001
From: Joris van Winden <j.vanwinden@student.tudelft.nl>
Date: Mon, 20 Apr 2026 14:34:47 +0200
Subject: [PATCH 08/17] remove more typeclasses and sorrys

---
 Mathlib/Probability/Process/Predictable.lean | 93 +++++++++-----------
 1 file changed, 41 insertions(+), 52 deletions(-)

diff --git a/Mathlib/Probability/Process/Predictable.lean b/Mathlib/Probability/Process/Predictable.lean
index fb784e02177c31..ace14f8dd8416e 100644
--- a/Mathlib/Probability/Process/Predictable.lean
+++ b/Mathlib/Probability/Process/Predictable.lean
@@ -23,7 +23,7 @@ and adapted. We also give an equivalent characterization of predictability for d
 ## Main results
 
 * `IsStronglyPredictable.progMeasurable` : A predictable process is progressively measurable.
-* `isStronglyPredictable_iff_measurable_add_one` : `u` is a discrete predictable process iff
+* `IsStronglyPredictable.iff_measurable_add_one` : `u` is a discrete predictable process iff
   `u (n + 1)` is `𝓕 n`-measurable and `u 0` is `𝓕 0`-measurable.
 
 ## Tags
@@ -133,9 +133,28 @@ lemma measurableSpace_le_predictable_of_measurableSet [Preorder ι] [OrderBot ι
   · exact hm'bot A hA
   · exact hm' i A hA
 
-end
+/-- The inclusion map from [0,i] × Ω with the subtype × 𝓕 i σ-algebra) to ι × Ω with the
+predictable σ-algebra is measurable -/
+lemma measurable_inclusion_predictable [LinearOrder ι] [OrderBot ι] [MeasurableSpace ι]
+    [TopologicalSpace ι] [OpensMeasurableSpace ι] [OrderClosedTopology ι] {𝓕 : Filtration ι m} {i} :
+    @Measurable (Set.Iic i × Ω) (ι × Ω) (Subtype.instMeasurableSpace.prod (𝓕 i)) 𝓕.predictable
+    fun x ↦ ⟨x.1.val, x.2⟩ := by
+  rw [measurable_iff_comap_le]
+  refine MeasurableSpace.comap_le_iff_le_map.2 <|
+    measurableSpace_le_predictable_of_measurableSet ?_ ?_
+  · intros A hA
+    simp only [MeasurableSpace.map_def,
+      (by aesop : (fun (p : Set.Iic i × Ω) ↦ ((p.1 : ι), p.2)) ⁻¹' ({⊥} ×ˢ A) = {⊥} ×ˢ A)]
+    exact (measurableSet_singleton _).prod <| 𝓕.mono bot_le _ hA
+  · intros j A hA
+    simp only [MeasurableSpace.map_def]
+    obtain hji | hij := le_total j i
+    · rw [(by grind : (fun (p : Set.Iic i × Ω) ↦ ((p.1 : ι), p.2)) ⁻¹' Set.Ioi j ×ˢ A
+        = (Subtype.val ⁻¹' (Set.Ioc j i)) ×ˢ A)]
+      exact (measurable_subtype_coe measurableSet_Ioc).prod (𝓕.mono hji _ hA)
+    · simp [(by grind : (fun (p : Set.Iic i × Ω) ↦ ((p.1 : ι), p.2)) ⁻¹' Set.Ioi j ×ˢ A = ∅)]
 
-section StronglyPredictable
+end
 
 variable [TopologicalSpace E]
 
@@ -150,40 +169,28 @@ open Filtration
 
 variable [LinearOrder ι] [OrderBot ι] [MeasurableSpace ι] [TopologicalSpace ι]
     [OpensMeasurableSpace ι] [OrderClosedTopology ι]
-    [MetrizableSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
 
 /-- A predictable process is progressively measurable. -/
 lemma progMeasurable {𝓕 : Filtration ι m} {u : ι → Ω → E} (h𝓕 : IsStronglyPredictable 𝓕 u) :
     ProgMeasurable 𝓕 u := by
-  refine fun i ↦ Measurable.stronglyMeasurable ?_
-  rw [IsStronglyPredictable, stronglyMeasurable_iff_measurable, measurable_iff_comap_le] at h𝓕
-  rw [measurable_iff_comap_le, (by aesop : (fun (p : Set.Iic i × Ω) ↦ u (p.1) p.2)
-      = Function.uncurry u ∘ (fun p ↦ (p.1, p.2))), ← MeasurableSpace.comap_comp]
-  refine (MeasurableSpace.comap_mono h𝓕).trans <| MeasurableSpace.comap_le_iff_le_map.2 <|
-    measurableSpace_le_predictable_of_measurableSet ?_ ?_
-  · intros A hA
-    simp only [MeasurableSpace.map_def,
-      (by aesop : (fun (p : Set.Iic i × Ω) ↦ ((p.1 : ι), p.2)) ⁻¹' ({⊥} ×ˢ A) = {⊥} ×ˢ A)]
-    exact (measurableSet_singleton _).prod <| 𝓕.mono bot_le _ hA
-  · intros j A hA
-    simp only [MeasurableSpace.map_def]
-    obtain hji | hij := le_total j i
-    · rw [(by grind : (fun (p : Set.Iic i × Ω) ↦ ((p.1 : ι), p.2)) ⁻¹' Set.Ioi j ×ˢ A
-        = (Subtype.val ⁻¹' (Set.Ioc j i)) ×ˢ A)]
-      exact (measurable_subtype_coe measurableSet_Ioc).prod (𝓕.mono hji _ hA)
-    · simp [(by grind : (fun (p : Set.Iic i × Ω) ↦ ((p.1 : ι), p.2)) ⁻¹' Set.Ioi j ×ˢ A = ∅)]
+  intro i
+  letI : MeasurableSpace (ι × Ω) := 𝓕.predictable
+  letI : MeasurableSpace (Set.Iic i × Ω) := Subtype.instMeasurableSpace.prod (𝓕 i)
+  let X m (x : Set.Iic i × Ω) := h𝓕.approx m ⟨x.1, x.2⟩
+  refine ⟨fun m ↦ SimpleFunc.mk (X m) ?_ ?_, ?_⟩
+  · exact fun e ↦ measurable_inclusion_predictable <| (h𝓕.approx m).measurableSet_fiber e
+  · exact Set.Finite.subset (h𝓕.approx m).finite_range (by grind)
+  · exact fun n ↦ by apply h𝓕.tendsto_approx
 
 /-- A predictable process is adapted. -/
 lemma stronglyAdapted {𝓕 : Filtration ι m} {u : ι → Ω → E} (h𝓕 : IsStronglyPredictable 𝓕 u) :
     StronglyAdapted 𝓕 u :=
   h𝓕.progMeasurable.stronglyAdapted
 
-end IsStronglyPredictable
-
 section Discrete
 
 /-- If `u` is a discrete predictable process, then `u (n + 1)` is `𝓕 n`-measurable. -/
-lemma IsStronglyPredictable.measurable_add_one {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E}
+lemma measurable_add_one {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E}
     (h𝓕 : IsStronglyPredictable 𝓕 u) (n : ℕ) : StronglyMeasurable[𝓕 n] (u (n + 1)) := by
   letI : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
   letI : MeasurableSpace Ω := 𝓕 n
@@ -197,8 +204,7 @@ lemma IsStronglyPredictable.measurable_add_one {𝓕 : Filtration ℕ m} {u : 
     rw [Set.range_subset_iff]
     aesop
 
-lemma isStronglyPredictable_of_measurable_add_one'
-    {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E}
+lemma of_measurable_add_one {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E}
     (h₀ : StronglyMeasurable[𝓕 0] (u 0)) (h : ∀ n, StronglyMeasurable[𝓕 n] (u (n + 1))) :
     IsStronglyPredictable 𝓕 u := by
   letI : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
@@ -206,7 +212,7 @@ lemma isStronglyPredictable_of_measurable_add_one'
   let X m (x : ℕ × Ω) := match x.1 with
     | 0 => h₀.approx m x.2
     | n + 1 => (h n).approx m x.2
-  -- second layer of approximation (to ensure Y has finite range as a process)
+  -- second layer of approximation (to ensure the whole process has finite range)
   let Y m (x : ℕ × Ω) := if x.1 ≤ m then X m x else X m ⟨0, x.2⟩
   use fun m ↦ SimpleFunc.mk (Y m) ?_ ?_
   · intro ⟨n, ω⟩
@@ -228,12 +234,9 @@ lemma isStronglyPredictable_of_measurable_add_one'
         letI : MeasurableSpace Ω := 𝓕 k
         exact ((h k).approx m).measurableSet_fiber s
       · rw [(by aesop : Function.curry (Y m) (k + 1) = Function.curry (X m) 0)]
+        apply 𝓕.mono (i := 0) (by simp)
         letI : MeasurableSpace Ω := 𝓕 0
-        have := (h₀.approx m).measurableSet_fiber s
-        -- first shrink sigma field to 𝓕 0
-        -- then apply this (h₀.approx m).measurableSet_fiber s
-        sorry -- split into cases and use that filtration is increasing
-      --exact ((h k).approx m).measurableSet_fiber s
+        exact (h₀.approx m).measurableSet_fiber s
   · apply Set.Finite.subset (s := ⋃ n ∈ Finset.range (m + 1), Set.range (Function.curry (X m) n))
     · refine Set.Finite.biUnion' (by aesop) ?_
       intro k hk
@@ -247,31 +250,17 @@ lemma isStronglyPredictable_of_measurable_add_one'
       · exact ⟨k, by aesop⟩
       · exact ⟨0, by aesop, ω, by aesop⟩
 
-variable [MetrizableSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
-
-lemma isStronglyPredictable_of_measurable_add_one
-    {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E}
-    (h₀ : Measurable[𝓕 0] (u 0)) (h : ∀ n, Measurable[𝓕 n] (u (n + 1))) :
-    IsStronglyPredictable 𝓕 u := by
-  refine Measurable.stronglyMeasurable ?_
-  intro s hs
-  rw [(by aesop : Function.uncurry u ⁻¹' s = ⋃ n : ℕ, {n} ×ˢ (u n ⁻¹' s))]
-  refine MeasurableSet.iUnion <| fun n ↦ ?_
-  obtain (rfl | hn) := n.eq_zero_or_eq_succ_pred
-  · exact MeasurableSpace.measurableSet_generateFrom <| Or.inl ⟨u 0 ⁻¹' s, h₀ hs, rfl⟩
-  · rw [hn]
-    exact measurableSet_predictable_singleton_prod (h (n - 1) hs)
-
 /-- A discrete process `u` is predictable iff `u (n + 1)` is `𝓕 n`-measurable for all `n` and
 `u 0` is `𝓕 0`-measurable. -/
-lemma IsStronglyPredictable.isStronglyPredictable_iff_measurable_add_one
+lemma iff_measurable_add_one
     {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E} :
-    IsStronglyPredictable 𝓕 u ↔ Measurable[𝓕 0] (u 0) ∧ ∀ n, Measurable[𝓕 n] (u (n + 1)) :=
-  ⟨fun h𝓕 ↦ ⟨(h𝓕.stronglyAdapted 0).measurable, fun n ↦ (h𝓕.measurable_add_one n).measurable⟩,
-    fun h ↦ isStronglyPredictable_of_measurable_add_one h.1 h.2⟩
+    IsStronglyPredictable 𝓕 u ↔
+    StronglyMeasurable[𝓕 0] (u 0) ∧ ∀ n, StronglyMeasurable[𝓕 n] (u (n + 1)) :=
+  ⟨fun h𝓕 ↦ ⟨h𝓕.progMeasurable.stronglyAdapted 0, h𝓕.measurable_add_one⟩,
+    fun h ↦ .of_measurable_add_one h.1 h.2⟩
 
 end Discrete
 
-end StronglyPredictable
+end IsStronglyPredictable
 
 end MeasureTheory

From a42e2c8e072574ecaf065e6b40eb6d9caa3719ed Mon Sep 17 00:00:00 2001
From: Joris van Winden <j.vanwinden@student.tudelft.nl>
Date: Mon, 20 Apr 2026 14:43:40 +0200
Subject: [PATCH 09/17] small change

---
 Mathlib/Probability/Process/Predictable.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Probability/Process/Predictable.lean b/Mathlib/Probability/Process/Predictable.lean
index ace14f8dd8416e..e1cdfeab22dd37 100644
--- a/Mathlib/Probability/Process/Predictable.lean
+++ b/Mathlib/Probability/Process/Predictable.lean
@@ -252,8 +252,7 @@ lemma of_measurable_add_one {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E}
 
 /-- A discrete process `u` is predictable iff `u (n + 1)` is `𝓕 n`-measurable for all `n` and
 `u 0` is `𝓕 0`-measurable. -/
-lemma iff_measurable_add_one
-    {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E} :
+lemma iff_measurable_add_one {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E} :
     IsStronglyPredictable 𝓕 u ↔
     StronglyMeasurable[𝓕 0] (u 0) ∧ ∀ n, StronglyMeasurable[𝓕 n] (u (n + 1)) :=
   ⟨fun h𝓕 ↦ ⟨h𝓕.progMeasurable.stronglyAdapted 0, h𝓕.measurable_add_one⟩,

From 86a3f2e369a59d1e01fd4c6a7ac6044b163859fc Mon Sep 17 00:00:00 2001
From: Joris van Winden <j.vanwinden@student.tudelft.nl>
Date: Mon, 20 Apr 2026 16:03:32 +0200
Subject: [PATCH 10/17] rename progMeasurable to isStronglyProgressive

---
 .../Martingale/OptionalSampling.lean          |  4 +-
 Mathlib/Probability/Process/Adapted.lean      | 80 ++++++++++---------
 Mathlib/Probability/Process/Predictable.lean  | 10 +--
 Mathlib/Probability/Process/Stopping.lean     | 45 ++++++-----
 4 files changed, 73 insertions(+), 66 deletions(-)

diff --git a/Mathlib/Probability/Martingale/OptionalSampling.lean b/Mathlib/Probability/Martingale/OptionalSampling.lean
index 06b2a90e3cdc2c..0c00d1562a9576 100644
--- a/Mathlib/Probability/Martingale/OptionalSampling.lean
+++ b/Mathlib/Probability/Martingale/OptionalSampling.lean
@@ -183,7 +183,7 @@ theorem condExp_stoppedValue_stopping_time_ae_eq_restrict_le (h : Martingale f 
       exact ht.2
     · refine StronglyMeasurable.indicator ?_ (hτ.measurableSet_le_stopping_time hσ)
       refine Measurable.stronglyMeasurable ?_
-      exact measurable_stoppedValue h.stronglyAdapted.progMeasurable_of_discrete hτ
+      exact measurable_stoppedValue h.stronglyAdapted.isStronglyProgressive_of_discrete hτ
     · intro x hx
       simp only [hx, Set.indicator_of_notMem, not_false_iff]
   exact condExp_of_aestronglyMeasurable' hσ.measurableSpace_le h_meas h_int
@@ -215,7 +215,7 @@ theorem stoppedValue_min_ae_eq_condExp [SigmaFiniteFiltration μ ℱ] (h : Marti
     · have h1 : μ[stoppedValue f τ | hτ.measurableSpace] = stoppedValue f τ := by
         apply condExp_of_stronglyMeasurable hτ.measurableSpace_le
         · exact Measurable.stronglyMeasurable <|
-            measurable_stoppedValue h.stronglyAdapted.progMeasurable_of_discrete hτ
+            measurable_stoppedValue h.stronglyAdapted.isStronglyProgressive_of_discrete hτ
         · exact integrable_stoppedValue ι hτ h.integrable hτ_le
       rw [h1]
       exact (condExp_stoppedValue_stopping_time_ae_eq_restrict_le h hτ hσ hτ_le).symm
diff --git a/Mathlib/Probability/Process/Adapted.lean b/Mathlib/Probability/Process/Adapted.lean
index 5ecaabab0014c0..015993319cb776 100644
--- a/Mathlib/Probability/Process/Adapted.lean
+++ b/Mathlib/Probability/Process/Adapted.lean
@@ -12,7 +12,7 @@ public import Mathlib.Topology.Instances.Discrete
 # Adapted and progressively measurable processes
 
 This file defines the related notions of a process `u` being `Adapted`, `StronglyAdapted`
-or `ProgMeasurable` (progressively measurable) with respect to a filter `f`, and proves
+or `StronglyProgressive` (progressively measurable) with respect to a filter `f`, and proves
 some basic facts about them.
 
 ## Main definitions
@@ -21,14 +21,14 @@ some basic facts about them.
   filtration `f` if at each point in time `i`, `u i` is `f i`-measurable
 * `MeasureTheory.StronglyAdapted`: a sequence of functions `u` is said to be strongly adapted to a
   filtration `f` if at each point in time `i`, `u i` is `f i`-strongly measurable
-* `MeasureTheory.ProgMeasurable`: a sequence of functions `u` is said to be progressively
+* `MeasureTheory.IsStronglyProgressive`: a sequence of functions `u` is said to be progressively
   measurable with respect to a filtration `f` if at each point in time `i`, `u` restricted to
   `Set.Iic i × Ω` is strongly measurable with respect to the product `MeasurableSpace` structure
   where the σ-algebra used for `Ω` is `f i`.
 
 ## Main results
 
-* `StronglyAdapted.progMeasurable_of_continuous`: a continuous strongly adapted process is
+* `StronglyAdapted.isStronglyProgressive_of_continuous`: a continuous strongly adapted process is
   progressively measurable.
 
 ## Tags
@@ -186,18 +186,18 @@ measurable with respect to a filtration `f` if at each point in time `i`, `u` re
 σ-algebra used for `Ω` is `f i`.
 The usual definition uses the interval `[0,i]`, which we replace by `Set.Iic i`. We recover the
 usual definition for index types `ℝ≥0` or `ℕ`. -/
-def ProgMeasurable [MeasurableSpace ι] (f : Filtration ι m) (u : ι → Ω → β) : Prop :=
+def IsStronglyProgressive [MeasurableSpace ι] (f : Filtration ι m) (u : ι → Ω → β) : Prop :=
   ∀ i, StronglyMeasurable[Subtype.instMeasurableSpace.prod (f i)] fun p : Set.Iic i × Ω => u p.1 p.2
 
-theorem progMeasurable_const [MeasurableSpace ι] (f : Filtration ι m) (b : β) :
-    ProgMeasurable f (fun _ _ => b : ι → Ω → β) := fun i =>
+theorem isStronglyProgressive_const [MeasurableSpace ι] (f : Filtration ι m) (b : β) :
+    IsStronglyProgressive f (fun _ _ => b : ι → Ω → β) := fun i =>
   @stronglyMeasurable_const _ _ (Subtype.instMeasurableSpace.prod (f i)) _ _
 
-namespace ProgMeasurable
+namespace IsStronglyProgressive
 
 variable [MeasurableSpace ι]
 
-protected theorem stronglyAdapted (h : ProgMeasurable f u) : StronglyAdapted f u := by
+protected theorem stronglyAdapted (h : IsStronglyProgressive f u) : StronglyAdapted f u := by
   intro i
   have : u i = (fun p : Set.Iic i × Ω => u p.1 p.2) ∘ fun x => (⟨i, Set.mem_Iic.mpr le_rfl⟩, x) :=
     rfl
@@ -205,8 +205,8 @@ protected theorem stronglyAdapted (h : ProgMeasurable f u) : StronglyAdapted f u
   exact (h i).comp_measurable measurable_prodMk_left
 
 protected theorem comp {t : ι → Ω → ι} [TopologicalSpace ι] [BorelSpace ι] [PseudoMetrizableSpace ι]
-    (h : ProgMeasurable f u) (ht : ProgMeasurable f t) (ht_le : ∀ i ω, t i ω ≤ i) :
-    ProgMeasurable f fun i ω => u (t i ω) ω := by
+    (h : IsStronglyProgressive f u) (ht : IsStronglyProgressive f t) (ht_le : ∀ i ω, t i ω ≤ i) :
+    IsStronglyProgressive f fun i ω => u (t i ω) ω := by
   intro i
   have : (fun p : ↥(Set.Iic i) × Ω => u (t (p.fst : ι) p.snd) p.snd) =
     (fun p : ↥(Set.Iic i) × Ω => u (p.fst : ι) p.snd) ∘ fun p : ↥(Set.Iic i) × Ω =>
@@ -217,68 +217,72 @@ protected theorem comp {t : ι → Ω → ι} [TopologicalSpace ι] [BorelSpace
 section Arithmetic
 
 @[to_additive]
-protected theorem mul [Mul β] [ContinuousMul β] (hu : ProgMeasurable f u)
-    (hv : ProgMeasurable f v) : ProgMeasurable f fun i ω => u i ω * v i ω := fun i =>
+protected theorem mul [Mul β] [ContinuousMul β] (hu : IsStronglyProgressive f u)
+    (hv : IsStronglyProgressive f v) : IsStronglyProgressive f fun i ω => u i ω * v i ω := fun i =>
   (hu i).mul (hv i)
 
 @[to_additive]
 protected theorem finset_prod' {γ} [CommMonoid β] [ContinuousMul β] {U : γ → ι → Ω → β}
-    {s : Finset γ} (h : ∀ c ∈ s, ProgMeasurable f (U c)) : ProgMeasurable f (∏ c ∈ s, U c) :=
-  Finset.prod_induction U (ProgMeasurable f) (fun _ _ => ProgMeasurable.mul)
-    (progMeasurable_const _ 1) h
+    {s : Finset γ} (h : ∀ c ∈ s, IsStronglyProgressive f (U c)) :
+    IsStronglyProgressive f (∏ c ∈ s, U c) :=
+  Finset.prod_induction U (IsStronglyProgressive f) (fun _ _ => .mul)
+    (isStronglyProgressive_const _ 1) h
 
 @[to_additive]
 protected theorem finset_prod {γ} [CommMonoid β] [ContinuousMul β] {U : γ → ι → Ω → β}
-    {s : Finset γ} (h : ∀ c ∈ s, ProgMeasurable f (U c)) :
-    ProgMeasurable f fun i a => ∏ c ∈ s, U c i a := by
-  convert ProgMeasurable.finset_prod' h using 1; ext (i a); simp only [Finset.prod_apply]
+    {s : Finset γ} (h : ∀ c ∈ s, IsStronglyProgressive f (U c)) :
+    IsStronglyProgressive f fun i a => ∏ c ∈ s, U c i a := by
+  convert IsStronglyProgressive.finset_prod' h using 1; ext (i a); simp only [Finset.prod_apply]
 
 @[to_additive]
-protected theorem inv [Group β] [ContinuousInv β] (hu : ProgMeasurable f u) :
-    ProgMeasurable f fun i ω => (u i ω)⁻¹ := fun i => (hu i).inv
+protected theorem inv [Group β] [ContinuousInv β] (hu : IsStronglyProgressive f u) :
+    IsStronglyProgressive f fun i ω => (u i ω)⁻¹ := fun i => (hu i).inv
 
 @[to_additive sub]
-protected theorem div' [Group β] [ContinuousDiv β] (hu : ProgMeasurable f u)
-    (hv : ProgMeasurable f v) : ProgMeasurable f fun i ω => u i ω / v i ω := fun i =>
+protected theorem div' [Group β] [ContinuousDiv β] (hu : IsStronglyProgressive f u)
+    (hv : IsStronglyProgressive f v) : IsStronglyProgressive f fun i ω => u i ω / v i ω := fun i =>
   (hu i).div' (hv i)
 
 /-- The norm of a progressively measurable process is progressively measurable. -/
 protected lemma norm {β : Type*} {u : ι → Ω → β} [SeminormedAddCommGroup β]
-    (hu : ProgMeasurable f u) :
-    ProgMeasurable f fun t ω ↦ ‖u t ω‖ := fun t ↦ (hu t).norm
+    (hu : IsStronglyProgressive f u) :
+    IsStronglyProgressive f fun t ω ↦ ‖u t ω‖ := fun t ↦ (hu t).norm
 
 end Arithmetic
 
-end ProgMeasurable
+end IsStronglyProgressive
 
-theorem progMeasurable_of_tendsto' {γ} [MeasurableSpace ι] [PseudoMetrizableSpace β]
+theorem isStronglyProgressive_of_tendsto' {γ} [MeasurableSpace ι] [PseudoMetrizableSpace β]
     (fltr : Filter γ) [fltr.NeBot] [fltr.IsCountablyGenerated] {U : γ → ι → Ω → β}
-    (h : ∀ l, ProgMeasurable f (U l)) (h_tendsto : Tendsto U fltr (𝓝 u)) : ProgMeasurable f u := by
+    (h : ∀ l, IsStronglyProgressive f (U l)) (h_tendsto : Tendsto U fltr (𝓝 u)) :
+    IsStronglyProgressive f u := by
   intro i
   apply @stronglyMeasurable_of_tendsto (Set.Iic i × Ω) β γ
     (MeasurableSpace.prod _ (f i)) _ _ fltr _ _ _ _ fun l => h l i
   rw [tendsto_pi_nhds] at h_tendsto ⊢
   exact fun _ ↦ Tendsto.apply_nhds (h_tendsto _) _
 
-theorem progMeasurable_of_tendsto [MeasurableSpace ι] [PseudoMetrizableSpace β] {U : ℕ → ι → Ω → β}
-    (h : ∀ l, ProgMeasurable f (U l)) (h_tendsto : Tendsto U atTop (𝓝 u)) : ProgMeasurable f u :=
-  progMeasurable_of_tendsto' atTop h h_tendsto
+theorem isStronglyProgressive_of_tendsto [MeasurableSpace ι] [PseudoMetrizableSpace β]
+    {U : ℕ → ι → Ω → β} (h : ∀ l, IsStronglyProgressive f (U l))
+    (h_tendsto : Tendsto U atTop (𝓝 u)) : IsStronglyProgressive f u :=
+  isStronglyProgressive_of_tendsto' atTop h h_tendsto
 
 /-- A continuous and strongly adapted process is progressively measurable. -/
-theorem StronglyAdapted.progMeasurable_of_continuous [TopologicalSpace ι] [MetrizableSpace ι]
+theorem StronglyAdapted.isStronglyProgressive_of_continuous [TopologicalSpace ι] [MetrizableSpace ι]
     [SecondCountableTopology ι] [MeasurableSpace ι] [OpensMeasurableSpace ι]
     [PseudoMetrizableSpace β] (h : StronglyAdapted f u) (hu_cont : ∀ ω, Continuous fun i => u i ω) :
-    ProgMeasurable f u := fun i =>
+    IsStronglyProgressive f u := fun i =>
   @stronglyMeasurable_uncurry_of_continuous_of_stronglyMeasurable _ _ (Set.Iic i) _ _ _ _ _ _ _
     (f i) _ (fun ω => (hu_cont ω).comp continuous_induced_dom) fun j => (h j).mono (f.mono j.prop)
 
-/-- For filtrations indexed by a discrete order, `StronglyAdapted` and `ProgMeasurable` are
-equivalent. This lemma provides `StronglyAdapted f u → ProgMeasurable f u`.
-See `ProgMeasurable.stronglyAdapted` for the reverse direction, which is true more generally. -/
-theorem StronglyAdapted.progMeasurable_of_discrete [TopologicalSpace ι] [DiscreteTopology ι]
+/-- For filtrations indexed by a discrete order, `StronglyAdapted` and `IsStronglyProgressive` are
+equivalent. This lemma provides `StronglyAdapted f u → IsStronglyProgressive f u`.
+See `IsStronglyProgressive.stronglyAdapted` for the reverse direction, which is true more generally.
+-/
+theorem StronglyAdapted.isStronglyProgressive_of_discrete [TopologicalSpace ι] [DiscreteTopology ι]
     [SecondCountableTopology ι] [MeasurableSpace ι] [OpensMeasurableSpace ι]
-    [PseudoMetrizableSpace β] (h : StronglyAdapted f u) : ProgMeasurable f u :=
-  h.progMeasurable_of_continuous fun _ => continuous_of_discreteTopology
+    [PseudoMetrizableSpace β] (h : StronglyAdapted f u) : IsStronglyProgressive f u :=
+  h.isStronglyProgressive_of_continuous fun _ => continuous_of_discreteTopology
 
 -- this dot notation will make more sense once we have a more general definition for predictable
 theorem Predictable.stronglyAdapted {f : Filtration ℕ m} {u : ℕ → Ω → β}
diff --git a/Mathlib/Probability/Process/Predictable.lean b/Mathlib/Probability/Process/Predictable.lean
index e1cdfeab22dd37..3e989be9e7617f 100644
--- a/Mathlib/Probability/Process/Predictable.lean
+++ b/Mathlib/Probability/Process/Predictable.lean
@@ -22,7 +22,7 @@ and adapted. We also give an equivalent characterization of predictability for d
 
 ## Main results
 
-* `IsStronglyPredictable.progMeasurable` : A predictable process is progressively measurable.
+* `IsStronglyPredictable.isStronglyProgressive` : A predictable process is progressively measurable.
 * `IsStronglyPredictable.iff_measurable_add_one` : `u` is a discrete predictable process iff
   `u (n + 1)` is `𝓕 n`-measurable and `u 0` is `𝓕 0`-measurable.
 
@@ -171,8 +171,8 @@ variable [LinearOrder ι] [OrderBot ι] [MeasurableSpace ι] [TopologicalSpace 
     [OpensMeasurableSpace ι] [OrderClosedTopology ι]
 
 /-- A predictable process is progressively measurable. -/
-lemma progMeasurable {𝓕 : Filtration ι m} {u : ι → Ω → E} (h𝓕 : IsStronglyPredictable 𝓕 u) :
-    ProgMeasurable 𝓕 u := by
+lemma isStronglyProgressive {𝓕 : Filtration ι m} {u : ι → Ω → E} (h𝓕 : IsStronglyPredictable 𝓕 u) :
+    IsStronglyProgressive 𝓕 u := by
   intro i
   letI : MeasurableSpace (ι × Ω) := 𝓕.predictable
   letI : MeasurableSpace (Set.Iic i × Ω) := Subtype.instMeasurableSpace.prod (𝓕 i)
@@ -185,7 +185,7 @@ lemma progMeasurable {𝓕 : Filtration ι m} {u : ι → Ω → E} (h𝓕 : IsS
 /-- A predictable process is adapted. -/
 lemma stronglyAdapted {𝓕 : Filtration ι m} {u : ι → Ω → E} (h𝓕 : IsStronglyPredictable 𝓕 u) :
     StronglyAdapted 𝓕 u :=
-  h𝓕.progMeasurable.stronglyAdapted
+  h𝓕.isStronglyProgressive.stronglyAdapted
 
 section Discrete
 
@@ -255,7 +255,7 @@ lemma of_measurable_add_one {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E}
 lemma iff_measurable_add_one {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E} :
     IsStronglyPredictable 𝓕 u ↔
     StronglyMeasurable[𝓕 0] (u 0) ∧ ∀ n, StronglyMeasurable[𝓕 n] (u (n + 1)) :=
-  ⟨fun h𝓕 ↦ ⟨h𝓕.progMeasurable.stronglyAdapted 0, h𝓕.measurable_add_one⟩,
+  ⟨fun h𝓕 ↦ ⟨h𝓕.isStronglyProgressive.stronglyAdapted 0, h𝓕.measurable_add_one⟩,
     fun h ↦ .of_measurable_add_one h.1 h.2⟩
 
 end Discrete
diff --git a/Mathlib/Probability/Process/Stopping.lean b/Mathlib/Probability/Process/Stopping.lean
index c9867fda5e07bc..100eea048692b5 100644
--- a/Mathlib/Probability/Process/Stopping.lean
+++ b/Mathlib/Probability/Process/Stopping.lean
@@ -23,8 +23,8 @@ Definition and properties of stopping times.
 
 ## Main results
 
-* `ProgMeasurable.stoppedProcess`: the stopped process of a progressively measurable process is
-  progressively measurable.
+* `IsStronglyProgressive.stoppedProcess`: the stopped process of a progressively measurable process
+  is progressively measurable.
 * `memLp_stoppedProcess`: if a process belongs to `ℒp` at every time in `ℕ`, then its stopped
   process belongs to `ℒp` as well.
 
@@ -870,13 +870,14 @@ theorem stoppedProcess_stoppedProcess_of_le_right (h : σ ≤ τ) :
 theorem stoppedProcess_stoppedProcess_of_le_left (h : τ ≤ σ) :
     stoppedProcess (stoppedProcess u τ) σ = stoppedProcess u τ := by simp [h]
 
-section ProgMeasurable
+section Progressive
 
 variable [MeasurableSpace ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι]
   [BorelSpace ι] [TopologicalSpace β] {f : Filtration ι m}
 
-theorem progMeasurable_min_stopping_time [PseudoMetrizableSpace ι] (hτ : IsStoppingTime f τ) :
-    ProgMeasurable f fun i ω ↦ (min (i : WithTop ι) (τ ω)).untopA := by
+theorem isStronglyProgressive_min_stopping_time [PseudoMetrizableSpace ι]
+    (hτ : IsStoppingTime f τ) :
+    IsStronglyProgressive f fun i ω ↦ (min (i : WithTop ι) (τ ω)).untopA := by
   refine fun i ↦ (Measurable.untopA ?_).stronglyMeasurable
   let m_prod : MeasurableSpace (Set.Iic i × Ω) := Subtype.instMeasurableSpace.prod (f i)
   let m_set : ∀ t : Set (Set.Iic i × Ω), MeasurableSpace t := fun _ =>
@@ -920,9 +921,10 @@ theorem progMeasurable_min_stopping_time [PseudoMetrizableSpace ι] (hτ : IsSto
       simp only [sc, s, not_le, Set.mem_compl_iff, Set.mem_setOf_eq, ← ht]
       norm_cast
 
-theorem ProgMeasurable.stoppedProcess [PseudoMetrizableSpace ι] (h : ProgMeasurable f u)
-    (hτ : IsStoppingTime f τ) : ProgMeasurable f (stoppedProcess u τ) := by
-  have h_meas := progMeasurable_min_stopping_time hτ
+theorem IsStronglyProgressive.stoppedProcess [PseudoMetrizableSpace ι]
+    (h : IsStronglyProgressive f u) (hτ : IsStoppingTime f τ) :
+    IsStronglyProgressive f (stoppedProcess u τ) := by
+  have h_meas := isStronglyProgressive_min_stopping_time hτ
   refine h.comp h_meas fun i ω ↦ ?_
   cases τ ω with
   | top => simp
@@ -931,18 +933,19 @@ theorem ProgMeasurable.stoppedProcess [PseudoMetrizableSpace ι] (h : ProgMeasur
     · simp [(mod_cast h_it : (i : WithTop ι) ≤ t)]
     · simpa [(mod_cast h_ti : t ≤ (i : WithTop ι))]
 
-theorem ProgMeasurable.stronglyAdapted_stoppedProcess [PseudoMetrizableSpace ι]
-    (h : ProgMeasurable f u) (hτ : IsStoppingTime f τ) :
+theorem IsStronglyProgressive.stronglyAdapted_stoppedProcess [PseudoMetrizableSpace ι]
+    (h : IsStronglyProgressive f u) (hτ : IsStoppingTime f τ) :
     StronglyAdapted f (MeasureTheory.stoppedProcess u τ) :=
   (h.stoppedProcess hτ).stronglyAdapted
 
-theorem ProgMeasurable.stronglyMeasurable_stoppedProcess [PseudoMetrizableSpace ι]
-    (hu : ProgMeasurable f u) (hτ : IsStoppingTime f τ) (i : ι) :
+theorem IsStronglyProgressive.stronglyMeasurable_stoppedProcess [PseudoMetrizableSpace ι]
+    (hu : IsStronglyProgressive f u) (hτ : IsStoppingTime f τ) (i : ι) :
     StronglyMeasurable (MeasureTheory.stoppedProcess u τ i) :=
   (hu.stronglyAdapted_stoppedProcess hτ i).mono (f.le _)
 
-theorem stronglyMeasurable_stoppedValue_of_le (h : ProgMeasurable f u) (hτ : IsStoppingTime f τ)
-    {n : ι} (hτ_le : ∀ ω, τ ω ≤ n) : StronglyMeasurable[f n] (stoppedValue u τ) := by
+theorem stronglyMeasurable_stoppedValue_of_le (h : IsStronglyProgressive f u)
+    (hτ : IsStoppingTime f τ) {n : ι} (hτ_le : ∀ ω, τ ω ≤ n) :
+    StronglyMeasurable[f n] (stoppedValue u τ) := by
   have hτ_le' ω : (τ ω).untopA ≤ n := untopA_le (hτ_le ω)
   have : stoppedValue u τ =
       (fun p : Set.Iic n × Ω => u (↑p.fst) p.snd) ∘ fun ω => (⟨(τ ω).untopA, hτ_le' ω⟩, ω) := by
@@ -954,7 +957,7 @@ theorem stronglyMeasurable_stoppedValue_of_le (h : ProgMeasurable f u) (hτ : Is
 
 lemma measurableSet_preimage_stoppedValue_inter [PseudoMetrizableSpace β] [MeasurableSpace β]
     [BorelSpace β]
-    (hf_prog : ProgMeasurable f u) (hτ : IsStoppingTime f τ)
+    (hf_prog : IsStronglyProgressive f u) (hτ : IsStoppingTime f τ)
     {t : Set β} (ht : MeasurableSet t) (i : ι) :
     MeasurableSet[f i] (stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ i}) := by
   have h_str_meas : ∀ i, StronglyMeasurable[f i] (stoppedValue u fun ω => min (τ ω) i) := fun i =>
@@ -969,7 +972,7 @@ lemma measurableSet_preimage_stoppedValue_inter [PseudoMetrizableSpace β] [Meas
   rw [min_eq_left h]
 
 theorem measurable_stoppedValue [PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β]
-    (hf_prog : ProgMeasurable f u) (hτ : IsStoppingTime f τ) :
+    (hf_prog : IsStronglyProgressive f u) (hτ : IsStoppingTime f τ) :
     Measurable[hτ.measurableSpace] (stoppedValue u τ) := by
   have h_str_meas : ∀ i, StronglyMeasurable[f i] (stoppedValue u fun ω => min (τ ω) i) := fun i =>
     stronglyMeasurable_stoppedValue_of_le hf_prog (hτ.min_const i) fun _ => min_le_right _ _
@@ -1006,7 +1009,7 @@ theorem measurable_stoppedValue [PseudoMetrizableSpace β] [MeasurableSpace β]
     exact (hf_prog.stronglyAdapted (Classical.arbitrary ι)).measurable.mono
       (f.le (Classical.arbitrary ι)) le_rfl
 
-end ProgMeasurable
+end Progressive
 
 end LinearOrder
 
@@ -1187,23 +1190,23 @@ variable [TopologicalSpace β] [PseudoMetrizableSpace β] [Nonempty ι] [LinearO
 theorem StronglyAdapted.stoppedProcess [MetrizableSpace ι] (hu : StronglyAdapted f u)
     (hu_cont : ∀ ω, Continuous fun i => u i ω) (hτ : IsStoppingTime f τ) :
     StronglyAdapted f (stoppedProcess u τ) :=
-  ((hu.progMeasurable_of_continuous hu_cont).stoppedProcess hτ).stronglyAdapted
+  ((hu.isStronglyProgressive_of_continuous hu_cont).stoppedProcess hτ).stronglyAdapted
 
 /-- If the indexing order has the discrete topology, then the stopped process of a strongly adapted
 process is strongly adapted. -/
 theorem StronglyAdapted.stoppedProcess_of_discrete [DiscreteTopology ι] (hu : StronglyAdapted f u)
     (hτ : IsStoppingTime f τ) : StronglyAdapted f (MeasureTheory.stoppedProcess u τ) :=
-  (hu.progMeasurable_of_discrete.stoppedProcess hτ).stronglyAdapted
+  (hu.isStronglyProgressive_of_discrete.stoppedProcess hτ).stronglyAdapted
 
 theorem StronglyAdapted.stronglyMeasurable_stoppedProcess [MetrizableSpace ι]
     (hu : StronglyAdapted f u) (hu_cont : ∀ ω, Continuous fun i => u i ω) (hτ : IsStoppingTime f τ)
     (n : ι) : StronglyMeasurable (MeasureTheory.stoppedProcess u τ n) :=
-  (hu.progMeasurable_of_continuous hu_cont).stronglyMeasurable_stoppedProcess hτ n
+  (hu.isStronglyProgressive_of_continuous hu_cont).stronglyMeasurable_stoppedProcess hτ n
 
 theorem StronglyAdapted.stronglyMeasurable_stoppedProcess_of_discrete [DiscreteTopology ι]
     (hu : StronglyAdapted f u) (hτ : IsStoppingTime f τ) (n : ι) :
     StronglyMeasurable (MeasureTheory.stoppedProcess u τ n) :=
-  hu.progMeasurable_of_discrete.stronglyMeasurable_stoppedProcess hτ n
+  hu.isStronglyProgressive_of_discrete.stronglyMeasurable_stoppedProcess hτ n
 
 end StronglyAdaptedStoppedProcess
 

From e9dd23a62400338ece3fb8c3b73c76dc6713e880 Mon Sep 17 00:00:00 2001
From: Joris van Winden <j.vanwinden@student.tudelft.nl>
Date: Mon, 20 Apr 2026 16:17:19 +0200
Subject: [PATCH 11/17] deprecate old theorem

---
 Mathlib/Probability/Process/Adapted.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Probability/Process/Adapted.lean b/Mathlib/Probability/Process/Adapted.lean
index 015993319cb776..5da2cd5ca11388 100644
--- a/Mathlib/Probability/Process/Adapted.lean
+++ b/Mathlib/Probability/Process/Adapted.lean
@@ -285,6 +285,7 @@ theorem StronglyAdapted.isStronglyProgressive_of_discrete [TopologicalSpace ι]
   h.isStronglyProgressive_of_continuous fun _ => continuous_of_discreteTopology
 
 -- this dot notation will make more sense once we have a more general definition for predictable
+@[deprecated "use `IsStronglyPredictable.stronglyAdapted`" (since := "2026-01-05")]
 theorem Predictable.stronglyAdapted {f : Filtration ℕ m} {u : ℕ → Ω → β}
     (hu : StronglyAdapted f fun n => u (n + 1)) (hu0 : StronglyMeasurable[f 0] (u 0)) :
     StronglyAdapted f u := fun n =>

From 7c3f0b4d87bbed0f3758e35a19aea3c2b090420f Mon Sep 17 00:00:00 2001
From: Joris van Winden <j.vanwinden@student.tudelft.nl>
Date: Mon, 20 Apr 2026 17:12:30 +0200
Subject: [PATCH 12/17] change 'progressively measurable' to 'strongly
 progressive' in comments

---
 Mathlib/Probability/Process/Adapted.lean | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/Mathlib/Probability/Process/Adapted.lean b/Mathlib/Probability/Process/Adapted.lean
index 5da2cd5ca11388..17ef8e0d84c17a 100644
--- a/Mathlib/Probability/Process/Adapted.lean
+++ b/Mathlib/Probability/Process/Adapted.lean
@@ -21,15 +21,15 @@ some basic facts about them.
   filtration `f` if at each point in time `i`, `u i` is `f i`-measurable
 * `MeasureTheory.StronglyAdapted`: a sequence of functions `u` is said to be strongly adapted to a
   filtration `f` if at each point in time `i`, `u i` is `f i`-strongly measurable
-* `MeasureTheory.IsStronglyProgressive`: a sequence of functions `u` is said to be progressively
-  measurable with respect to a filtration `f` if at each point in time `i`, `u` restricted to
+* `MeasureTheory.IsStronglyProgressive`: a sequence of functions `u` is said to be strongly
+  progressive with respect to a filtration `f` if at each point in time `i`, `u` restricted to
   `Set.Iic i × Ω` is strongly measurable with respect to the product `MeasurableSpace` structure
   where the σ-algebra used for `Ω` is `f i`.
 
 ## Main results
 
 * `StronglyAdapted.isStronglyProgressive_of_continuous`: a continuous strongly adapted process is
-  progressively measurable.
+  strongly progressive.
 
 ## Tags
 
@@ -180,10 +180,10 @@ end StronglyAdapted
 
 variable {β : Type*} [TopologicalSpace β] {u v : ι → Ω → β}
 
-/-- Progressively measurable process. A sequence of functions `u` is said to be progressively
-measurable with respect to a filtration `f` if at each point in time `i`, `u` restricted to
-`Set.Iic i × Ω` is measurable with respect to the product `MeasurableSpace` structure where the
-σ-algebra used for `Ω` is `f i`.
+/-- Strongly progressive process. A sequence of functions `u` is said to be strongly
+progressive with respect to a filtration `f` if at each point in time `i`, `u` restricted to
+`Set.Iic i × Ω` is strongly measurable with respect to the product `MeasurableSpace` structure
+where the σ-algebra used for `Ω` is `f i`.
 The usual definition uses the interval `[0,i]`, which we replace by `Set.Iic i`. We recover the
 usual definition for index types `ℝ≥0` or `ℕ`. -/
 def IsStronglyProgressive [MeasurableSpace ι] (f : Filtration ι m) (u : ι → Ω → β) : Prop :=
@@ -243,7 +243,7 @@ protected theorem div' [Group β] [ContinuousDiv β] (hu : IsStronglyProgressive
     (hv : IsStronglyProgressive f v) : IsStronglyProgressive f fun i ω => u i ω / v i ω := fun i =>
   (hu i).div' (hv i)
 
-/-- The norm of a progressively measurable process is progressively measurable. -/
+/-- The norm of a strongly progressive process is strongly progressive. -/
 protected lemma norm {β : Type*} {u : ι → Ω → β} [SeminormedAddCommGroup β]
     (hu : IsStronglyProgressive f u) :
     IsStronglyProgressive f fun t ω ↦ ‖u t ω‖ := fun t ↦ (hu t).norm
@@ -267,7 +267,7 @@ theorem isStronglyProgressive_of_tendsto [MeasurableSpace ι] [PseudoMetrizableS
     (h_tendsto : Tendsto U atTop (𝓝 u)) : IsStronglyProgressive f u :=
   isStronglyProgressive_of_tendsto' atTop h h_tendsto
 
-/-- A continuous and strongly adapted process is progressively measurable. -/
+/-- A continuous and strongly adapted process is strongly progressive. -/
 theorem StronglyAdapted.isStronglyProgressive_of_continuous [TopologicalSpace ι] [MetrizableSpace ι]
     [SecondCountableTopology ι] [MeasurableSpace ι] [OpensMeasurableSpace ι]
     [PseudoMetrizableSpace β] (h : StronglyAdapted f u) (hu_cont : ∀ ω, Continuous fun i => u i ω) :

From 5a16551020fa2140344890bab18b41ec6609c122 Mon Sep 17 00:00:00 2001
From: Joris van Winden <j.vanwinden@student.tudelft.nl>
Date: Mon, 20 Apr 2026 18:20:48 +0200
Subject: [PATCH 13/17] clean up proof

---
 Mathlib/Probability/Process/Predictable.lean | 51 +++++++++-----------
 1 file changed, 24 insertions(+), 27 deletions(-)

diff --git a/Mathlib/Probability/Process/Predictable.lean b/Mathlib/Probability/Process/Predictable.lean
index 3e989be9e7617f..a5b7081ad60daa 100644
--- a/Mathlib/Probability/Process/Predictable.lean
+++ b/Mathlib/Probability/Process/Predictable.lean
@@ -194,13 +194,13 @@ lemma measurable_add_one {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E}
     (h𝓕 : IsStronglyPredictable 𝓕 u) (n : ℕ) : StronglyMeasurable[𝓕 n] (u (n + 1)) := by
   letI : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
   letI : MeasurableSpace Ω := 𝓕 n
-  let X k := (Function.curry (h𝓕.approx k) (n + 1))
-  refine ⟨(fun k ↦ SimpleFunc.mk (X k) ?_ ?_), (fun ω ↦ h𝓕.tendsto_approx ⟨(n + 1), ω⟩)⟩
+  let X m := (Function.curry (h𝓕.approx m) (n + 1))
+  refine ⟨(fun m ↦ SimpleFunc.mk (X m) ?_ ?_), (fun ω ↦ h𝓕.tendsto_approx ⟨(n + 1), ω⟩)⟩
   · intro s
-    rw [(by aesop : X k ⁻¹' {s} = {ω | (n + 1, ω) ∈ h𝓕.approx k ⁻¹' {s}})]
+    rw [(by aesop : X m ⁻¹' {s} = {ω | (n + 1, ω) ∈ h𝓕.approx m ⁻¹' {s}})]
     apply measurableSet_prodMk_add_one_of_predictable
-    apply (h𝓕.approx k).measurableSet_fiber
-  · apply (h𝓕.approx k).finite_range.subset
+    apply (h𝓕.approx m).measurableSet_fiber
+  · apply (h𝓕.approx m).finite_range.subset
     rw [Set.range_subset_iff]
     aesop
 
@@ -214,41 +214,38 @@ lemma of_measurable_add_one {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E}
     | n + 1 => (h n).approx m x.2
   -- second layer of approximation (to ensure the whole process has finite range)
   let Y m (x : ℕ × Ω) := if x.1 ≤ m then X m x else X m ⟨0, x.2⟩
-  use fun m ↦ SimpleFunc.mk (Y m) ?_ ?_
-  · intro ⟨n, ω⟩
-    rw [tendsto_congr' (f₂ := fun m ↦ X m ⟨n, ω⟩)]
-    · rcases n with rfl | k
-      · exact h₀.tendsto_approx ω
-      · exact (h k).tendsto_approx ω
-    · filter_upwards [eventually_ge_atTop n] with m hm using by simp; grind
+  refine ⟨fun m ↦ SimpleFunc.mk (Y m) ?_ ?_, ?_⟩
   · intro s
     rw [(by aesop : Y m ⁻¹' {s} = ⋃ n : ℕ, {n} ×ˢ ((Function.curry (Y m) n) ⁻¹' {s}))]
     refine MeasurableSet.iUnion <| fun n ↦ ?_
-    rcases n with rfl | k
+    rcases n with rfl | n
     · apply measurableSet_predictable_singleton_bot_prod
       letI : MeasurableSpace Ω := 𝓕 0
       exact (h₀.approx m).measurableSet_fiber s
     · apply measurableSet_predictable_singleton_prod
-      by_cases! hmk : k + 1 ≤ m
-      · rw [(by aesop : Function.curry (Y m) (k + 1) = Function.curry (X m) (k + 1))]
-        letI : MeasurableSpace Ω := 𝓕 k
-        exact ((h k).approx m).measurableSet_fiber s
-      · rw [(by aesop : Function.curry (Y m) (k + 1) = Function.curry (X m) 0)]
+      by_cases! hmk : n + 1 ≤ m
+      · rw [(by aesop : Function.curry (Y m) (n + 1) = Function.curry (X m) (n + 1))]
+        letI : MeasurableSpace Ω := 𝓕 n
+        exact ((h n).approx m).measurableSet_fiber s
+      · rw [(by aesop : Function.curry (Y m) (n + 1) = Function.curry (X m) 0)]
         apply 𝓕.mono (i := 0) (by simp)
         letI : MeasurableSpace Ω := 𝓕 0
         exact (h₀.approx m).measurableSet_fiber s
-  · apply Set.Finite.subset (s := ⋃ n ∈ Finset.range (m + 1), Set.range (Function.curry (X m) n))
-    · refine Set.Finite.biUnion' (by aesop) ?_
-      intro k hk
-      rcases k with rfl | k
+  · apply Set.Finite.subset (s := ⋃ k ∈ Finset.range (m + 1), Set.range (Function.curry (X m) k))
+    · refine Set.Finite.biUnion' (by aesop) (fun n hn ↦ ?_)
+      rcases n with rfl | n
       · exact @(h₀.approx m).finite_range
-      · exact @((h k).approx m).finite_range
+      · exact @((h n).approx m).finite_range
     · intro e he
-      obtain ⟨⟨k, ω⟩, he'⟩ := Set.mem_range.mp he
+      obtain ⟨⟨n, ω⟩, hnω⟩ := Set.mem_range.mp he
       simp_rw [Set.mem_iUnion, Set.mem_range]
-      by_cases! h' : k ≤ m
-      · exact ⟨k, by aesop⟩
-      · exact ⟨0, by aesop, ω, by aesop⟩
+      exact ⟨if n ≤ m then n else 0, by aesop, ω, by aesop⟩
+  · intro ⟨n, ω⟩
+    rw [tendsto_congr' (f₂ := fun m ↦ X m ⟨n, ω⟩)]
+    · rcases n with rfl | n
+      · exact h₀.tendsto_approx ω
+      · exact (h n).tendsto_approx ω
+    · filter_upwards [eventually_ge_atTop n] with m hm using by simp; grind
 
 /-- A discrete process `u` is predictable iff `u (n + 1)` is `𝓕 n`-measurable for all `n` and
 `u 0` is `𝓕 0`-measurable. -/

From 519c3b1aaf6d47e8fa95048665f0ae664c632cef Mon Sep 17 00:00:00 2001
From: Joris van Winden <j.vanwinden@student.tudelft.nl>
Date: Mon, 20 Apr 2026 18:36:45 +0200
Subject: [PATCH 14/17] remove usage of deprecated lemma

---
 Mathlib/Probability/Martingale/Centering.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Probability/Martingale/Centering.lean b/Mathlib/Probability/Martingale/Centering.lean
index 1b8e04aa590b63..e0611477a529ed 100644
--- a/Mathlib/Probability/Martingale/Centering.lean
+++ b/Mathlib/Probability/Martingale/Centering.lean
@@ -135,9 +135,9 @@ theorem martingalePart_add_ae_eq [SigmaFiniteFiltration μ ℱ] {f g : ℕ → 
   have hhpred : StronglyAdapted ℱ fun n => h (n + 1) := by
     rw [hh]
     exact stronglyAdapted_predictablePart.sub hg
+  have := (IsStronglyPredictable.of_measurable_add_one (hg0.symm ▸ stronglyMeasurable_zero) hg)
   have hhmgle : Martingale h ℱ μ := hf.sub (martingale_martingalePart
-    (hf.stronglyAdapted.add <| Predictable.stronglyAdapted hg <| hg0.symm ▸ stronglyMeasurable_zero)
-    fun n => (hf.integrable n).add <| hgint n)
+    (hf.stronglyAdapted.add this.stronglyAdapted) fun n => (hf.integrable n).add <| hgint n)
   refine (eventuallyEq_iff_sub.2 ?_).symm
   filter_upwards [hhmgle.eq_zero_of_predictable hhpred n] with ω hω
   unfold h at hω

From 680ef550909fa040724a79619ce38a71bc18c36d Mon Sep 17 00:00:00 2001
From: Joris van Winden <j.vanwinden@student.tudelft.nl>
Date: Fri, 24 Apr 2026 11:36:44 +0200
Subject: [PATCH 15/17] add deprecation notices to Adapted.lean

---
 Mathlib/Probability/Process/Adapted.lean | 53 ++++++++++++++++++++++++
 1 file changed, 53 insertions(+)

diff --git a/Mathlib/Probability/Process/Adapted.lean b/Mathlib/Probability/Process/Adapted.lean
index 17ef8e0d84c17a..17bcfcd92bddd1 100644
--- a/Mathlib/Probability/Process/Adapted.lean
+++ b/Mathlib/Probability/Process/Adapted.lean
@@ -293,4 +293,57 @@ theorem Predictable.stronglyAdapted {f : Filtration ℕ m} {u : ℕ → Ω → 
   | 0 => hu0
   | n + 1 => (hu n).mono (f.mono n.le_succ)
 
+@[deprecated (since := "2026-04-24")] alias ProgMeasurable := IsStronglyProgressive
+
+@[deprecated (since := "2026-04-24")] alias progMeasurable_const := isStronglyProgressive_const
+
+@[deprecated (since := "2026-04-24")]
+alias ProgMeasurable.stronglyAdapted := IsStronglyProgressive.stronglyAdapted
+
+@[deprecated (since := "2026-04-24")] alias ProgMeasurable.comp := IsStronglyProgressive.comp
+
+@[deprecated (since := "2026-04-24")] alias ProgMeasurable.add := IsStronglyProgressive.add
+
+@[to_additive existing, deprecated (since := "2026-04-24")]
+alias ProgMeasurable.mul := IsStronglyProgressive.mul
+
+@[deprecated (since := "2026-04-24")]
+alias ProgMeasurable.finset_sum' := IsStronglyProgressive.finset_sum'
+
+@[to_additive existing, deprecated (since := "2026-04-24")]
+alias ProgMeasurable.finset_prod' := IsStronglyProgressive.finset_prod'
+
+@[deprecated (since := "2026-04-24")]
+alias ProgMeasurable.finset_sum := IsStronglyProgressive.finset_sum
+
+@[to_additive existing, deprecated (since := "2026-04-24")]
+alias ProgMeasurable.finset_prod := IsStronglyProgressive.finset_prod
+
+@[deprecated (since := "2026-04-24")]
+alias ProgMeasurable.neg := IsStronglyProgressive.neg
+
+@[to_additive existing, deprecated (since := "2026-04-24")]
+alias ProgMeasurable.inv := IsStronglyProgressive.inv
+
+@[deprecated (since := "2026-04-24")] alias ProgMeasurable.sub := IsStronglyProgressive.sub
+
+@[to_additive existing ProgMeasurable.sub, deprecated (since := "2026-04-24")]
+alias ProgMeasurable.div' := IsStronglyProgressive.div'
+
+@[deprecated (since := "2026-04-24")] alias ProgMeasurable.norm := IsStronglyProgressive.norm
+
+@[deprecated (since := "2026-04-24")]
+alias progMeasurable_of_tendsto := isStronglyProgressive_of_tendsto
+
+@[deprecated (since := "2026-04-24")]
+alias progMeasurable_of_tendsto' := isStronglyProgressive_of_tendsto'
+
+@[deprecated (since := "2026-04-24")]
+alias StronglyAdapted.progMeasurable_of_continuous :=
+  StronglyAdapted.isStronglyProgressive_of_continuous
+
+@[deprecated (since := "2026-04-24")]
+alias StronglyAdapted.progMeasurable_of_discrete :=
+  StronglyAdapted.isStronglyProgressive_of_discrete
+
 end MeasureTheory

From 3a6c5ef04a59da3494bf5deb7709d5159a5508fc Mon Sep 17 00:00:00 2001
From: Joris van Winden <j.vanwinden@student.tudelft.nl>
Date: Fri, 24 Apr 2026 11:44:16 +0200
Subject: [PATCH 16/17] add deprecation notices to Predictable.lean

---
 Mathlib/Probability/Process/Predictable.lean | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/Mathlib/Probability/Process/Predictable.lean b/Mathlib/Probability/Process/Predictable.lean
index a5b7081ad60daa..44a01b4792914d 100644
--- a/Mathlib/Probability/Process/Predictable.lean
+++ b/Mathlib/Probability/Process/Predictable.lean
@@ -259,4 +259,22 @@ end Discrete
 
 end IsStronglyPredictable
 
+@[deprecated (since := "2026-04-24")]
+alias IsPredictable := IsStronglyPredictable
+
+@[deprecated (since := "2026-04-24")]
+alias IsPredictable.progMeasurable := IsStronglyPredictable.isStronglyProgressive
+
+@[deprecated (since := "2026-04-24")]
+alias IsPredictable.adapted := IsStronglyPredictable.stronglyAdapted
+
+@[deprecated (since := "2026-04-24")]
+alias IsPredictable.measurable_add_one := IsStronglyPredictable.measurable_add_one
+
+@[deprecated (since := "2026-04-24")]
+alias IsPredictable.of_measurable_add_one := IsStronglyPredictable.of_measurable_add_one
+
+@[deprecated (since := "2026-04-24")]
+alias IsPredictable.iff_measurable_add_one := IsStronglyPredictable.iff_measurable_add_one
+
 end MeasureTheory

From 0ec408f8ff0a85cb3b09c770626891ff526c6982 Mon Sep 17 00:00:00 2001
From: Joris van Winden <j.vanwinden@student.tudelft.nl>
Date: Fri, 24 Apr 2026 11:48:12 +0200
Subject: [PATCH 17/17] add deprecation notice to Stopping.lean

---
 Mathlib/Probability/Process/Stopping.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/Mathlib/Probability/Process/Stopping.lean b/Mathlib/Probability/Process/Stopping.lean
index 100eea048692b5..5734d43eab9a86 100644
--- a/Mathlib/Probability/Process/Stopping.lean
+++ b/Mathlib/Probability/Process/Stopping.lean
@@ -921,6 +921,9 @@ theorem isStronglyProgressive_min_stopping_time [PseudoMetrizableSpace ι]
       simp only [sc, s, not_le, Set.mem_compl_iff, Set.mem_setOf_eq, ← ht]
       norm_cast
 
+@[deprecated (since := "2026-04-24")]
+alias progMeasurable_min_stopping_time := isStronglyProgressive_min_stopping_time
+
 theorem IsStronglyProgressive.stoppedProcess [PseudoMetrizableSpace ι]
     (h : IsStronglyProgressive f u) (hτ : IsStoppingTime f τ) :
     IsStronglyProgressive f (stoppedProcess u τ) := by
@@ -933,11 +936,18 @@ theorem IsStronglyProgressive.stoppedProcess [PseudoMetrizableSpace ι]
     · simp [(mod_cast h_it : (i : WithTop ι) ≤ t)]
     · simpa [(mod_cast h_ti : t ≤ (i : WithTop ι))]
 
+@[deprecated (since := "2026-04-24")]
+alias ProgMeasurable.stoppedProcess := IsStronglyProgressive.stoppedProcess
+
 theorem IsStronglyProgressive.stronglyAdapted_stoppedProcess [PseudoMetrizableSpace ι]
     (h : IsStronglyProgressive f u) (hτ : IsStoppingTime f τ) :
     StronglyAdapted f (MeasureTheory.stoppedProcess u τ) :=
   (h.stoppedProcess hτ).stronglyAdapted
 
+@[deprecated (since := "2026-04-24")]
+alias ProgMeasurable.stronglyAdapted_stoppedProcess :=
+  IsStronglyProgressive.stronglyAdapted_stoppedProcess
+
 theorem IsStronglyProgressive.stronglyMeasurable_stoppedProcess [PseudoMetrizableSpace ι]
     (hu : IsStronglyProgressive f u) (hτ : IsStoppingTime f τ) (i : ι) :
     StronglyMeasurable (MeasureTheory.stoppedProcess u τ i) :=