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 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 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 progressively measurable.

Tags

adapted, progressively measurable

def MeasureTheory.Adapted {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] (f : Filtration ι m) (u : (i : ι) → Ω → β i) : Prop

A sequence of functions u is adapted to a filtration f if for all i, u i is f i-measurable.

Equations

• MeasureTheory.Adapted f u = ∀ (i : ι), Measurable (u i)

theorem MeasureTheory.Adapted.mul {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] {u v : (i : ι) → Ω → β i} [(i : ι) → Mul (β i)] [∀ (i : ι), MeasurableMul₂ (β i)] (hu : Adapted f u) (hv : Adapted f v) : Adapted f (u * v)

theorem MeasureTheory.Adapted.add {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] {u v : (i : ι) → Ω → β i} [(i : ι) → Add (β i)] [∀ (i : ι), MeasurableAdd₂ (β i)] (hu : Adapted f u) (hv : Adapted f v) : Adapted f (u + v)

theorem MeasureTheory.Adapted.div {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] {u v : (i : ι) → Ω → β i} [(i : ι) → Div (β i)] [∀ (i : ι), MeasurableDiv₂ (β i)] (hu : Adapted f u) (hv : Adapted f v) : Adapted f (u / v)

theorem MeasureTheory.Adapted.sub {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] {u v : (i : ι) → Ω → β i} [(i : ι) → Sub (β i)] [∀ (i : ι), MeasurableSub₂ (β i)] (hu : Adapted f u) (hv : Adapted f v) : Adapted f (u - v)

theorem MeasureTheory.Adapted.inv {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] {u : (i : ι) → Ω → β i} [(i : ι) → Group (β i)] [∀ (i : ι), MeasurableInv (β i)] (hu : Adapted f u) : Adapted f u⁻¹

theorem MeasureTheory.Adapted.neg {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] {u : (i : ι) → Ω → β i} [(i : ι) → AddGroup (β i)] [∀ (i : ι), MeasurableNeg (β i)] (hu : Adapted f u) : Adapted f (-u)

theorem MeasureTheory.Adapted.smul {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] {u : (i : ι) → Ω → β i} {𝕂 : Type u_4} [MeasurableSpace 𝕂] [(i : ι) → SMul 𝕂 (β i)] [∀ (i : ι), MeasurableSMul 𝕂 (β i)] (c : 𝕂) (hu : Adapted f u) : Adapted f (c • u)

theorem MeasureTheory.Adapted.measurable {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] {u : (i : ι) → Ω → β i} {i : ι} (hf : Adapted f u) : Measurable (u i)

theorem MeasureTheory.Adapted.measurable_le {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] {u : (i : ι) → Ω → β i} {i j : ι} (hf : Adapted f u) (hij : i ≤ j) : Measurable (u i)

theorem MeasureTheory.adapted_const' {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] (f : Filtration ι m) (x : (i : ι) → β i) : Adapted f fun (i : ι) (x_1 : Ω) => x i

