diff --git a/Mathlib/Probability/Martingale/Basic.lean b/Mathlib/Probability/Martingale/Basic.lean
index 8eba7015b428fb..a30e56290b0fcd 100644
--- a/Mathlib/Probability/Martingale/Basic.lean
+++ b/Mathlib/Probability/Martingale/Basic.lean
@@ -509,39 +509,28 @@ 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]
+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 : 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
-
-/-- A predictable supermartingale is a.e. less than or equal to its initial state.
+  zero_le_of_predictable hfmgle hf.measurable_add_one n
 
-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 : 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
-
-/-- A predictable martingale is a.e. equal to its initial state.
+  le_zero_of_predictable hfmgle hfadp.measurable_add_one n
 
-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 : IsPredictable 𝒢 f) (n : ℕ) : f n =ᵐ[μ] f 0 :=
-  eq_zero_of_predictable hfmgle (fun _ ↦ (hfadp.measurable_add_one _).stronglyMeasurable) n
+    (hfmgle : Martingale f 𝒢 μ) (hfadp : IsStronglyPredictable 𝒢 f) (n : ℕ) : f n =ᵐ[μ] f 0 :=
+  eq_zero_of_predictable hfmgle hfadp.measurable_add_one n
 
-end IsPredictable
+end IsStronglyPredictable
 
 namespace Submartingale
 
