Filtrations

This file defines filtrations of a measurable space and σ-finite filtrations.

Main definitions

• MeasureTheory.Filtration: a filtration on a measurable space. That is, a monotone sequence of sub-σ-algebras.
• MeasureTheory.SigmaFiniteFiltration: a filtration f is σ-finite with respect to a measure μ if for all i, μ.trim (f.le i) is σ-finite.
• MeasureTheory.Filtration.natural: the smallest filtration that makes a process adapted. That notion adapted is not defined yet in this file. See MeasureTheory.adapted.

Main results

• MeasureTheory.Filtration.instCompleteLattice: filtrations are a complete lattice.

Tags

filtration, stochastic process

structure MeasureTheory.Filtration {Ω : Type u_1} (ι : Type u_2) [Preorder ι] (m : MeasurableSpace Ω) : Type (max u_1 u_2)

A Filtration on a measurable space Ω with σ-algebra m is a monotone sequence of sub-σ-algebras of m.

• seq : ι → MeasurableSpace Ω

  The sequence of sub-σ-algebras of m

• mono' : Monotone ↑self
• le' (i : ι) : ↑self i ≤ m

instance MeasureTheory.instCoeFunFiltrationForallMeasurableSpace {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] : CoeFun (Filtration ι m) fun (x : Filtration ι m) => ι → MeasurableSpace Ω

Equations

• MeasureTheory.instCoeFunFiltrationForallMeasurableSpace = { coe := fun (f : MeasureTheory.Filtration ι m) => ↑f }

