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

source

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

Type (max u_1 u_2)

seq : ι → measurable_space Ω
mono' : monotone self.seq
le' : ∀ (i : ι), self.seq i ≤ m

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

Instances for measure_theory.filtration

source

@[protected, instance]

def measure_theory.filtration.has_coe_to_fun {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] :

has_coe_to_fun (measure_theory.filtration ι m) (λ (_x : measure_theory.filtration ι m), ι → measurable_space Ω)

Equations

measure_theory.filtration.has_coe_to_fun = {coe := λ (f : measure_theory.filtration ι m), f.seq}

source

@[protected]

theorem measure_theory.filtration.mono {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {i j : ι} (f : measure_theory.filtration ι m) (hij : i ≤ j) :

⇑f i ≤ ⇑f j

source

@[protected]

theorem measure_theory.filtration.le {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] (f : measure_theory.filtration ι m) (i : ι) :

⇑f i ≤ m

source

@[protected, ext]

theorem measure_theory.filtration.ext {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {f g : measure_theory.filtration ι m} (h : ⇑f = ⇑g) :

f = g

source

def measure_theory.filtration.const {Ω : Type u_1} (ι : Type u_3) {m : measurable_space Ω} [preorder ι] (m' : measurable_space Ω) (hm' : m' ≤ m) :

measure_theory.filtration ι m

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

Equations

measure_theory.filtration.const ι m' hm' = {seq := λ (_x : ι), m', mono' := _, le' := _}

source

@[simp]

theorem measure_theory.filtration.const_apply {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {m' : measurable_space Ω} {hm' : m' ≤ m} (i : ι) :

⇑(measure_theory.filtration.const ι m' hm') i = m'

source

@[protected, instance]

def measure_theory.filtration.inhabited {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] :

inhabited (measure_theory.filtration ι m)

Equations

measure_theory.filtration.inhabited = {default := measure_theory.filtration.const ι m measure_theory.filtration.inhabited._proof_1}

source

@[protected, instance]

def measure_theory.filtration.has_le {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] :

has_le (measure_theory.filtration ι m)

Equations

measure_theory.filtration.has_le = {le := λ (f g : measure_theory.filtration ι m), ∀ (i : ι), ⇑f i ≤ ⇑g i}

source

@[protected, instance]

def measure_theory.filtration.has_bot {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] :

has_bot (measure_theory.filtration ι m)

Equations

measure_theory.filtration.has_bot = {bot := measure_theory.filtration.const ι ⊥ measure_theory.filtration.has_bot._proof_1}

source

@[protected, instance]

def measure_theory.filtration.has_top {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] :

has_top (measure_theory.filtration ι m)

Equations

measure_theory.filtration.has_top = {top := measure_theory.filtration.const ι m measure_theory.filtration.has_top._proof_1}

source

@[protected, instance]

def measure_theory.filtration.has_sup {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] :

has_sup (measure_theory.filtration ι m)

Equations

measure_theory.filtration.has_sup = {sup := λ (f g : measure_theory.filtration ι m), {seq := λ (i : ι), ⇑f i ⊔ ⇑g i, mono' := _, le' := _}}

source

@[norm_cast]

theorem measure_theory.filtration.coe_fn_sup {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {f g : measure_theory.filtration ι m} :

⇑(f ⊔ g) = ⇑f ⊔ ⇑g

source

@[protected, instance]

def measure_theory.filtration.has_inf {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] :

has_inf (measure_theory.filtration ι m)

Equations

measure_theory.filtration.has_inf = {inf := λ (f g : measure_theory.filtration ι m), {seq := λ (i : ι), ⇑f i ⊓ ⇑g i, mono' := _, le' := _}}

source

@[norm_cast]

theorem measure_theory.filtration.coe_fn_inf {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {f g : measure_theory.filtration ι m} :

⇑(f ⊓ g) = ⇑f ⊓ ⇑g

source

@[protected, instance]

def measure_theory.filtration.has_Sup {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] :

has_Sup (measure_theory.filtration ι m)

Equations

measure_theory.filtration.has_Sup = {Sup := λ (s : set (measure_theory.filtration ι m)), {seq := λ (i : ι), has_Sup.Sup ((λ (f : measure_theory.filtration ι m), ⇑f i) '' s), mono' := _, le' := _}}

source

theorem measure_theory.filtration.Sup_def {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] (s : set (measure_theory.filtration ι m)) (i : ι) :

⇑(has_Sup.Sup s) i = has_Sup.Sup ((λ (f : measure_theory.filtration ι m), ⇑f i) '' s)

source

@[protected, instance]

noncomputable def measure_theory.filtration.has_Inf {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] :

has_Inf (measure_theory.filtration ι m)

Equations

measure_theory.filtration.has_Inf = {Inf := λ (s : set (measure_theory.filtration ι m)), {seq := λ (i : ι), ite s.nonempty (has_Inf.Inf ((λ (f : measure_theory.filtration ι m), ⇑f i) '' s)) m, mono' := _, le' := _}}

source

theorem measure_theory.filtration.Inf_def {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] (s : set (measure_theory.filtration ι m)) (i : ι) :

⇑(has_Inf.Inf s) i = ite s.nonempty (has_Inf.Inf ((λ (f : measure_theory.filtration ι m), ⇑f i) '' s)) m

source

@[protected, instance]

noncomputable def measure_theory.filtration.complete_lattice {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] :

complete_lattice (measure_theory.filtration ι m)

Equations

measure_theory.filtration.complete_lattice = {sup := has_sup.sup measure_theory.filtration.has_sup, le := has_le.le measure_theory.filtration.has_le, lt := lattice.lt._default has_le.le, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf measure_theory.filtration.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := has_Sup.Sup measure_theory.filtration.has_Sup, le_Sup := _, Sup_le := _, Inf := has_Inf.Inf measure_theory.filtration.has_Inf, Inf_le := _, le_Inf := _, top := ⊤, bot := ⊥, le_top := _, bot_le := _}

source

theorem measure_theory.measurable_set_of_filtration {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {f : measure_theory.filtration ι m} {s : set Ω} {i : ι} (hs : measurable_set s) :

measurable_set s

source

@[class]

structure measure_theory.sigma_finite_filtration {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] (μ : measure_theory.measure Ω) (f : measure_theory.filtration ι m) :

Prop

sigma_finite : ∀ (i : ι), measure_theory.sigma_finite (μ.trim _)

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

measure_theory.is_finite_measure.sigma_finite_filtration

source

@[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 : measure_theory.filtration ι m) [hf : measure_theory.sigma_finite_filtration μ f] (i : ι) :

measure_theory.sigma_finite (μ.trim _)

source

@[protected, instance]

def measure_theory.is_finite_measure.sigma_finite_filtration {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] (μ : measure_theory.measure Ω) (f : measure_theory.filtration ι m) [measure_theory.is_finite_measure μ] :

measure_theory.sigma_finite_filtration μ f

source

theorem measure_theory.integrable.uniform_integrable_condexp_filtration {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {μ : measure_theory.measure Ω} [measure_theory.is_finite_measure μ] {f : measure_theory.filtration ι m} {g : Ω → ℝ} (hg : measure_theory.integrable g μ) :

measure_theory.uniform_integrable (λ (i : ι), measure_theory.condexp (⇑f i) μ g) 1 μ

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

source

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

measure_theory.filtration ι m

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

measure_theory.filtration_of_set hsm = {seq := λ (i : ι), measurable_space.generate_from {t : set Ω | ∃ (j : ι) (H : j ≤ i), s j = t}, mono' := _, le' := _}

source

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) :

measurable_set (s j)

source

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 : ι) :

measurable_set (s i)

source

def measure_theory.filtration.natural {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [topological_space β] [topological_space.metrizable_space β] [mβ : measurable_space β] [borel_space β] [preorder ι] (u : ι → Ω → β) (hum : ∀ (i : ι), measure_theory.strongly_measurable (u i)) :

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

measure_theory.filtration.natural u hum = {seq := λ (i : ι), ⨆ (j : ι) (H : j ≤ i), measurable_space.comap (u j) mβ, mono' := _, le' := _}

source

theorem measure_theory.filtration.filtration_of_set_eq_natural {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [topological_space β] [topological_space.metrizable_space β] [mβ : measurable_space β] [borel_space β] [preorder ι] [mul_zero_one_class β] [nontrivial β] {s : ι → set Ω} (hsm : ∀ (i : ι), measurable_set (s i)) :

measure_theory.filtration_of_set hsm = measure_theory.filtration.natural (λ (i : ι), (s i).indicator (λ (ω : Ω), 1)) _

source

noncomputable def measure_theory.filtration.limit_process {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {E : Type u_4} [has_zero E] [topological_space E] (f : ι → Ω → E) (ℱ : measure_theory.filtration ι m) (μ : measure_theory.measure Ω . "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

measure_theory.filtration.limit_process f ℱ μ = dite (∃ (g : Ω → E), measure_theory.strongly_measurable g ∧ ∀ᵐ (ω : Ω) ∂μ, filter.tendsto (λ (n : ι), f n ω) filter.at_top (nhds (g ω))) (λ (h : ∃ (g : Ω → E), measure_theory.strongly_measurable g ∧ ∀ᵐ (ω : Ω) ∂μ, filter.tendsto (λ (n : ι), f n ω) filter.at_top (nhds (g ω))), classical.some h) (λ (h : ¬∃ (g : Ω → E), measure_theory.strongly_measurable g ∧ ∀ᵐ (ω : Ω) ∂μ, filter.tendsto (λ (n : ι), f n ω) filter.at_top (nhds (g ω))), 0)

source

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] [topological_space E] {ℱ : measure_theory.filtration ι m} {f : ι → Ω → E} {μ : measure_theory.measure Ω} :

measure_theory.strongly_measurable (measure_theory.filtration.limit_process f ℱ μ)

source

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] [topological_space E] {ℱ : measure_theory.filtration ι m} {f : ι → Ω → E} {μ : measure_theory.measure Ω} :

measure_theory.strongly_measurable (measure_theory.filtration.limit_process f ℱ μ)

source

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} [normed_add_comm_group F] {ℱ : measure_theory.filtration ℕ m} {f : ℕ → Ω → F} (hfm : ∀ (n : ℕ), measure_theory.ae_strongly_measurable (f n) μ) (hbdd : ∀ (n : ℕ), measure_theory.snorm (f n) p μ ≤ ↑R) :

measure_theory.mem_ℒp (measure_theory.filtration.limit_process f ℱ μ) p μ