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 Ω
• mono' : Monotone ↑self
• le' : ∀ (i : ι), ↑self i ≤ m

instance MeasureTheory.instCoeFunFiltrationForAllMeasurableSpace {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] : CoeFun (MeasureTheory.Filtration ι m) fun (x : MeasureTheory.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 : MeasureTheory.Filtration ι m) (hij : i ≤ j) : ↑f i ≤ ↑f j

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

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

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

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

Equations

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

@[simp]

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

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

Equations

• MeasureTheory.Filtration.instInhabitedFiltration = { default := MeasureTheory.Filtration.const ι m (_ : m ≤ m) }

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

Equations

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

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

Equations

• MeasureTheory.Filtration.instBotFiltration = { bot := MeasureTheory.Filtration.const ι ⊥ (_ : ⊥ ≤ m) }

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

Equations

• MeasureTheory.Filtration.instTopFiltration = { top := MeasureTheory.Filtration.const ι m (_ : m ≤ m) }

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

Equations

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

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

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

Equations

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

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

instance MeasureTheory.Filtration.instSupSetFiltration {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] : SupSet (MeasureTheory.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 (MeasureTheory.Filtration ι m)) (i : ι) : ↑(sSup s) i = sSup ((fun (f : MeasureTheory.Filtration ι m) => ↑f i) '' s)

noncomputable instance MeasureTheory.Filtration.instInfSetFiltration {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] : InfSet (MeasureTheory.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 (MeasureTheory.Filtration ι m)) (i : ι) : ↑(sInf s) i = if Set.Nonempty s then sInf ((fun (f : MeasureTheory.Filtration ι m) => ↑f i) '' s) else m

noncomputable instance MeasureTheory.Filtration.instCompleteLattice {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] : CompleteLattice (MeasureTheory.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 : MeasureTheory.Filtration ι m} {s : Set Ω} {i : ι} (hs : MeasurableSet s) : MeasurableSet s

class MeasureTheory.SigmaFiniteFiltration {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] (μ : MeasureTheory.Measure Ω) (f : MeasureTheory.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 (MeasureTheory.Measure.trim μ (_ : ↑f i ≤ m))

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

Equations

• (_ : MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ (_ : ↑f i ≤ m))) = (_ : MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ (_ : ↑f i ≤ m)))

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

Equations

• (_ : MeasureTheory.SigmaFiniteFiltration μ f) = (_ : MeasureTheory.SigmaFiniteFiltration μ f)

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

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

def MeasureTheory.filtrationOfSet {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {s : ι → Set Ω} (hsm : ∀ (i : ι), MeasurableSet (s i)) : MeasureTheory.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

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

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 : ι), MeasureTheory.StronglyMeasurable (u i)) : MeasureTheory.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

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

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)) : MeasureTheory.filtrationOfSet hsm = MeasureTheory.Filtration.natural (fun (i : ι) => Set.indicator (s i) fun (x : Ω) => 1) (_ : ∀ (i : ι), MeasureTheory.StronglyMeasurable (Set.indicator (s i) 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) (ℱ : MeasureTheory.Filtration ι m) (μ : MeasureTheory.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] {ℱ : MeasureTheory.Filtration ι m} {f : ι → Ω → E} {μ : MeasureTheory.Measure Ω} : MeasureTheory.StronglyMeasurable (MeasureTheory.Filtration.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] {ℱ : MeasureTheory.Filtration ι m} {f : ι → Ω → E} {μ : MeasureTheory.Measure Ω} : MeasureTheory.StronglyMeasurable (MeasureTheory.Filtration.limitProcess f ℱ μ)

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