# Documentation

Mathlib.Probability.Process.Filtration

# 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) [] (m : ) :
Type (max u_1 u_2)
• seq : ι
• mono' : Monotone s
• le' : ∀ (i : ι), s i m

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

Instances For
instance MeasureTheory.instCoeFunFiltrationForAllMeasurableSpace {Ω : Type u_1} {ι : Type u_3} {m : } [] :
CoeFun () fun x => ι
theorem MeasureTheory.Filtration.mono {Ω : Type u_1} {ι : Type u_3} {m : } [] {i : ι} {j : ι} (f : ) (hij : i j) :
f i f j
theorem MeasureTheory.Filtration.le {Ω : Type u_1} {ι : Type u_3} {m : } [] (f : ) (i : ι) :
f i m
theorem MeasureTheory.Filtration.ext {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {g : } (h : f = g) :
f = g
def MeasureTheory.Filtration.const {Ω : Type u_1} (ι : Type u_3) {m : } [] (m' : ) (hm' : m' m) :

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

Instances For
@[simp]
theorem MeasureTheory.Filtration.const_apply {Ω : Type u_1} {ι : Type u_3} {m : } [] {m' : } {hm' : m' m} (i : ι) :
↑() i = m'
instance MeasureTheory.Filtration.instInhabitedFiltration {Ω : Type u_1} {ι : Type u_3} {m : } [] :
instance MeasureTheory.Filtration.instLEFiltration {Ω : Type u_1} {ι : Type u_3} {m : } [] :
instance MeasureTheory.Filtration.instBotFiltration {Ω : Type u_1} {ι : Type u_3} {m : } [] :
instance MeasureTheory.Filtration.instTopFiltration {Ω : Type u_1} {ι : Type u_3} {m : } [] :
instance MeasureTheory.Filtration.instSupFiltration {Ω : Type u_1} {ι : Type u_3} {m : } [] :
theorem MeasureTheory.Filtration.coeFn_sup {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {g : } :
↑(f g) = f g
instance MeasureTheory.Filtration.instInfFiltration {Ω : Type u_1} {ι : Type u_3} {m : } [] :
theorem MeasureTheory.Filtration.coeFn_inf {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {g : } :
↑(f g) = f g
instance MeasureTheory.Filtration.instSupSetFiltration {Ω : Type u_1} {ι : Type u_3} {m : } [] :
theorem MeasureTheory.Filtration.sSup_def {Ω : Type u_1} {ι : Type u_3} {m : } [] (s : ) (i : ι) :
↑(sSup s) i = sSup ((fun f => f i) '' s)
noncomputable instance MeasureTheory.Filtration.instInfSetFiltration {Ω : Type u_1} {ι : Type u_3} {m : } [] :
theorem MeasureTheory.Filtration.sInf_def {Ω : Type u_1} {ι : Type u_3} {m : } [] (s : ) (i : ι) :
↑(sInf s) i = if then sInf ((fun f => f i) '' s) else m
noncomputable instance MeasureTheory.Filtration.instCompleteLattice {Ω : Type u_1} {ι : Type u_3} {m : } [] :
theorem MeasureTheory.measurableSet_of_filtration {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {s : Set Ω} {i : ι} (hs : ) :
class MeasureTheory.SigmaFiniteFiltration {Ω : Type u_1} {ι : Type u_3} {m : } [] (μ : ) (f : ) :

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

Instances
instance MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration {Ω : Type u_1} {ι : Type u_3} {m : } [] (μ : ) (f : ) [hf : ] (i : ι) :
instance MeasureTheory.IsFiniteMeasure.sigmaFiniteFiltration {Ω : Type u_1} {ι : Type u_3} {m : } [] (μ : ) (f : ) :
theorem MeasureTheory.Integrable.uniformIntegrable_condexp_filtration {Ω : Type u_1} {ι : Type u_3} {m : } [] {μ : } {f : } {g : Ω} (hg : ) :

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 : } [] {s : ιSet Ω} (hsm : ∀ (i : ι), MeasurableSet (s i)) :

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.

Instances For
theorem MeasureTheory.measurableSet_filtrationOfSet {Ω : Type u_1} {ι : Type u_3} {m : } [] {s : ιSet Ω} (hsm : ∀ (i : ι), MeasurableSet (s i)) (i : ι) {j : ι} (hj : j i) :
theorem MeasureTheory.measurableSet_filtrationOfSet' {Ω : Type u_1} {ι : Type u_3} {m : } [] {s : ιSet Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (i : ι) :
def MeasureTheory.Filtration.natural {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [mβ : ] [] [] (u : ιΩβ) (hum : ∀ (i : ι), ) :

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.

Instances For
theorem MeasureTheory.Filtration.filtrationOfSet_eq_natural {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [mβ : ] [] [] [] [] {s : ιSet Ω} (hsm : ∀ (i : ι), MeasurableSet (s i)) :
= MeasureTheory.Filtration.natural (fun i => Set.indicator (s i) fun x => 1) (_ : ∀ (i : ι), )
noncomputable def MeasureTheory.Filtration.limitProcess {Ω : Type u_1} {ι : Type u_3} {m : } [] {E : Type u_4} [Zero E] [] (f : ιΩE) (ℱ : ) (μ : ) :
Ω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.

Instances For
theorem MeasureTheory.Filtration.stronglyMeasurable_limitProcess {Ω : Type u_1} {ι : Type u_3} {m : } [] {E : Type u_4} [Zero E] [] {ℱ : } {f : ιΩE} {μ : } :
theorem MeasureTheory.Filtration.stronglyMeasurable_limit_process' {Ω : Type u_1} {ι : Type u_3} {m : } [] {E : Type u_4} [Zero E] [] {ℱ : } {f : ιΩE} {μ : } :
theorem MeasureTheory.Filtration.memℒp_limitProcess_of_snorm_bdd {Ω : Type u_1} {m : } {μ : } {R : NNReal} {p : ENNReal} {F : Type u_5} {ℱ : } {f : ΩF} (hfm : ∀ (n : ), ) (hbdd : ∀ (n : ), MeasureTheory.snorm (f n) p μ R) :