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)
- seq : ι → MeasurableSpace Ω
- 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 : MeasurableSpace Ω}
[Preorder ι]
:
CoeFun (MeasureTheory.Filtration ι m) fun x => ι → MeasurableSpace Ω
theorem
MeasureTheory.Filtration.mono
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{i : ι}
{j : ι}
(f : MeasureTheory.Filtration ι m)
(hij : i ≤ j)
:
↑f i ≤ ↑f j
theorem
MeasureTheory.Filtration.le
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
(f : MeasureTheory.Filtration ι m)
(i : ι)
:
↑f i ≤ m
theorem
MeasureTheory.Filtration.ext
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : MeasureTheory.Filtration ι m}
{g : MeasureTheory.Filtration ι m}
(h : ↑f = ↑g)
:
f = g
def
MeasureTheory.Filtration.const
{Ω : Type u_1}
(ι : Type u_3)
{m : MeasurableSpace Ω}
[Preorder ι]
(m' : MeasurableSpace Ω)
(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 : MeasurableSpace Ω}
[Preorder ι]
{m' : MeasurableSpace Ω}
{hm' : m' ≤ m}
(i : ι)
:
↑(MeasureTheory.Filtration.const ι m' hm') i = m'
instance
MeasureTheory.Filtration.instInhabitedFiltration
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
:
instance
MeasureTheory.Filtration.instLEFiltration
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
:
LE (MeasureTheory.Filtration ι m)
instance
MeasureTheory.Filtration.instBotFiltration
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
:
Bot (MeasureTheory.Filtration ι m)
instance
MeasureTheory.Filtration.instTopFiltration
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
:
Top (MeasureTheory.Filtration ι m)
instance
MeasureTheory.Filtration.instSupFiltration
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
:
Sup (MeasureTheory.Filtration ι m)
theorem
MeasureTheory.Filtration.coeFn_sup
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : MeasureTheory.Filtration ι m}
{g : MeasureTheory.Filtration ι m}
:
instance
MeasureTheory.Filtration.instInfFiltration
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
:
Inf (MeasureTheory.Filtration ι m)
theorem
MeasureTheory.Filtration.coeFn_inf
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : MeasureTheory.Filtration ι m}
{g : MeasureTheory.Filtration ι m}
:
instance
MeasureTheory.Filtration.instSupSetFiltration
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
:
theorem
MeasureTheory.Filtration.sSup_def
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
(s : Set (MeasureTheory.Filtration ι m))
(i : ι)
:
noncomputable instance
MeasureTheory.Filtration.instInfSetFiltration
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
:
theorem
MeasureTheory.Filtration.sInf_def
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
(s : Set (MeasureTheory.Filtration ι m))
(i : ι)
:
↑(sInf s) i = if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m
noncomputable instance
MeasureTheory.Filtration.instCompleteLattice
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
:
theorem
MeasureTheory.measurableSet_of_filtration
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : MeasureTheory.Filtration ι m}
{s : Set Ω}
{i : ι}
(hs : MeasurableSet s)
:
class
MeasureTheory.SigmaFiniteFiltration
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
(μ : MeasureTheory.Measure Ω)
(f : MeasureTheory.Filtration ι m)
:
- SigmaFinite : ∀ (i : ι), MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ (_ : ↑f i ≤ m))
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 : MeasurableSpace Ω}
[Preorder ι]
(μ : MeasureTheory.Measure Ω)
(f : MeasureTheory.Filtration ι m)
[hf : MeasureTheory.SigmaFiniteFiltration μ f]
(i : ι)
:
MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ (_ : ↑f i ≤ m))
instance
MeasureTheory.IsFiniteMeasure.sigmaFiniteFiltration
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
(μ : MeasureTheory.Measure Ω)
(f : MeasureTheory.Filtration ι m)
[MeasureTheory.IsFiniteMeasure μ]
:
theorem
MeasureTheory.Integrable.uniformIntegrable_condexp_filtration
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{f : MeasureTheory.Filtration ι m}
{g : Ω → ℝ}
(hg : MeasureTheory.Integrable g)
:
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 : MeasurableSpace Ω}
[Preorder ι]
{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 : 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 : ι), MeasureTheory.StronglyMeasurable (u 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 : MeasurableSpace Ω}
[TopologicalSpace β]
[TopologicalSpace.MetrizableSpace β]
[mβ : MeasurableSpace β]
[BorelSpace β]
[Preorder ι]
[MulZeroOneClass β]
[Nontrivial β]
{s : ι → Set Ω}
(hsm : ∀ (i : ι), MeasurableSet (s i))
:
MeasureTheory.filtrationOfSet hsm = MeasureTheory.Filtration.natural (fun i => Set.indicator (s i) fun x => 1)
(_ : ∀ (i : ι), MeasureTheory.StronglyMeasurable (Set.indicator (s i) 1))
noncomputable def
MeasureTheory.Filtration.limitProcess
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{E : Type u_4}
[Zero E]
[TopologicalSpace E]
(f : ι → Ω → E)
(ℱ : MeasureTheory.Filtration ι m)
(μ : MeasureTheory.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.
Instances For
theorem
MeasureTheory.Filtration.stronglyMeasurable_limitProcess
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{E : Type u_4}
[Zero E]
[TopologicalSpace E]
{ℱ : MeasureTheory.Filtration ι m}
{f : ι → Ω → E}
{μ : MeasureTheory.Measure Ω}
:
theorem
MeasureTheory.Filtration.stronglyMeasurable_limit_process'
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{E : Type u_4}
[Zero E]
[TopologicalSpace E]
{ℱ : MeasureTheory.Filtration ι m}
{f : ι → Ω → E}
{μ : MeasureTheory.Measure Ω}
:
theorem
MeasureTheory.Filtration.memℒp_limitProcess_of_snorm_bdd
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{R : NNReal}
{p : ENNReal}
{F : Type u_5}
[NormedAddCommGroup F]
{ℱ : MeasureTheory.Filtration ℕ m}
{f : ℕ → Ω → F}
(hfm : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ)
(hbdd : ∀ (n : ℕ), MeasureTheory.snorm (f n) p μ ≤ ↑R)
: