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 filtrationf
is σ-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 notionadapted
is not defined yet in this file. SeeMeasureTheory.adapted
.
Main results #
MeasureTheory.Filtration.instCompleteLattice
: filtrations are a complete lattice.
Tags #
filtration, stochastic process
- 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
The constant filtration which is equal to m
for all i : ι
.
Instances For
- 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
Given an integrable function g
, the conditional expectations of g
with respect to a
filtration is uniformly integrable.
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
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
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.