theorem MeasureTheory.adapted_const {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {β : Type u_4} [MeasurableSpace β] (f : Filtration ι m) (x : β) : Adapted f fun (x_1 : ι) (x_2 : Ω) => x

def MeasureTheory.StronglyAdapted {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {β : ι → Type u_3} [(i : ι) → TopologicalSpace (β i)] (f : Filtration ι m) (u : (i : ι) → Ω → β i) : Prop

A sequence of functions u is strongly adapted to a filtration f if for all i, u i is f i-strongly measurable.

Equations

• MeasureTheory.StronglyAdapted f u = ∀ (i : ι), MeasureTheory.StronglyMeasurable (u i)

theorem MeasureTheory.StronglyAdapted.mul {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : ι → Type u_3} [(i : ι) → TopologicalSpace (β i)] {u v : (i : ι) → Ω → β i} [(i : ι) → Mul (β i)] [∀ (i : ι), ContinuousMul (β i)] (hu : StronglyAdapted f u) (hv : StronglyAdapted f v) : StronglyAdapted f (u * v)

theorem MeasureTheory.StronglyAdapted.add {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : ι → Type u_3} [(i : ι) → TopologicalSpace (β i)] {u v : (i : ι) → Ω → β i} [(i : ι) → Add (β i)] [∀ (i : ι), ContinuousAdd (β i)] (hu : StronglyAdapted f u) (hv : StronglyAdapted f v) : StronglyAdapted f (u + v)

theorem MeasureTheory.StronglyAdapted.div {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : ι → Type u_3} [(i : ι) → TopologicalSpace (β i)] {u v : (i : ι) → Ω → β i} [(i : ι) → Div (β i)] [∀ (i : ι), ContinuousDiv (β i)] (hu : StronglyAdapted f u) (hv : StronglyAdapted f v) : StronglyAdapted f (u / v)

theorem MeasureTheory.StronglyAdapted.sub {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : ι → Type u_3} [(i : ι) → TopologicalSpace (β i)] {u v : (i : ι) → Ω → β i} [(i : ι) → Sub (β i)] [∀ (i : ι), ContinuousSub (β i)] (hu : StronglyAdapted f u) (hv : StronglyAdapted f v) : StronglyAdapted f (u - v)

theorem MeasureTheory.StronglyAdapted.inv {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : ι → Type u_3} [(i : ι) → TopologicalSpace (β i)] {u : (i : ι) → Ω → β i} [(i : ι) → Group (β i)] [∀ (i : ι), ContinuousInv (β i)] (hu : StronglyAdapted f u) : StronglyAdapted f u⁻¹

theorem MeasureTheory.StronglyAdapted.neg {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : ι → Type u_3} [(i : ι) → TopologicalSpace (β i)] {u : (i : ι) → Ω → β i} [(i : ι) → AddGroup (β i)] [∀ (i : ι), ContinuousNeg (β i)] (hu : StronglyAdapted f u) : StronglyAdapted f (-u)

theorem MeasureTheory.StronglyAdapted.smul {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : ι → Type u_3} [(i : ι) → TopologicalSpace (β i)] {u : (i : ι) → Ω → β i} [(i : ι) → SMul ℝ (β i)] [∀ (i : ι), ContinuousConstSMul ℝ (β i)] (c : ℝ) (hu : StronglyAdapted f u) : StronglyAdapted f (c • u)

theorem MeasureTheory.StronglyAdapted.stronglyMeasurable {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : ι → Type u_3} [(i : ι) → TopologicalSpace (β i)] {u : (i : ι) → Ω → β i} {i : ι} (hf : StronglyAdapted f u) : StronglyMeasurable (u i)

theorem MeasureTheory.StronglyAdapted.stronglyMeasurable_le {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : ι → Type u_3} [(i : ι) → TopologicalSpace (β i)] {u : (i : ι) → Ω → β i} {i j : ι} (hf : StronglyAdapted f u) (hij : i ≤ j) : StronglyMeasurable (u i)

theorem MeasureTheory.StronglyAdapted.adapted {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : ι → Type u_3} [(i : ι) → TopologicalSpace (β i)] {u : (i : ι) → Ω → β i} [mΒ : (i : ι) → MeasurableSpace (β i)] [∀ (i : ι), BorelSpace (β i)] [∀ (i : ι), TopologicalSpace.PseudoMetrizableSpace (β i)] (hf : StronglyAdapted f u) : Adapted f u

theorem MeasureTheory.Adapted.stronglyAdapted {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : ι → Type u_3} [(i : ι) → TopologicalSpace (β i)] {u : (i : ι) → Ω → β i} [mΒ : (i : ι) → MeasurableSpace (β i)] [∀ (i : ι), OpensMeasurableSpace (β i)] [∀ (i : ι), TopologicalSpace.PseudoMetrizableSpace (β i)] [∀ (i : ι), SecondCountableTopology (β i)] (hf : Adapted f u) : StronglyAdapted f u

theorem MeasureTheory.stronglyAdapted_iff_adapted {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : ι → Type u_3} [(i : ι) → TopologicalSpace (β i)] {u : (i : ι) → Ω → β i} [mΒ : (i : ι) → MeasurableSpace (β i)] [∀ (i : ι), BorelSpace (β i)] [∀ (i : ι), TopologicalSpace.PseudoMetrizableSpace (β i)] [∀ (i : ι), SecondCountableTopology (β i)] : StronglyAdapted f u ↔ Adapted f u

theorem MeasureTheory.stronglyAdapted_const' {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {β : ι → Type u_3} [(i : ι) → TopologicalSpace (β i)] (f : Filtration ι m) (x : (i : ι) → β i) : StronglyAdapted f fun (i : ι) (x_1 : Ω) => x i

theorem MeasureTheory.stronglyAdapted_const {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {β : Type u_4} [TopologicalSpace β] (f : Filtration ι m) (x : β) : StronglyAdapted f fun (x_1 : ι) (x_2 : Ω) => x

theorem MeasureTheory.stronglyAdapted_zero' {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] (β : ι → Type u_3) [(i : ι) → TopologicalSpace (β i)] [(i : ι) → Zero (β i)] (f : Filtration ι m) : StronglyAdapted f 0

theorem MeasureTheory.stronglyAdapted_zero {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] (β : Type u_4) [TopologicalSpace β] [Zero β] (f : Filtration ι m) : StronglyAdapted f 0

theorem MeasureTheory.Filtration.stronglyAdapted_natural {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {β : ι → Type u_3} [(i : ι) → TopologicalSpace (β i)] {u : (i : ι) → Ω → β i} [∀ (i : ι), TopologicalSpace.MetrizableSpace (β i)] [mβ : (i : ι) → MeasurableSpace (β i)] [∀ (i : ι), BorelSpace (β i)] (hum : ∀ (i : ι), StronglyMeasurable (u i)) : StronglyAdapted (natural u hum) u

def MeasureTheory.ProgMeasurable {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {β : Type u_3} [TopologicalSpace β] [MeasurableSpace ι] (f : Filtration ι m) (u : ι → Ω → β) : Prop

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. 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 ℕ.

Equations

• MeasureTheory.ProgMeasurable f u = ∀ (i : ι), MeasureTheory.StronglyMeasurable fun (p : ↑(Set.Iic i) × Ω) => u (↑p.1) p.2

theorem MeasureTheory.progMeasurable_const {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {β : Type u_3} [TopologicalSpace β] [MeasurableSpace ι] (f : Filtration ι m) (b : β) : ProgMeasurable f fun (x : ι) (x_1 : Ω) => b

theorem MeasureTheory.ProgMeasurable.stronglyAdapted {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : Type u_3} [TopologicalSpace β] {u : ι → Ω → β} [MeasurableSpace ι] (h : ProgMeasurable f u) : StronglyAdapted f u

theorem MeasureTheory.ProgMeasurable.comp {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : Type u_3} [TopologicalSpace β] {u : ι → Ω → β} [MeasurableSpace ι] {t : ι → Ω → ι} [TopologicalSpace ι] [BorelSpace ι] [TopologicalSpace.PseudoMetrizableSpace ι] (h : ProgMeasurable f u) (ht : ProgMeasurable f t) (ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i) : ProgMeasurable f fun (i : ι) (ω : Ω) => u (t i ω) ω

theorem MeasureTheory.ProgMeasurable.mul {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : Type u_3} [TopologicalSpace β] {u v : ι → Ω → β} [MeasurableSpace ι] [Mul β] [ContinuousMul β] (hu : ProgMeasurable f u) (hv : ProgMeasurable f v) : ProgMeasurable f fun (i : ι) (ω : Ω) => u i ω * v i ω

theorem MeasureTheory.ProgMeasurable.add {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : Type u_3} [TopologicalSpace β] {u v : ι → Ω → β} [MeasurableSpace ι] [Add β] [ContinuousAdd β] (hu : ProgMeasurable f u) (hv : ProgMeasurable f v) : ProgMeasurable f fun (i : ι) (ω : Ω) => u i ω + v i ω

theorem MeasureTheory.ProgMeasurable.finset_prod' {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : Type u_3} [TopologicalSpace β] [MeasurableSpace ι] {γ : Type u_4} [CommMonoid β] [ContinuousMul β] {U : γ → ι → Ω → β} {s : Finset γ} (h : ∀ c ∈ s, ProgMeasurable f (U c)) : ProgMeasurable f (∏ c ∈ s, U c)

theorem MeasureTheory.ProgMeasurable.finset_sum' {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : Type u_3} [TopologicalSpace β] [MeasurableSpace ι] {γ : Type u_4} [AddCommMonoid β] [ContinuousAdd β] {U : γ → ι → Ω → β} {s : Finset γ} (h : ∀ c ∈ s, ProgMeasurable f (U c)) : ProgMeasurable f (∑ c ∈ s, U c)

theorem MeasureTheory.ProgMeasurable.finset_prod {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : Type u_3} [TopologicalSpace β] [MeasurableSpace ι] {γ : Type u_4} [CommMonoid β] [ContinuousMul β] {U : γ → ι → Ω → β} {s : Finset γ} (h : ∀ c ∈ s, ProgMeasurable f (U c)) : ProgMeasurable f fun (i : ι) (a : Ω) => ∏ c ∈ s, U c i a

theorem MeasureTheory.ProgMeasurable.finset_sum {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : Type u_3} [TopologicalSpace β] [MeasurableSpace ι] {γ : Type u_4} [AddCommMonoid β] [ContinuousAdd β] {U : γ → ι → Ω → β} {s : Finset γ} (h : ∀ c ∈ s, ProgMeasurable f (U c)) : ProgMeasurable f fun (i : ι) (a : Ω) => ∑ c ∈ s, U c i a

theorem MeasureTheory.ProgMeasurable.inv {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : Type u_3} [TopologicalSpace β] {u : ι → Ω → β} [MeasurableSpace ι] [Group β] [ContinuousInv β] (hu : ProgMeasurable f u) : ProgMeasurable f fun (i : ι) (ω : Ω) => (u i ω)⁻¹

theorem MeasureTheory.ProgMeasurable.neg {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : Type u_3} [TopologicalSpace β] {u : ι → Ω → β} [MeasurableSpace ι] [AddGroup β] [ContinuousNeg β] (hu : ProgMeasurable f u) : ProgMeasurable f fun (i : ι) (ω : Ω) => -u i ω

theorem MeasureTheory.ProgMeasurable.div {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : Type u_3} [TopologicalSpace β] {u v : ι → Ω → β} [MeasurableSpace ι] [Group β] [ContinuousDiv β] (hu : ProgMeasurable f u) (hv : ProgMeasurable f v) : ProgMeasurable f fun (i : ι) (ω : Ω) => u i ω / v i ω

theorem MeasureTheory.ProgMeasurable.sub {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : Type u_3} [TopologicalSpace β] {u v : ι → Ω → β} [MeasurableSpace ι] [AddGroup β] [ContinuousSub β] (hu : ProgMeasurable f u) (hv : ProgMeasurable f v) : ProgMeasurable f fun (i : ι) (ω : Ω) => u i ω - v i ω

theorem MeasureTheory.progMeasurable_of_tendsto' {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : Type u_3} [TopologicalSpace β] {u : ι → Ω → β} {γ : Type u_4} [MeasurableSpace ι] [TopologicalSpace.PseudoMetrizableSpace β] (fltr : Filter γ) [fltr.NeBot] [fltr.IsCountablyGenerated] {U : γ → ι → Ω → β} (h : ∀ (l : γ), ProgMeasurable f (U l)) (h_tendsto : Filter.Tendsto U fltr (nhds u)) : ProgMeasurable f u

theorem MeasureTheory.progMeasurable_of_tendsto {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : Type u_3} [TopologicalSpace β] {u : ι → Ω → β} [MeasurableSpace ι] [TopologicalSpace.PseudoMetrizableSpace β] {U : ℕ → ι → Ω → β} (h : ∀ (l : ℕ), ProgMeasurable f (U l)) (h_tendsto : Filter.Tendsto U Filter.atTop (nhds u)) : ProgMeasurable f u

theorem MeasureTheory.StronglyAdapted.progMeasurable_of_continuous {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : Type u_3} [TopologicalSpace β] {u : ι → Ω → β} [TopologicalSpace ι] [TopologicalSpace.MetrizableSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [OpensMeasurableSpace ι] [TopologicalSpace.PseudoMetrizableSpace β] (h : StronglyAdapted f u) (hu_cont : ∀ (ω : Ω), Continuous fun (i : ι) => u i ω) : ProgMeasurable f u

A continuous and strongly adapted process is progressively measurable.

theorem MeasureTheory.StronglyAdapted.progMeasurable_of_discrete {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {β : Type u_3} [TopologicalSpace β] {u : ι → Ω → β} [TopologicalSpace ι] [DiscreteTopology ι] [SecondCountableTopology ι] [MeasurableSpace ι] [OpensMeasurableSpace ι] [TopologicalSpace.PseudoMetrizableSpace β] (h : StronglyAdapted f u) : ProgMeasurable f u

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 MeasureTheory.Predictable.stronglyAdapted {Ω : Type u_1} {m : MeasurableSpace Ω} {β : Type u_3} [TopologicalSpace β] {f : Filtration ℕ m} {u : ℕ → Ω → β} (hu : StronglyAdapted f fun (n : ℕ) => u (n + 1)) (hu0 : StronglyMeasurable (u 0)) : StronglyAdapted f u