refactor(Probability/Process): rework predictable and progressive processes

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
 

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ω

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

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,33 +180,33 @@ 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
   rw [this]
   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,75 +217,133 @@ 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. -/
+/-- 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
+    [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
+@[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 =>
   match n with
   | 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