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 filtrationfis σ-finite with respect to a measureμif for alli,μ.trim (f.le i)is σ-finite.MeasureTheory.Filtration.natural: the smallest filtration that makes a process adapted. That notionadaptedis not defined yet in this file. SeeMeasureTheory.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 Ω
The sequence of sub-σ-algebras of
m - mono' : Monotone ↑self
Instances For
instance
MeasureTheory.instCoeFunFiltrationForallMeasurableSpace
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
:
CoeFun (Filtration ι m) fun (x : Filtration ι m) => ι → MeasurableSpace Ω
Equations
theorem
MeasureTheory.Filtration.mono
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{i j : ι}
(f : Filtration ι m)
(hij : i ≤ j)
:
theorem
MeasureTheory.Filtration.le
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
(f : Filtration ι m)
(i : ι)
:
theorem
MeasureTheory.Filtration.ext
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f g : Filtration ι m}
(h : ↑f = ↑g)
:
theorem
MeasureTheory.Filtration.ext_iff
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f g : Filtration ι m}
:
def
MeasureTheory.Filtration.const
{Ω : Type u_1}
(ι : Type u_3)
{m : MeasurableSpace Ω}
[Preorder ι]
(m' : MeasurableSpace Ω)
(hm' : m' ≤ m)
:
Filtration ι m
The constant filtration which is equal to m for all i : ι.
Equations
Instances For
@[simp]
theorem
MeasureTheory.Filtration.const_apply
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{m' : MeasurableSpace Ω}
{hm' : m' ≤ m}
(i : ι)
:
instance
MeasureTheory.Filtration.instInhabited
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
:
Inhabited (Filtration ι m)
Equations
instance
MeasureTheory.Filtration.instLE
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
:
LE (Filtration ι m)
Equations
instance
MeasureTheory.Filtration.instBot
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
:
Bot (Filtration ι m)
Equations
instance
MeasureTheory.Filtration.instTop
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
:
Top (Filtration ι m)
Equations
instance
MeasureTheory.Filtration.instMax
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
:
Max (Filtration ι m)
Equations
theorem
MeasureTheory.Filtration.coeFn_sup
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f g : Filtration ι m}
:
instance
MeasureTheory.Filtration.instMin
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
:
Min (Filtration ι m)
Equations
theorem
MeasureTheory.Filtration.coeFn_inf
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f g : Filtration ι m}
:
instance
MeasureTheory.Filtration.instSupSet
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
:
SupSet (Filtration ι m)
Equations
theorem
MeasureTheory.Filtration.sSup_def
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
(s : Set (Filtration ι m))
(i : ι)
:
noncomputable instance
MeasureTheory.Filtration.instInfSet
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
:
InfSet (Filtration ι m)
Equations
theorem
MeasureTheory.Filtration.sInf_def
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
(s : Set (Filtration ι m))
(i : ι)
:
noncomputable instance
MeasureTheory.Filtration.instCompleteLattice
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
:
CompleteLattice (Filtration ι m)
Equations
theorem
MeasureTheory.measurableSet_of_filtration
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{s : Set Ω}
{i : ι}
(hs : MeasurableSet s)
:
class
MeasureTheory.SigmaFiniteFiltration
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
(μ : Measure Ω)
(f : Filtration ι m)
:
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 (μ.trim ⋯)
Instances
instance
MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
(μ : Measure Ω)
(f : Filtration ι m)
[hf : SigmaFiniteFiltration μ f]
(i : ι)
:
SigmaFinite (μ.trim ⋯)
@[instance 100]
instance
MeasureTheory.IsFiniteMeasure.sigmaFiniteFiltration
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
(μ : Measure Ω)
(f : Filtration ι m)
[IsFiniteMeasure μ]
:
theorem
MeasureTheory.Integrable.uniformIntegrable_condExp_filtration
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{μ : Measure Ω}
[IsFiniteMeasure μ]
{f : Filtration ι m}
{g : Ω → ℝ}
(hg : Integrable g μ)
:
UniformIntegrable (fun (i : ι) => μ[g|↑f i]) 1 μ
Given an integrable function g, the conditional expectations of g with respect to a
filtration is uniformly integrable.
@[deprecated MeasureTheory.Integrable.uniformIntegrable_condExp_filtration (since := "2025-01-21")]
theorem
MeasureTheory.Integrable.uniformIntegrable_condexp_filtration
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{μ : Measure Ω}
[IsFiniteMeasure μ]
{f : Filtration ι m}
{g : Ω → ℝ}
(hg : Integrable g μ)
:
UniformIntegrable (fun (i : ι) => μ[g|↑f i]) 1 μ
Alias of MeasureTheory.Integrable.uniformIntegrable_condExp_filtration.
Given an integrable function g, the conditional expectations of g with respect to a
filtration is uniformly integrable.
theorem
MeasureTheory.Filtration.condExp_condExp
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(f : Ω → E)
{μ : Measure Ω}
(ℱ : Filtration ι m)
{i j : ι}
(hij : i ≤ j)
[SigmaFinite (μ.trim ⋯)]
:
def
MeasureTheory.filtrationOfSet
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{s : ι → Set Ω}
(hsm : ∀ (i : ι), MeasurableSet (s i))
:
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
Instances For
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 : ι), StronglyMeasurable (u i))
:
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
Instances For
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))
:
noncomputable def
MeasureTheory.Filtration.limitProcess
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{E : Type u_4}
[Zero E]
[TopologicalSpace E]
(f : ι → Ω → E)
(ℱ : Filtration ι m)
(μ : 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
Instances For
theorem
MeasureTheory.Filtration.stronglyMeasurable_limitProcess
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{E : Type u_4}
[Zero E]
[TopologicalSpace E]
{ℱ : Filtration ι m}
{f : ι → Ω → E}
{μ : Measure Ω}
:
StronglyMeasurable (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]
{ℱ : Filtration ι m}
{f : ι → Ω → E}
{μ : Measure Ω}
:
StronglyMeasurable (limitProcess f ℱ μ)
theorem
MeasureTheory.Filtration.memLp_limitProcess_of_eLpNorm_bdd
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{μ : Measure Ω}
{R : NNReal}
{p : ENNReal}
{F : Type u_5}
[NormedAddCommGroup F]
{ℱ : Filtration ℕ m}
{f : ℕ → Ω → F}
(hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ)
(hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R)
:
MemLp (limitProcess f ℱ μ) p μ
@[deprecated MeasureTheory.Filtration.memLp_limitProcess_of_eLpNorm_bdd (since := "2025-02-21")]
theorem
MeasureTheory.Filtration.memℒp_limitProcess_of_eLpNorm_bdd
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{μ : Measure Ω}
{R : NNReal}
{p : ENNReal}
{F : Type u_5}
[NormedAddCommGroup F]
{ℱ : Filtration ℕ m}
{f : ℕ → Ω → F}
(hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ)
(hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R)
:
MemLp (limitProcess f ℱ μ) p μ
Alias of MeasureTheory.Filtration.memLp_limitProcess_of_eLpNorm_bdd.
Filtration of the first events #
def
MeasureTheory.Filtration.piLE
{ι : Type u_3}
[Preorder ι]
{X : ι → Type u_4}
[(i : ι) → MeasurableSpace (X i)]
:
The canonical filtration on the product space Π i, X i, where piLE i
consists of measurable sets depending only on coordinates ≤ i.
Equations
Instances For
theorem
MeasureTheory.Filtration.piLE_eq_comap_frestrictLe
{ι : Type u_3}
[Preorder ι]
{X : ι → Type u_4}
[(i : ι) → MeasurableSpace (X i)]
[LocallyFiniteOrderBot ι]
(i : ι)
:
def
MeasureTheory.Filtration.piFinset
{ι : Type u_4}
{X : ι → Type u_5}
[(i : ι) → MeasurableSpace (X i)]
:
The filtration of events which only depends on finitely many coordinates
on the product space Π i, X i, piFinset s consists of measurable sets depending only on
coordinates in s, where s : Finset ι.
Equations
Instances For
theorem
MeasureTheory.Filtration.piFinset_eq_comap_restrict
{ι : Type u_4}
{X : ι → Type u_5}
[(i : ι) → MeasurableSpace (X i)]
(s : Finset ι)
:
def
MeasureTheory.Filtration.cylinderEventsCompl
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{α : Type u_4}
:
The exterior σ-algebras of finite sets of α form a cofiltration indexed by Finset α.