feat(Probability): add Adapted (leanprover-community#32882)

Add `Adapted` which is a version of `StronglyAdapted` for `Measurable `rather than `StronglyMeasurable`.
Also add theorems which state when one property implies the other and when they are equivalent. 

- [x] depends on: leanprover-community#33063

Co-authored-by: David Ledvinka <dledvinka.ledvinka@mail.utoronto.ca>

Author: DavidLedvinka

Mathlib/Probability/Kernel/Disintegration/Density.lean

@@ -163,8 +163,6 @@ lemma stronglyAdapted_densityProcess (κ : Kernel α (γ × β)) (ν : Kernel α
     StronglyAdapted (countableFiltration γ) (fun n x ↦ densityProcess κ ν n a x s) :=
   fun n ↦ stronglyMeasurable_countableFiltration_densityProcess κ ν n a hs
 
-@[deprecated (since := "2025-12-19")] alias adapted_densityProcess := stronglyAdapted_densityProcess
-
 lemma densityProcess_nonneg (κ : Kernel α (γ × β)) (ν : Kernel α γ) (n : ℕ)
     (a : α) (x : γ) (s : Set β) :
     0 ≤ densityProcess κ ν n a x s :=

Mathlib/Probability/Martingale/BorelCantelli.lean

@@ -57,9 +57,6 @@ theorem StronglyAdapted.isStoppingTime_leastGE (r : ℝ) (hf : StronglyAdapted 
     IsStoppingTime ℱ (leastGE f r) :=
   hittingAfter_isStoppingTime hf measurableSet_Ici
 
-@[deprecated (since := "2025-12-19")]
-alias Adapted.isStoppingTime_leastGE := StronglyAdapted.isStoppingTime_leastGE
-
 /-- The stopped process of `f` above `r` is the process that is equal to `f` until `leastGE f r`
 (the first time `f` passes above `r`), and then is constant afterwards. -/
 noncomputable def stoppedAbove (f : ℕ → Ω → ℝ) (r : ℝ) : ℕ → Ω → ℝ :=
@@ -251,9 +248,6 @@ theorem stronglyAdapted_process (hs : ∀ n, MeasurableSet[ℱ n] (s n)) :
   fun _ => Finset.stronglyMeasurable_sum _ fun _ hk =>
     stronglyMeasurable_one.indicator <| ℱ.mono (Finset.mem_range.1 hk) _ <| hs _
 
-@[deprecated (since := "2025-12-19")]
-alias adapted_process := stronglyAdapted_process
-
 theorem martingalePart_process_ae_eq (ℱ : Filtration ℕ m0) (μ : Measure Ω) (s : ℕ → Set Ω) (n : ℕ) :
     martingalePart (process s) ℱ μ n =
       ∑ k ∈ Finset.range n, ((s (k + 1)).indicator 1 - μ[(s (k + 1)).indicator 1|ℱ k]) := by

Mathlib/Probability/Martingale/Centering.lean

@@ -57,16 +57,10 @@ theorem stronglyAdapted_predictablePart :
   fun _ => Finset.stronglyMeasurable_sum _ fun _ hin =>
     stronglyMeasurable_condExp.mono (ℱ.mono (Finset.mem_range_succ_iff.mp hin))
 
-@[deprecated (since := "2025-12-19")]
-alias adapted_predictablePart := stronglyAdapted_predictablePart
-
 theorem stronglyAdapted_predictablePart' : StronglyAdapted ℱ fun n => predictablePart f ℱ μ n :=
   fun _ => Finset.stronglyMeasurable_sum _ fun _ hin =>
     stronglyMeasurable_condExp.mono (ℱ.mono (Finset.mem_range_le hin))
 
-@[deprecated (since := "2025-12-19")]
-alias adapted_predictablePart' := stronglyAdapted_predictablePart'
-
 /-- Any `ℕ`-indexed stochastic process can be written as the sum of a martingale and a predictable
 process. This is the martingale. See `predictablePart` for the predictable process. -/
 noncomputable def martingalePart {m0 : MeasurableSpace Ω} (f : ℕ → Ω → E) (ℱ : Filtration ℕ m0)
@@ -85,9 +79,6 @@ theorem martingalePart_eq_sum : martingalePart f ℱ μ = fun n =>
 theorem stronglyAdapted_martingalePart (hf : StronglyAdapted ℱ f) :
   StronglyAdapted ℱ (martingalePart f ℱ μ) := hf.sub stronglyAdapted_predictablePart'
 
-@[deprecated (since := "2025-12-19")]
-alias adapted_martingalePart := stronglyAdapted_martingalePart
-
 theorem integrable_martingalePart (hf_int : ∀ n, Integrable (f n) μ) (n : ℕ) :
     Integrable (martingalePart f ℱ μ n) μ := by
   rw [martingalePart_eq_sum]

Mathlib/Probability/Martingale/Upcrossing.lean

@@ -330,23 +330,14 @@ theorem StronglyAdapted.isStoppingTime_crossing (hf : StronglyAdapted ℱ f) :
     refine isStoppingTime_hittingBtwn_isStoppingTime this ?_ measurableSet_Iic hf _
     simp [upperCrossingTime_le]
 
-@[deprecated (since := "2025-12-19")]
-alias Adapted.isStoppingTime_crossing := StronglyAdapted.isStoppingTime_crossing
-
 theorem StronglyAdapted.isStoppingTime_upperCrossingTime (hf : StronglyAdapted ℱ f) :
     IsStoppingTime ℱ (fun ω ↦ (upperCrossingTime a b f N n ω : ℕ)) :=
   hf.isStoppingTime_crossing.1
 
-@[deprecated (since := "2025-12-19")]
-alias Adapted.isStoppingTime_upperCrossingTime := StronglyAdapted.isStoppingTime_upperCrossingTime
-
 theorem StronglyAdapted.isStoppingTime_lowerCrossingTime (hf : StronglyAdapted ℱ f) :
     IsStoppingTime ℱ (fun ω ↦ (lowerCrossingTime a b f N n ω : ℕ)) :=
   hf.isStoppingTime_crossing.2
 
-@[deprecated (since := "2025-12-19")]
-alias Adapted.isStoppingTime_lowerCrossingTime := StronglyAdapted.isStoppingTime_lowerCrossingTime
-
 /-- `upcrossingStrat a b f N n` is 1 if `n` is between a consecutive pair of lower and upper
 crossings and is 0 otherwise. `upcrossingStrat` is shifted by one index so that it is adapted
 rather than predictable. -/
@@ -390,9 +381,6 @@ theorem StronglyAdapted.upcrossingStrat (hf : StronglyAdapted ℱ f) :
   simp_rw [← not_le]
   exact hl.inter hu.compl
 
-@[deprecated (since := "2025-12-19")]
-alias Adapted.upcrossingStrat := StronglyAdapted.upcrossingStrat
-
 theorem Submartingale.sum_upcrossingStrat_mul [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ)
     (a b : ℝ) (N : ℕ) : Submartingale (fun n : ℕ =>
       ∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) ℱ μ :=
@@ -769,9 +757,6 @@ theorem StronglyAdapted.measurable_upcrossingsBefore (hf : StronglyAdapted ℱ f
   simpa only [ENat.some_eq_coe, Nat.cast_lt] using
     hf.isStoppingTime_upperCrossingTime.measurableSet_lt_of_pred N
 
-@[deprecated (since := "2025-12-19")]
-alias Adapted.measurable_upcrossingsBefore := StronglyAdapted.measurable_upcrossingsBefore
-
 theorem StronglyAdapted.integrable_upcrossingsBefore [IsFiniteMeasure μ]
     (hf : StronglyAdapted ℱ f) (hab : a < b) :
     Integrable (fun ω => (upcrossingsBefore a b f N ω : ℝ)) μ :=
@@ -782,9 +767,6 @@ theorem StronglyAdapted.integrable_upcrossingsBefore [IsFiniteMeasure μ]
   ⟨Measurable.aestronglyMeasurable (measurable_from_top.comp (hf.measurable_upcrossingsBefore hab)),
     .of_bounded this⟩
 
-@[deprecated (since := "2025-12-19")]
-alias Adapted.integrable_upcrossingsBefore := StronglyAdapted.integrable_upcrossingsBefore
-
 /-- The number of upcrossings of a realization of a stochastic process (`upcrossings` takes value
 in `ℝ≥0∞` and so is allowed to be `∞`). -/
 noncomputable def upcrossings [Preorder ι] [OrderBot ι] [InfSet ι] (a b : ℝ) (f : ι → Ω → ℝ)
@@ -795,9 +777,6 @@ theorem StronglyAdapted.measurable_upcrossings (hf : StronglyAdapted ℱ f) (hab
     Measurable (upcrossings a b f) :=
   .iSup fun _ => measurable_from_top.comp (hf.measurable_upcrossingsBefore hab)
 
-@[deprecated (since := "2025-12-19")]
-alias Adapted.measurable_upcrossings := StronglyAdapted.measurable_upcrossings
-
 theorem upcrossings_lt_top_iff :
     upcrossings a b f ω < ∞ ↔ ∃ k, ∀ N, upcrossingsBefore a b f N ω ≤ k := by
   have : upcrossings a b f ω < ∞ ↔ ∃ k : ℝ≥0, upcrossings a b f ω ≤ k := by

Mathlib/Probability/Process/Adapted.lean

@@ -11,11 +11,14 @@ public import Mathlib.Topology.Instances.Discrete
 /-!
 # Adapted and progressively measurable processes
 
-This file defines the related notions of a process `u` being `StronglyAdapted` or `ProgMeasurable`
-(progressively measurable) with respect to a filtration `f`, and proves some basic facts about them.
+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
+some basic facts about them.
 
 ## Main definitions
 
+* `MeasureTheory.Adapted`: a sequence of functions `u` is said to be adapted to a
+  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
@@ -44,11 +47,55 @@ namespace MeasureTheory
 
 variable {Ω ι : Type*} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m}
 
+section Adapted
+
+variable {β : ι → Type*} [∀ i, MeasurableSpace (β i)] {u v : (i : ι) → Ω → β i}
+
+/-- A sequence of functions `u` is adapted to a filtration `f` if for all `i`,
+`u i` is `f i`-measurable. -/
+def Adapted (f : Filtration ι m) (u : (i : ι) → Ω → β i) : Prop :=
+  ∀ i : ι, Measurable[f i] (u i)
+
+namespace Adapted
+
+@[to_additive]
+protected theorem mul [∀ i, Mul (β i)] [∀ i, MeasurableMul₂ (β i)]
+    (hu : Adapted f u) (hv : Adapted f v) :
+    Adapted f (u * v) := fun i => (hu i).mul (hv i)
+
+@[to_additive]
+protected theorem div [∀ i, Div (β i)] [∀ i, MeasurableDiv₂ (β i)]
+    (hu : Adapted f u) (hv : Adapted f v) :
+    Adapted f (u / v) := fun i => (hu i).div (hv i)
+
+@[to_additive]
+protected theorem inv [∀ i, Group (β i)] [∀ i, MeasurableInv (β i)] (hu : Adapted f u) :
+    Adapted f u⁻¹ := fun i => (hu i).inv
+
+protected theorem smul {𝕂 : Type*} [MeasurableSpace 𝕂]
+    [∀ i, SMul 𝕂 (β i)] [∀ i, MeasurableSMul 𝕂 (β i)] (c : 𝕂) (hu : Adapted f u) :
+    Adapted f (c • u) := fun i => (hu i).const_smul c
+
+protected theorem measurable {i : ι} (hf : Adapted f u) : Measurable[m] (u i) :=
+  (hf i).mono (f.le i) (by rfl)
+
+theorem measurable_le {i j : ι} (hf : Adapted f u) (hij : i ≤ j) : Measurable[f j] (u i) :=
+  (hf i).mono (f.mono hij) (by rfl)
+
+end Adapted
+
+theorem adapted_const' (f : Filtration ι m) (x : (i : ι) → β i) : Adapted f fun i _ ↦ x i :=
+  fun _ ↦ measurable_const
+
+theorem adapted_const {β : Type*} [MeasurableSpace β] (f : Filtration ι m) (x : β) :
+    Adapted f fun _ _ ↦ x := adapted_const' _ _
+
+end Adapted
+
 section StronglyAdapted
 
 variable {β : ι → Type*} [∀ i, TopologicalSpace (β i)] {u v : (i : ι) → Ω → β i}
 
-
 /-- A sequence of functions `u` is strongly adapted to a filtration `f` if for all `i`,
 `u i` is `f i`-strongly measurable. -/
 def StronglyAdapted (f : Filtration ι m) (u : (i : ι) → Ω → β i) : Prop :=
@@ -82,6 +129,20 @@ theorem stronglyMeasurable_le {i j : ι} (hf : StronglyAdapted f u) (hij : i ≤
 
 end StronglyAdapted
 
+theorem StronglyAdapted.adapted [mΒ : ∀ i, MeasurableSpace (β i)] [∀ i, BorelSpace (β i)]
+    [∀ i, PseudoMetrizableSpace (β i)] (hf : StronglyAdapted f u) :
+    Adapted f u := fun _ ↦ (hf _).measurable
+
+theorem Adapted.stronglyAdapted [mΒ : ∀ i, MeasurableSpace (β i)]
+    [∀ i, OpensMeasurableSpace (β i)] [∀ i, PseudoMetrizableSpace (β i)]
+    [∀ i, SecondCountableTopology (β i)] (hf : Adapted f u) :
+    StronglyAdapted f u := fun _ ↦ (hf _).stronglyMeasurable
+
+theorem stronglyAdapted_iff_adapted [mΒ : ∀ i, MeasurableSpace (β i)]
+    [∀ i, BorelSpace (β i)] [∀ i, PseudoMetrizableSpace (β i)]
+    [∀ i, SecondCountableTopology (β i)] :
+    StronglyAdapted f u ↔ Adapted f u := ⟨fun h ↦ h.adapted, fun h ↦ h.stronglyAdapted⟩
+
 theorem stronglyAdapted_const' (f : Filtration ι m) (x : (i : ι) → β i) :
     StronglyAdapted f fun i _ ↦ x i :=
   fun _ ↦ stronglyMeasurable_const
@@ -218,41 +279,4 @@ theorem Predictable.stronglyAdapted {f : Filtration ℕ m} {u : ℕ → Ω → 
   | 0 => hu0
   | n + 1 => (hu n).mono (f.mono n.le_succ)
 
-section Deprications
-
-@[deprecated (since := "2025-12-19")] alias Adapted := StronglyAdapted
-
-@[deprecated (since := "2025-12-19")] alias Adapted.mul := StronglyAdapted.mul
-
-@[deprecated (since := "2025-12-19")] alias Adapted.div := StronglyAdapted.div
-
-@[deprecated (since := "2025-12-19")] alias Adapted.smul := StronglyAdapted.smul
-
-@[deprecated (since := "2025-12-19")]
-alias Adapted.stronglyMeasurable := StronglyAdapted.stronglyMeasurable
-
-@[deprecated (since := "2025-12-19")] alias adapted_const' := stronglyAdapted_const'
-
-@[deprecated (since := "2025-12-19")] alias adapted_const := stronglyAdapted_const
-
-@[deprecated (since := "2025-12-19")] alias adapted_zero' := stronglyAdapted_zero'
-
-@[deprecated (since := "2025-12-19")] alias adapted_zero := stronglyAdapted_zero
-
-@[deprecated (since := "2025-12-19")]
-alias Filtration.adapted_natural := Filtration.stronglyAdapted_natural
-
-@[deprecated (since := "2025-12-19")] alias ProgMeasurable.adapted := ProgMeasurable.stronglyAdapted
-
-@[deprecated (since := "2025-12-19")]
-alias Adapted.progMeasurable_of_continuous := StronglyAdapted.progMeasurable_of_continuous
-
-@[deprecated (since := "2025-12-19")]
-alias Adapted.progMeasurable_of_discrete := StronglyAdapted.progMeasurable_of_discrete
-
-@[deprecated (since := "2025-12-19")]
-alias Predictable.adapted := Predictable.stronglyAdapted
-
-end Deprications
-
 end MeasureTheory

Mathlib/Probability/Process/Stopping.lean

@@ -869,9 +869,6 @@ theorem ProgMeasurable.stronglyAdapted_stoppedProcess [PseudoMetrizableSpace ι]
     StronglyAdapted f (MeasureTheory.stoppedProcess u τ) :=
   (h.stoppedProcess hτ).stronglyAdapted
 
-@[deprecated (since := "2025-12-19")]
-alias ProgMeasurable.adapted_stoppedProcess := ProgMeasurable.stronglyAdapted_stoppedProcess
-
 theorem ProgMeasurable.stronglyMeasurable_stoppedProcess [PseudoMetrizableSpace ι]
     (hu : ProgMeasurable f u) (hτ : IsStoppingTime f τ) (i : ι) :
     StronglyMeasurable (MeasureTheory.stoppedProcess u τ i) :=
@@ -1125,35 +1122,22 @@ theorem StronglyAdapted.stoppedProcess [MetrizableSpace ι] (hu : StronglyAdapte
     StronglyAdapted f (stoppedProcess u τ) :=
   ((hu.progMeasurable_of_continuous hu_cont).stoppedProcess hτ).stronglyAdapted
 
-@[deprecated (since := "2025-12-19")]
-alias Adapted.stoppedProcess := StronglyAdapted.stoppedProcess
-
 /-- 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
 
-@[deprecated (since := "2025-12-19")]
-alias Adapted.stoppedProcess_of_discrete := StronglyAdapted.stoppedProcess_of_discrete
-
 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
 
-@[deprecated (since := "2025-12-19")]
-alias Adapted.stronglyMeasurable_stoppedProcess := StronglyAdapted.stronglyMeasurable_stoppedProcess
-
 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
 
-@[deprecated (since := "2025-12-19")]
-alias Adapted.stronglyMeasurable_stoppedProcess_of_discrete :=
-  StronglyAdapted.stronglyMeasurable_stoppedProcess_of_discrete
-
 end StronglyAdaptedStoppedProcess
 
 section Nat