# Filtrations #

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

## Tags #

filtration, stochastic process

structure MeasureTheory.Filtration {Ω : Type u_1} (ι : Type u_2) [] (m : ) :
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 : ι
• mono' : Monotone self
• le' : ∀ (i : ι), self i m
Instances For
theorem MeasureTheory.Filtration.mono' {Ω : Type u_1} {ι : Type u_2} [] {m : } (self : ) :
Monotone self
theorem MeasureTheory.Filtration.le' {Ω : Type u_1} {ι : Type u_2} [] {m : } (self : ) (i : ι) :
self i m
instance MeasureTheory.instCoeFunFiltrationForallMeasurableSpace {Ω : Type u_1} {ι : Type u_3} {m : } [] :
CoeFun () fun (x : ) => ι
Equations
• MeasureTheory.instCoeFunFiltrationForallMeasurableSpace = { coe := fun (f : ) => f }
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 : ι.

Equations
• = { seq := fun (x : ι) => m', mono' := , le' := }
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.instInhabited {Ω : Type u_1} {ι : Type u_3} {m : } [] :
Equations
• MeasureTheory.Filtration.instInhabited = { default := }
instance MeasureTheory.Filtration.instLE {Ω : Type u_1} {ι : Type u_3} {m : } [] :
Equations
• MeasureTheory.Filtration.instLE = { le := fun (f g : ) => ∀ (i : ι), f i g i }
instance MeasureTheory.Filtration.instBot {Ω : Type u_1} {ι : Type u_3} {m : } [] :
Equations
• MeasureTheory.Filtration.instBot = { bot := }
instance MeasureTheory.Filtration.instTop {Ω : Type u_1} {ι : Type u_3} {m : } [] :
Equations
• MeasureTheory.Filtration.instTop = { top := }
instance MeasureTheory.Filtration.instSup {Ω : Type u_1} {ι : Type u_3} {m : } [] :
Equations
• MeasureTheory.Filtration.instSup = { sup := fun (f g : ) => { seq := fun (i : ι) => f i g i, mono' := , le' := } }
theorem MeasureTheory.Filtration.coeFn_sup {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {g : } :
(f g) = f g
instance MeasureTheory.Filtration.instInf {Ω : Type u_1} {ι : Type u_3} {m : } [] :
Equations
• MeasureTheory.Filtration.instInf = { inf := fun (f g : ) => { seq := fun (i : ι) => f i g i, mono' := , le' := } }
theorem MeasureTheory.Filtration.coeFn_inf {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {g : } :
(f g) = f g
instance MeasureTheory.Filtration.instSupSet {Ω : Type u_1} {ι : Type u_3} {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 : } [] (s : ) (i : ι) :
(sSup s) i = sSup ((fun (f : ) => f i) '' s)
noncomputable instance MeasureTheory.Filtration.instInfSet {Ω : Type u_1} {ι : Type u_3} {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 : } [] (s : ) (i : ι) :
(sInf s) i = if s.Nonempty then sInf ((fun (f : ) => f i) '' s) else m
noncomputable instance MeasureTheory.Filtration.instCompleteLattice {Ω : Type u_1} {ι : Type u_3} {m : } [] :
Equations
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
theorem MeasureTheory.SigmaFiniteFiltration.SigmaFinite {Ω : Type u_1} {ι : Type u_3} {m : } [] {μ : } {f : } [self : ] (i : ι) :
instance MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration {Ω : Type u_1} {ι : Type u_3} {m : } [] (μ : ) (f : ) [hf : ] (i : ι) :
Equations
• =
@[instance 100]
instance MeasureTheory.IsFiniteMeasure.sigmaFiniteFiltration {Ω : Type u_1} {ι : Type u_3} {m : } [] (μ : ) (f : ) :
Equations
• =
theorem MeasureTheory.Integrable.uniformIntegrable_condexp_filtration {Ω : Type u_1} {ι : Type u_3} {m : } [] {μ : } {f : } {g : Ω} (hg : ) :
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 : } [] {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.

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

Equations
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 : ι) => (s i).indicator fun (x : Ω) => 1)
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.

Equations
• One or more equations did not get rendered due to their size.
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) :