theorem MeasureTheory.Filtration.mono {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {i j : ι} (f : Filtration ι m) (hij : i ≤ j) : ↑f i ≤ ↑f j

theorem MeasureTheory.Filtration.le {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] (f : Filtration ι m) (i : ι) : ↑f i ≤ m

theorem MeasureTheory.Filtration.ext {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {f g : Filtration ι m} (h : ↑f = ↑g) : f = g

theorem MeasureTheory.Filtration.ext_iff {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {f g : Filtration ι m} : f = g ↔ ↑f = ↑g

def MeasureTheory.Filtration.const {Ω : Type u_1} (ι : Type u_3) {m : MeasurableSpace Ω} [Preorder ι] (m' : MeasurableSpace Ω) (hm' : m' ≤ m) : Filtration ι m

The constant filtration which is equal to m for all i : ι.

Equations

• MeasureTheory.Filtration.const ι m' hm' = { seq := fun (x : ι) => m', mono' := ⋯, le' := ⋯ }

@[simp]

theorem MeasureTheory.Filtration.const_apply {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {m' : MeasurableSpace Ω} {hm' : m' ≤ m} (i : ι) : ↑(const ι m' hm') i = m'

instance MeasureTheory.Filtration.instInhabited {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] : Inhabited (Filtration ι m)

Equations

• MeasureTheory.Filtration.instInhabited = { default := MeasureTheory.Filtration.const ι m ⋯ }

instance MeasureTheory.Filtration.instLE {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] : LE (Filtration ι m)

Equations

• MeasureTheory.Filtration.instLE = { le := fun (f g : MeasureTheory.Filtration ι m) => ∀ (i : ι), ↑f i ≤ ↑g i }

instance MeasureTheory.Filtration.instBot {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] : Bot (Filtration ι m)

Equations

• MeasureTheory.Filtration.instBot = { bot := MeasureTheory.Filtration.const ι ⊥ ⋯ }

instance MeasureTheory.Filtration.instTop {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] : Top (Filtration ι m)

Equations

• MeasureTheory.Filtration.instTop = { top := MeasureTheory.Filtration.const ι m ⋯ }

instance MeasureTheory.Filtration.instMax {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] : Max (Filtration ι m)

Equations

• MeasureTheory.Filtration.instMax = { max := fun (f g : MeasureTheory.Filtration ι m) => { seq := fun (i : ι) => ↑f i ⊔ ↑g i, mono' := ⋯, le' := ⋯ } }

theorem MeasureTheory.Filtration.coeFn_sup {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {f g : Filtration ι m} : ↑(f ⊔ g) = ↑f ⊔ ↑g

instance MeasureTheory.Filtration.instMin {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] : Min (Filtration ι m)

Equations

• MeasureTheory.Filtration.instMin = { min := fun (f g : MeasureTheory.Filtration ι m) => { seq := fun (i : ι) => ↑f i ⊓ ↑g i, mono' := ⋯, le' := ⋯ } }

theorem MeasureTheory.Filtration.coeFn_inf {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {f g : Filtration ι m} : ↑(f ⊓ g) = ↑f ⊓ ↑g

instance MeasureTheory.Filtration.instSupSet {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] : SupSet (Filtration ι m)

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.Filtration.sSup_def {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] (s : Set (Filtration ι m)) (i : ι) : ↑(sSup s) i = sSup ((fun (f : Filtration ι m) => ↑f i) '' s)

noncomputable instance MeasureTheory.Filtration.instInfSet {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] : InfSet (Filtration ι m)

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.Filtration.sInf_def {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] (s : Set (Filtration ι m)) (i : ι) : ↑(sInf s) i = if s.Nonempty then sInf ((fun (f : Filtration ι m) => ↑f i) '' s) else m

noncomputable instance MeasureTheory.Filtration.instCompleteLattice {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] : CompleteLattice (Filtration ι m)

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.measurableSet_of_filtration {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {s : Set Ω} {i : ι} (hs : MeasurableSet s) : MeasurableSet s

class MeasureTheory.SigmaFiniteFiltration {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] (μ : Measure Ω) (f : Filtration ι m) : Prop

A measure is σ-finite with respect to filtration if it is σ-finite with respect to all the sub-σ-algebra of the filtration.

• SigmaFinite (i : ι) : MeasureTheory.SigmaFinite (μ.trim ⋯)

instance MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] (μ : Measure Ω) (f : Filtration ι m) [hf : SigmaFiniteFiltration μ f] (i : ι) : SigmaFinite (μ.trim ⋯)

@[instance 100]

instance MeasureTheory.IsFiniteMeasure.sigmaFiniteFiltration {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] (μ : Measure Ω) (f : Filtration ι m) [IsFiniteMeasure μ] : SigmaFiniteFiltration μ f

theorem MeasureTheory.Integrable.uniformIntegrable_condExp_filtration {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {μ : Measure Ω} [IsFiniteMeasure μ] {f : Filtration ι m} {g : Ω → ℝ} (hg : Integrable g μ) : UniformIntegrable (fun (i : ι) => μ[g|↑f i]) 1 μ

Given an integrable function g, the conditional expectations of g with respect to a filtration is uniformly integrable.

@[deprecated MeasureTheory.Integrable.uniformIntegrable_condExp_filtration (since := "2025-01-21")]

theorem MeasureTheory.Integrable.uniformIntegrable_condexp_filtration {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {μ : Measure Ω} [IsFiniteMeasure μ] {f : Filtration ι m} {g : Ω → ℝ} (hg : Integrable g μ) : UniformIntegrable (fun (i : ι) => μ[g|↑f i]) 1 μ

Alias of MeasureTheory.Integrable.uniformIntegrable_condExp_filtration.

---

Given an integrable function g, the conditional expectations of g with respect to a filtration is uniformly integrable.

theorem MeasureTheory.Filtration.condExp_condExp {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f : Ω → E) {μ : Measure Ω} (ℱ : Filtration ι m) {i j : ι} (hij : i ≤ j) [SigmaFinite (μ.trim ⋯)] : μ[μ[f|↑ℱ j]|↑ℱ i] =ᶠ[ae μ] μ[f|↑ℱ i]

def MeasureTheory.filtrationOfSet {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {s : ι → Set Ω} (hsm : ∀ (i : ι), MeasurableSet (s i)) : Filtration ι m

Given a sequence of measurable sets (sₙ), filtrationOfSet is the smallest filtration such that sₙ is measurable with respect to the n-th sub-σ-algebra in filtrationOfSet.

Equations

• MeasureTheory.filtrationOfSet hsm = { seq := fun (i : ι) => MeasurableSpace.generateFrom {t : Set Ω | ∃ j ≤ i, s j = t}, mono' := ⋯, le' := ⋯ }

theorem MeasureTheory.measurableSet_filtrationOfSet {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {s : ι → Set Ω} (hsm : ∀ (i : ι), MeasurableSet (s i)) (i : ι) {j : ι} (hj : j ≤ i) : MeasurableSet (s j)

theorem MeasureTheory.measurableSet_filtrationOfSet' {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {s : ι → Set Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (i : ι) : MeasurableSet (s i)

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

Given a sequence of functions, the natural filtration is the smallest sequence of σ-algebras such that that sequence of functions is measurable with respect to the filtration.

Equations

• MeasureTheory.Filtration.natural u hum = { seq := fun (i : ι) => ⨆ (j : ι), ⨆ (_ : j ≤ i), MeasurableSpace.comap (u j) mβ, mono' := ⋯, le' := ⋯ }

theorem MeasureTheory.Filtration.filtrationOfSet_eq_natural {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [TopologicalSpace.MetrizableSpace β] [mβ : MeasurableSpace β] [BorelSpace β] [Preorder ι] [MulZeroOneClass β] [Nontrivial β] {s : ι → Set Ω} (hsm : ∀ (i : ι), MeasurableSet (s i)) : filtrationOfSet hsm = natural (fun (i : ι) => (s i).indicator fun (x : Ω) => 1) ⋯

noncomputable def MeasureTheory.Filtration.limitProcess {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {E : Type u_4} [Zero E] [TopologicalSpace E] (f : ι → Ω → E) (ℱ : Filtration ι m) (μ : Measure Ω) : Ω → E

Given a process f and a filtration ℱ, if f converges to some g almost everywhere and g is ⨆ n, ℱ n-measurable, then limitProcess f ℱ μ chooses said g, else it returns 0.

This definition is used to phrase the a.e. martingale convergence theorem Submartingale.ae_tendsto_limitProcess where an L¹-bounded submartingale f adapted to ℱ converges to limitProcess f ℱ μ μ-almost everywhere.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.Filtration.stronglyMeasurable_limitProcess {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {E : Type u_4} [Zero E] [TopologicalSpace E] {ℱ : Filtration ι m} {f : ι → Ω → E} {μ : Measure Ω} : StronglyMeasurable (limitProcess f ℱ μ)

theorem MeasureTheory.Filtration.stronglyMeasurable_limit_process' {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {E : Type u_4} [Zero E] [TopologicalSpace E] {ℱ : Filtration ι m} {f : ι → Ω → E} {μ : Measure Ω} : StronglyMeasurable (limitProcess f ℱ μ)

theorem MeasureTheory.Filtration.memLp_limitProcess_of_eLpNorm_bdd {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : Measure Ω} {R : NNReal} {p : ENNReal} {F : Type u_5} [NormedAddCommGroup F] {ℱ : Filtration ℕ m} {f : ℕ → Ω → F} (hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ) (hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R) : MemLp (limitProcess f ℱ μ) p μ

@[deprecated MeasureTheory.Filtration.memLp_limitProcess_of_eLpNorm_bdd (since := "2025-02-21")]

theorem MeasureTheory.Filtration.memℒp_limitProcess_of_eLpNorm_bdd {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : Measure Ω} {R : NNReal} {p : ENNReal} {F : Type u_5} [NormedAddCommGroup F] {ℱ : Filtration ℕ m} {f : ℕ → Ω → F} (hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ) (hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R) : MemLp (limitProcess f ℱ μ) p μ

Alias of MeasureTheory.Filtration.memLp_limitProcess_of_eLpNorm_bdd.

Filtration of the first events

def MeasureTheory.Filtration.piLE {ι : Type u_3} [Preorder ι] {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] : Filtration ι MeasurableSpace.pi

The canonical filtration on the product space Π i, X i, where piLE i consists of measurable sets depending only on coordinates ≤ i.

Equations

• MeasureTheory.Filtration.piLE = { seq := fun (i : ι) => MeasurableSpace.comap (Preorder.restrictLe i) MeasurableSpace.pi, mono' := ⋯, le' := ⋯ }

theorem MeasureTheory.Filtration.piLE_eq_comap_frestrictLe {ι : Type u_3} [Preorder ι] {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] [LocallyFiniteOrderBot ι] (i : ι) : ↑piLE i = MeasurableSpace.comap (Preorder.frestrictLe i) MeasurableSpace.pi

def MeasureTheory.Filtration.piFinset {ι : Type u_4} {X : ι → Type u_5} [(i : ι) → MeasurableSpace (X i)] : Filtration (Finset ι) MeasurableSpace.pi

The filtration of events which only depends on finitely many coordinates on the product space Π i, X i, piFinset s consists of measurable sets depending only on coordinates in s, where s : Finset ι.

Equations

• MeasureTheory.Filtration.piFinset = { seq := fun (s : Finset ι) => MeasurableSpace.comap s.restrict MeasurableSpace.pi, mono' := ⋯, le' := ⋯ }

theorem MeasureTheory.Filtration.piFinset_eq_comap_restrict {ι : Type u_4} {X : ι → Type u_5} [(i : ι) → MeasurableSpace (X i)] (s : Finset ι) : ↑piFinset s = MeasurableSpace.comap (↑s).restrict MeasurableSpace.pi

def MeasureTheory.Filtration.cylinderEventsCompl {Ω : Type u_1} {m : MeasurableSpace Ω} {α : Type u_4} : Filtration (Finset α)ᵒᵈ MeasurableSpace.pi

The exterior σ-algebras of finite sets of α form a cofiltration indexed by Finset α.

Equations

• MeasureTheory.Filtration.cylinderEventsCompl = { seq := fun (Λ : (Finset α)ᵒᵈ) => MeasureTheory.cylinderEvents (↑(OrderDual.ofDual Λ))ᶜ, mono' := ⋯, le' := ⋯ }