diff --git a/Mathlib/Probability/Martingale/Centering.lean b/Mathlib/Probability/Martingale/Centering.lean
index e46df349b27e39..e5dde9e933ed2e 100644
--- a/Mathlib/Probability/Martingale/Centering.lean
+++ b/Mathlib/Probability/Martingale/Centering.lean
@@ -97,13 +97,13 @@ lemma Submartingale.predictablePart_nonneg [PartialOrder E] [IsOrderedAddMonoid
   filter_upwards [hf.monotone_predictablePart] with ω hω n
   simpa [predictablePart_zero] using hω (Nat.zero_le n)
 
-lemma IsPredictable.predictablePart_eq [SecondCountableTopology E] [MeasurableSpace E]
-    [BorelSpace E] [SigmaFiniteFiltration μ ℱ] (hf : IsPredictable ℱ f)
+lemma IsStronglyPredictable.predictablePart_eq [SecondCountableTopology E] [MeasurableSpace E]
+    [BorelSpace E] [SigmaFiniteFiltration μ ℱ] (hf : IsStronglyPredictable ℱ f)
     (hfint : ∀ n, Integrable (f n) μ) (n : ℕ) :
     predictablePart f ℱ μ n =ᵐ[μ] f n - f 0 := by
   simp only [predictablePart, ← Finset.sum_range_sub]
   exact eventuallyEq_sum fun i hi => (condExp_of_stronglyMeasurable (ℱ.le i)
-    ((hf.measurable_add_one i).stronglyMeasurable.sub (hf.adapted i))
+    ((hf.measurable_add_one i).sub (hf.stronglyAdapted i))
     ((hfint (i + 1)).sub (hfint i))).eventuallyEq
 
 theorem stronglyAdapted_predictablePart :
@@ -112,9 +112,9 @@ theorem stronglyAdapted_predictablePart :
     stronglyMeasurable_condExp.mono (ℱ.mono (Finset.mem_range_succ_iff.mp hin))
 
 lemma isPredictable_predictablePart [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] :
-    IsPredictable ℱ (predictablePart f ℱ μ) :=
-  isPredictable_of_measurable_add_one (by simp [measurable_const'])
-    fun n ↦ (stronglyAdapted_predictablePart n).measurable
+    IsStronglyPredictable ℱ (predictablePart f ℱ μ) :=
+  IsStronglyPredictable.of_measurable_add_one (by measurability)
+    fun n ↦ (stronglyAdapted_predictablePart n)
 
 theorem stronglyAdapted_predictablePart' : StronglyAdapted ℱ fun n => predictablePart f ℱ μ n :=
   fun _ => Finset.stronglyMeasurable_sum _ fun _ hin =>
@@ -147,7 +147,7 @@ lemma Martingale.martingalePart_eq (hf : Martingale f ℱ μ) (n : ℕ) :
   simp [martingalePart, hω]
 
 lemma IsPredictable.martingalePart_eq [SecondCountableTopology E] [MeasurableSpace E]
-    [BorelSpace E] [SigmaFiniteFiltration μ ℱ] (hf : IsPredictable ℱ f)
+    [BorelSpace E] [SigmaFiniteFiltration μ ℱ] (hf : IsStronglyPredictable ℱ f)
     (hfint : ∀ n, Integrable (f n) μ) (n : ℕ) :
     martingalePart f ℱ μ n =ᵐ[μ] f 0 := by
   filter_upwards [hf.predictablePart_eq (μ := μ) hfint n] with ω hω
@@ -222,9 +222,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ω
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 2092a74b9dcae8..459901c30206bf 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,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.ProgMeasurable`: 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.progMeasurable_of_continuous`: a continuous strongly adapted process is
-  progressively measurable.
+* `StronglyAdapted.isStronglyProgressive_of_continuous`: a continuous strongly adapted process is
+  strongly progressive.
 
 ## Tags
 
@@ -180,24 +180,24 @@ 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 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,81 +217,124 @@ 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 finsetProd' {γ} [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
-
-@[deprecated (since := "2026-04-08")]
-protected alias finset_prod' := ProgMeasurable.finsetProd'
+    {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 finsetProd {γ} [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.finsetProd' h using 1; ext (i a); simp only [Finset.prod_apply]
-
-@[deprecated (since := "2026-04-08")]
-protected alias finset_prod := ProgMeasurable.finsetProd
+    {s : Finset γ} (h : ∀ c ∈ s, IsStronglyProgressive f (U c)) :
+    IsStronglyProgressive f fun i a => ∏ c ∈ s, U c i a := by
+  convert IsStronglyProgressive.finsetProd' 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. -/
+/-- The norm of a strongly progressive process is strongly progressive. -/
 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 ι]
+/-- 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 ω) :
-    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
-
--- this dot notation will make more sense once we have a more general definition for predictable
-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 =>
-  match n with
-  | 0 => hu0
-  | n + 1 => (hu n).mono (f.mono n.le_succ)
+    [PseudoMetrizableSpace β] (h : StronglyAdapted f u) : IsStronglyProgressive f u :=
+  h.isStronglyProgressive_of_continuous fun _ => continuous_of_discreteTopology
+
+@[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.finsetSum'
+
+@[to_additive existing, deprecated (since := "2026-04-24")]
+alias ProgMeasurable.finset_prod' := IsStronglyProgressive.finsetProd'
+
+@[deprecated (since := "2026-04-24")]
+alias ProgMeasurable.finset_sum := IsStronglyProgressive.finsetSum
+
+@[to_additive existing, deprecated (since := "2026-04-24")]
+alias ProgMeasurable.finset_prod := IsStronglyProgressive.finsetProd
+
+@[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
diff --git a/Mathlib/Probability/Process/Predictable.lean b/Mathlib/Probability/Process/Predictable.lean
index b6e8240c02f665..77cc5d0db4b418 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.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.
 
 ## Tags
@@ -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 IsPredictable (𝓕 : 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,51 +78,15 @@ lemma measurableSet_predictable_Ioc_prod [LinearOrder ι] [OrderBot ι]
     exact (measurableSet_predictable_Ioi_prod hs).diff
       (measurableSet_predictable_Ioi_prod <| 𝓕.mono hij _ hs)
 
-lemma measurableSpace_le_predictable_of_measurableSet [Preorder ι] [OrderBot ι]
-    {𝓕 : Filtration ι m} {m' : MeasurableSpace (ι × Ω)}
-    (hm'bot : ∀ A, MeasurableSet[𝓕 ⊥] A → MeasurableSet[m'] ({⊥} ×ˢ A))
-    (hm' : ∀ i A, MeasurableSet[𝓕 i] A → MeasurableSet[m'] ((Set.Ioi i) ×ˢ A)) :
-    𝓕.predictable ≤ m' := by
-  refine MeasurableSpace.generateFrom_le ?_
-  rintro - (⟨A, hA, rfl⟩ | ⟨i, A, hA, rfl⟩)
-  · exact hm'bot A hA
-  · exact hm' i A hA
-
-namespace IsPredictable
-
-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𝓕 : IsPredictable 𝓕 u) :
-    ProgMeasurable 𝓕 u := by
-  refine fun i ↦ Measurable.stronglyMeasurable ?_
-  rw [IsPredictable, 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 = ∅)]
-
-/-- A predictable process is adapted. -/
-lemma adapted {𝓕 : Filtration ι m} {u : ι → Ω → E} (h𝓕 : IsPredictable 𝓕 u) :
-    StronglyAdapted 𝓕 u :=
-  h𝓕.progMeasurable.stronglyAdapted
+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
 
-omit [SecondCountableTopology E] in
 lemma measurableSet_prodMk_add_one_of_predictable {𝓕 : Filtration ℕ m} {s : Set (ℕ × Ω)}
     (hs : MeasurableSet[𝓕.predictable] s) (n : ℕ) :
     MeasurableSet[𝓕 n] {ω | (n + 1, ω) ∈ s} := by
@@ -168,50 +123,167 @@ 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𝓕 : IsPredictable 𝓕 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
+lemma measurableSpace_le_predictable_of_measurableSet [Preorder ι] [OrderBot ι]
+    {𝓕 : Filtration ι m} {m' : MeasurableSpace (ι × Ω)}
+    (hm'bot : ∀ A, MeasurableSet[𝓕 ⊥] A → MeasurableSet[m'] ({⊥} ×ˢ A))
+    (hm' : ∀ i A, MeasurableSet[𝓕 i] A → MeasurableSet[m'] ((Set.Ioi i) ×ˢ A)) :
+    𝓕.predictable ≤ m' := by
+  refine MeasurableSpace.generateFrom_le ?_
+  rintro - (⟨A, hA, rfl⟩ | ⟨i, A, hA, rfl⟩)
+  · exact hm'bot A hA
+  · exact hm' i A hA
 
-end IsPredictable
+/-- 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
+end
 
-variable [MetrizableSpace E] [MeasurableSpace E] [BorelSpace E]
+variable [TopologicalSpace 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
+/-- 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
+
+variable [LinearOrder ι] [OrderBot ι] [MeasurableSpace ι] [TopologicalSpace ι]
+    [OpensMeasurableSpace ι] [OrderClosedTopology ι]
+
+/-- A predictable process is progressively measurable. -/
+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)
+  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𝓕.isStronglyProgressive.stronglyAdapted
 
-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
-  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)
+section Discrete
+
+/-- 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 : ℕ) : StronglyMeasurable[𝓕 n] (u (n + 1)) := by
+  letI : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
+  letI : MeasurableSpace Ω := 𝓕 n
+  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 m ⁻¹' {s} = {ω | (n + 1, ω) ∈ h𝓕.approx m ⁻¹' {s}})]
+    apply measurableSet_prodMk_add_one_of_predictable
+    apply (h𝓕.approx m).measurableSet_fiber
+  · apply (h𝓕.approx m).finite_range.subset
+    rw [Set.range_subset_iff]
+    aesop
+
+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
+  -- 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 the whole process has finite range)
+  let Y m (x : ℕ × Ω) := if x.1 ≤ m then X m x else X m ⟨0, x.2⟩
+  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 | 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 : 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 := ⋃ 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 n).approx m).finite_range
+    · intro e he
+      obtain ⟨⟨n, ω⟩, hnω⟩ := Set.mem_range.mp he
+      simp_rw [Set.mem_iUnion, Set.mem_range]
+      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. -/
-lemma isPredictable_iff_measurable_add_one [SecondCountableTopology E]
-    {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E} :
-    IsPredictable 𝓕 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⟩
+lemma iff_measurable_add_one {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E} :
+    IsStronglyPredictable 𝓕 u ↔
+    StronglyMeasurable[𝓕 0] (u 0) ∧ ∀ n, StronglyMeasurable[𝓕 n] (u (n + 1)) :=
+  ⟨fun h𝓕 ↦ ⟨h𝓕.isStronglyProgressive.stronglyAdapted 0, h𝓕.measurable_add_one⟩,
+    fun h ↦ .of_measurable_add_one h.1 h.2⟩
 
