# mathlib3documentation

probability.process.filtration

# Filtrations #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main definitions #

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

## Main results #

• measure_theory.filtration.complete_lattice: filtrations are a complete lattice.

## Tags #

filtration, stochastic process

structure measure_theory.filtration {Ω : Type u_1} (ι : Type u_2) [preorder ι] (m : measurable_space Ω) :
Type (max u_1 u_2)

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

Instances for measure_theory.filtration
@[protected, instance]
def measure_theory.filtration.has_coe_to_fun {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] :
(λ (_x : ,
Equations
@[protected]
theorem measure_theory.filtration.mono {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {i j : ι} (f : m) (hij : i j) :
f i f j
@[protected]
theorem measure_theory.filtration.le {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] (f : m) (i : ι) :
f i m
@[protected, ext]
theorem measure_theory.filtration.ext {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {f g : m} (h : f = g) :
f = g
def measure_theory.filtration.const {Ω : Type u_1} (ι : Type u_3) {m : measurable_space Ω} [preorder ι] (m' : measurable_space Ω) (hm' : m' m) :

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

Equations
@[simp]
theorem measure_theory.filtration.const_apply {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {m' : measurable_space Ω} {hm' : m' m} (i : ι) :
hm') i = m'
@[protected, instance]
def measure_theory.filtration.inhabited {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] :
Equations
@[protected, instance]
def measure_theory.filtration.has_le {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] :
Equations
@[protected, instance]
def measure_theory.filtration.has_bot {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] :
Equations
@[protected, instance]
def measure_theory.filtration.has_top {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] :
Equations
@[protected, instance]
def measure_theory.filtration.has_sup {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] :
Equations
@[norm_cast]
theorem measure_theory.filtration.coe_fn_sup {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {f g : m} :
(f g) = f g
@[protected, instance]
def measure_theory.filtration.has_inf {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] :
Equations
@[norm_cast]
theorem measure_theory.filtration.coe_fn_inf {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {f g : m} :
(f g) = f g
@[protected, instance]
def measure_theory.filtration.has_Sup {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] :
Equations
theorem measure_theory.filtration.Sup_def {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] (s : set ) (i : ι) :
(has_Sup.Sup s) i = has_Sup.Sup ((λ (f : , f i) '' s)
@[protected, instance]
noncomputable def measure_theory.filtration.has_Inf {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] :
Equations
theorem measure_theory.filtration.Inf_def {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] (s : set ) (i : ι) :
(has_Inf.Inf s) i = (has_Inf.Inf ((λ (f : , f i) '' s)) m
@[protected, instance]
noncomputable def measure_theory.filtration.complete_lattice {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] :
Equations
theorem measure_theory.measurable_set_of_filtration {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {f : m} {s : set Ω} {i : ι} (hs : measurable_set s) :
@[class]
structure measure_theory.sigma_finite_filtration {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] (μ : measure_theory.measure Ω) (f : m) :
Prop
• sigma_finite : (i : ι),

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

Instances of this typeclass
@[protected, instance]
def measure_theory.sigma_finite_of_sigma_finite_filtration {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] (μ : measure_theory.measure Ω) (f : m) (i : ι) :
@[protected, instance]
theorem measure_theory.integrable.uniform_integrable_condexp_filtration {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {μ : measure_theory.measure Ω} {f : m} {g : Ω } (hg : μ) :
measure_theory.uniform_integrable (λ (i : ι), μ g) 1 μ

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

def measure_theory.filtration_of_set {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {s : ι set Ω} (hsm : (i : ι), measurable_set (s i)) :

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

Equations
theorem measure_theory.measurable_set_filtration_of_set {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {s : ι set Ω} (hsm : (i : ι), measurable_set (s i)) (i : ι) {j : ι} (hj : j i) :
theorem measure_theory.measurable_set_filtration_of_set' {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {s : ι set Ω} (hsm : (n : ι), measurable_set (s n)) (i : ι) :
def measure_theory.filtration.natural {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [mβ : measurable_space β] [borel_space β] [preorder ι] (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
theorem measure_theory.filtration.filtration_of_set_eq_natural {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [mβ : measurable_space β] [borel_space β] [preorder ι] [nontrivial β] {s : ι set Ω} (hsm : (i : ι), measurable_set (s i)) :
= measure_theory.filtration.natural (λ (i : ι), (s i).indicator (λ (ω : Ω), 1)) _
noncomputable def measure_theory.filtration.limit_process {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {E : Type u_4} [has_zero E] (f : ι Ω E) (ℱ : m) (μ : . "volume_tac") :
Ω E

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

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

Equations
theorem measure_theory.filtration.strongly_measurable_limit_process {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {E : Type u_4} [has_zero E] {ℱ : m} {f : ι Ω E} {μ : measure_theory.measure Ω} :
theorem measure_theory.filtration.strongly_measurable_limit_process' {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {E : Type u_4} [has_zero E] {ℱ : m} {f : ι Ω E} {μ : measure_theory.measure Ω} :
theorem measure_theory.filtration.mem_ℒp_limit_process_of_snorm_bdd {Ω : Type u_1} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {R : nnreal} {p : ennreal} {F : Type u_2} {ℱ : m} {f : Ω F} (hfm : (n : ), ) (hbdd : (n : ), measure_theory.snorm (f n) p μ R) :