-end
+end Discrete
+
+end IsStronglyPredictable
+
+@[deprecated IsStronglyPredictable.stronglyAdapted (since := "2026-01-05")]
+theorem Predictable.stronglyAdapted {β : Type*} [TopologicalSpace β] {f : Filtration ℕ m}
+    {u : ℕ → Ω → β} (hu : StronglyAdapted f fun n => u (n + 1))
+    (hu0 : StronglyMeasurable[f 0] (u 0)) :
+    StronglyAdapted f u := fun n =>
+  match n with
+  | 0 => hu0
+  | n + 1 => (hu n).mono (f.mono n.le_succ)
+
+@[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
diff --git a/Mathlib/Probability/Process/Stopping.lean b/Mathlib/Probability/Process/Stopping.lean
index aaa809864c1d39..749ed011ec5f4a 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,13 @@ 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τ
+@[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
+  have h_meas := isStronglyProgressive_min_stopping_time hτ
   refine h.comp h_meas fun i ω ↦ ?_
   cases τ ω with
   | top => simp
@@ -931,18 +936,26 @@ 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 τ) :
+@[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
 
-theorem ProgMeasurable.stronglyMeasurable_stoppedProcess [PseudoMetrizableSpace ι]
-    (hu : ProgMeasurable f u) (hτ : IsStoppingTime f τ) (i : ι) :
+@[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) :=
   (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 +967,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 +982,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 +1019,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 +1200,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