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 filtration f is σ-finite with respect to a measure μ if for all i, μ.trim (f.le i) is σ-finite.
• MeasureTheory.Filtration.natural: the smallest filtration that makes a process adapted. That notion adapted is not defined yet in this file. See MeasureTheory.adapted.
• MeasureTheory.Filtration.rightCont: the right-continuation of a filtration.
• MeasureTheory.Filtration.IsRightContinuous: a filtration is right-continuous if it is equal to its right-continuation.

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
• le' (i : ι) : ↑self i ≤ m

instance MeasureTheory.instCoeFunFiltrationForallMeasurableSpace {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] : CoeFun (Filtration ι m) fun (x : Filtration ι m) => ι → MeasurableSpace Ω

theorem MeasureTheory.Filtration.mono {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {i j : ι} (f : Filtration ι m) (hij : i ≤ j) : ↑f i ≤ ↑f j

theorem MeasureTheory.Filtration.le {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] (f : Filtration ι m) (i : ι) : ↑f i ≤ m

theorem MeasureTheory.Filtration.ext {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f g : Filtration ι m} (h : ↑f = ↑g) : f = g

theorem MeasureTheory.Filtration.ext_iff {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f g : Filtration ι m} : f = g ↔ ↑f = ↑g

def MeasureTheory.Filtration.const {Ω : Type u_1} (ι : Type u_2) {m : MeasurableSpace Ω} [Preorder ι] (m' : MeasurableSpace Ω) (hm' : m' ≤ m) : Filtration ι m

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

@[simp]

theorem MeasureTheory.Filtration.const_apply {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {m' : MeasurableSpace Ω} {hm' : m' ≤ m} (i : ι) : ↑(const ι m' hm') i = m'

instance MeasureTheory.Filtration.instInhabited {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] : Inhabited (Filtration ι m)

instance MeasureTheory.Filtration.instLE {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] : LE (Filtration ι m)

instance MeasureTheory.Filtration.instBot {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] : Bot (Filtration ι m)

instance MeasureTheory.Filtration.instTop {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] : Top (Filtration ι m)

instance MeasureTheory.Filtration.instMax {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] : Max (Filtration ι m)

theorem MeasureTheory.Filtration.coeFn_sup {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f g : Filtration ι m} : ↑(f ⊔ g) = ↑f ⊔ ↑g

instance MeasureTheory.Filtration.instMin {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] : Min (Filtration ι m)

theorem MeasureTheory.Filtration.coeFn_inf {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f g : Filtration ι m} : ↑(f ⊓ g) = ↑f ⊓ ↑g

instance MeasureTheory.Filtration.instSupSet {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] : SupSet (Filtration ι m)

theorem MeasureTheory.Filtration.sSup_def {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] (s : Set (Filtration ι m)) (i : ι) : ↑(sSup s) i = sSup ((fun (f : Filtration ι m) => ↑f i) '' s)

noncomputable instance MeasureTheory.Filtration.instInfSet {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] : InfSet (Filtration ι m)

theorem MeasureTheory.Filtration.sInf_def {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] (s : Set (Filtration ι m)) (i : ι) : ↑(sInf s) i = if s.Nonempty then sInf ((fun (f : Filtration ι m) => ↑f i) '' s) else m

noncomputable instance MeasureTheory.Filtration.instCompleteLattice {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] : CompleteLattice (Filtration ι m)

theorem MeasureTheory.measurableSet_of_filtration {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {s : Set Ω} {i : ι} (hs : MeasurableSet s) : MeasurableSet s

class MeasureTheory.SigmaFiniteFiltration {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] (μ : Measure Ω) (f : Filtration ι m) : Prop

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

instance MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] (μ : Measure Ω) (f : Filtration ι m) [hf : SigmaFiniteFiltration μ f] (i : ι) : SigmaFinite (μ.trim ⋯)

@[instance 100]

instance MeasureTheory.IsFiniteMeasure.sigmaFiniteFiltration {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] (μ : Measure Ω) (f : Filtration ι m) [IsFiniteMeasure μ] : SigmaFiniteFiltration μ f

theorem MeasureTheory.Integrable.uniformIntegrable_condExp_filtration {Ω : Type u_1} {ι : Type u_2} {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.

theorem MeasureTheory.Filtration.condExp_condExp {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f : Ω → E) {μ : Measure Ω} (ℱ : Filtration ι m) {i j : ι} (hij : i ≤ j) [SigmaFinite (μ.trim ⋯)] : μ[μ[f | ↑ℱ j] | ↑ℱ i] =ᶠ[ae μ] μ[f | ↑ℱ i]

def MeasureTheory.filtrationOfSet {Ω : Type u_1} {ι : Type u_2} {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.

theorem MeasureTheory.measurableSet_filtrationOfSet {Ω : Type u_1} {ι : Type u_2} {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_2} {m : MeasurableSpace Ω} [Preorder ι] {s : ι → Set Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (i : ι) : MeasurableSet (s i)

theorem MeasureTheory.Filtration.rightCont_def {Ω : Type u_3} {ι : Type u_4} {m : MeasurableSpace Ω} [PartialOrder ι] (𝓕 : Filtration ι m) : 𝓕.rightCont = { seq := fun (i : ι) => if (nhdsWithin i (Set.Ioi i)).NeBot then ⨅ (j : ι), ⨅ (_ : j > i), ↑𝓕 j else ↑𝓕 i, mono' := ⋯, le' := ⋯ }

@[irreducible]

noncomputable def MeasureTheory.Filtration.rightCont {Ω : Type u_3} {ι : Type u_4} {m : MeasurableSpace Ω} [PartialOrder ι] (𝓕 : Filtration ι m) : Filtration ι m

Given a filtration 𝓕, its right continuation is the filtration 𝓕₊ defined as follows:

• If i is isolated on the right, then 𝓕₊ i := 𝓕 i;
• Otherwise, 𝓕₊ i := ⨅ j > i, 𝓕 j. It is sometimes simply defined as 𝓕₊ i := ⨅ j > i, 𝓕 j when the index type is ℝ. In the general case this is not ideal however. If i is maximal for instance, then 𝓕₊ i = ⊤, which is inconvenient because 𝓕₊ is not a Filtration ι m anymore. If the index type is discrete (such as ℕ), then we would have 𝓕 = 𝓕₊ (i.e. 𝓕 is right-continuous) only if 𝓕 is constant.

To avoid requiring a TopologicalSpace instance on ι in the definition, we endow ι with the order topology Preorder.topology inside the definition. Say you write a statement about 𝓕₊ which does not require a TopologicalSpace structure on ι, but you wish to use a statement which requires a topology (such as rightCont_apply). Then you can endow ι with the order topology by writing

  letI := Preorder.topology ι
  haveI : OrderTopology ι := ⟨rfl⟩

def MeasureTheory.Filtration.«term_₊» : Lean.TrailingParserDescr

Given a filtration 𝓕, its right continuation is the filtration 𝓕₊ defined as follows:

• If i is isolated on the right, then 𝓕₊ i := 𝓕 i;
• Otherwise, 𝓕₊ i := ⨅ j > i, 𝓕 j. It is sometimes simply defined as 𝓕₊ i := ⨅ j > i, 𝓕 j when the index type is ℝ. In the general case this is not ideal however. If i is maximal for instance, then 𝓕₊ i = ⊤, which is inconvenient because 𝓕₊ is not a Filtration ι m anymore. If the index type is discrete (such as ℕ), then we would have 𝓕 = 𝓕₊ (i.e. 𝓕 is right-continuous) only if 𝓕 is constant.

To avoid requiring a TopologicalSpace instance on ι in the definition, we endow ι with the order topology Preorder.topology inside the definition. Say you write a statement about 𝓕₊ which does not require a TopologicalSpace structure on ι, but you wish to use a statement which requires a topology (such as rightCont_apply). Then you can endow ι with the order topology by writing

  letI := Preorder.topology ι
  haveI : OrderTopology ι := ⟨rfl⟩

theorem MeasureTheory.Filtration.rightCont_apply {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] [TopologicalSpace ι] [OrderTopology ι] (𝓕 : Filtration ι m) (i : ι) : ↑𝓕.rightCont i = if (nhdsWithin i (Set.Ioi i)).NeBot then ⨅ (j : ι), ⨅ (_ : j > i), ↑𝓕 j else ↑𝓕 i

theorem MeasureTheory.Filtration.rightCont_eq_of_nhdsGT_eq_bot {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] [TopologicalSpace ι] [OrderTopology ι] (𝓕 : Filtration ι m) {i : ι} (hi : nhdsWithin i (Set.Ioi i) = ⊥) : ↑𝓕.rightCont i = ↑𝓕 i

@[simp]

theorem MeasureTheory.Filtration.rightCont_eq_self {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [LinearOrder ι] [SuccOrder ι] (𝓕 : Filtration ι m) : 𝓕.rightCont = 𝓕

If the index type is a SuccOrder, then 𝓕₊ = 𝓕.

theorem MeasureTheory.Filtration.rightCont_eq_of_isMax {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] (𝓕 : Filtration ι m) {i : ι} (hi : IsMax i) : ↑𝓕.rightCont i = ↑𝓕 i

theorem MeasureTheory.Filtration.rightCont_eq_of_exists_gt {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [LinearOrder ι] (𝓕 : Filtration ι m) {i : ι} (hi : ∃ j > i, Set.Ioo i j = ∅) : ↑𝓕.rightCont i = ↑𝓕 i

theorem MeasureTheory.Filtration.rightCont_eq_of_neBot_nhdsGT {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] [TopologicalSpace ι] [OrderTopology ι] (𝓕 : Filtration ι m) (i : ι) [(nhdsWithin i (Set.Ioi i)).NeBot] : ↑𝓕.rightCont i = ⨅ (j : ι), ⨅ (_ : j > i), ↑𝓕 j

If i is not isolated on the right, then 𝓕₊ i = ⨅ j > i, 𝓕 j. This is for instance the case when ι is a densely ordered linear order with no maximal elements and equipped with the order topology, see rightCont_eq.

theorem MeasureTheory.Filtration.rightCont_eq_of_not_isMax {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [LinearOrder ι] [DenselyOrdered ι] (𝓕 : Filtration ι m) {i : ι} (hi : ¬IsMax i) : ↑𝓕.rightCont i = ⨅ (j : ι), ⨅ (_ : j > i), ↑𝓕 j

theorem MeasureTheory.Filtration.rightCont_eq {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [LinearOrder ι] [DenselyOrdered ι] [NoMaxOrder ι] (𝓕 : Filtration ι m) (i : ι) : ↑𝓕.rightCont i = ⨅ (j : ι), ⨅ (_ : j > i), ↑𝓕 j

If ι is a densely ordered linear order with no maximal element, then no point is isolated on the right, so that 𝓕₊ i = ⨅ j > i, 𝓕 j holds for all i. This is in particular the case when ι := ℝ≥0.

theorem MeasureTheory.Filtration.le_rightCont {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] (𝓕 : Filtration ι m) : 𝓕 ≤ 𝓕.rightCont

@[simp]

theorem MeasureTheory.Filtration.rightCont_self {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] (𝓕 : Filtration ι m) : 𝓕.rightCont.rightCont = 𝓕.rightCont

class MeasureTheory.Filtration.IsRightContinuous {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] (𝓕 : Filtration ι m) : Prop

A filtration 𝓕 is right continuous if it is equal to its right continuation 𝓕₊.

• RC : 𝓕.rightCont ≤ 𝓕

  The right continuity property.

theorem MeasureTheory.Filtration.IsRightContinuous.eq {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] {𝓕 : Filtration ι m} [h : 𝓕.IsRightContinuous] : 𝓕.rightCont = 𝓕

instance MeasureTheory.Filtration.instIsRightContinuousRightCont {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] {𝓕 : Filtration ι m} : 𝓕.rightCont.IsRightContinuous

theorem MeasureTheory.Filtration.IsRightContinuous.measurableSet {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] {𝓕 : Filtration ι m} [𝓕.IsRightContinuous] {i : ι} {s : Set Ω} (hs : MeasurableSet s) : MeasurableSet s

def MeasureTheory.Filtration.natural {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {β : ι → Type u_3} [(i : ι) → TopologicalSpace (β i)] [∀ (i : ι), TopologicalSpace.MetrizableSpace (β i)] [mβ : (i : ι) → MeasurableSpace (β i)] [∀ (i : ι), BorelSpace (β i)] [Preorder ι] (u : (i : ι) → Ω → β i) (hum : ∀ (i : ι), StronglyMeasurable (u i)) : Filtration ι m

Given a sequence of functions, the natural filtration is the smallest sequence of σ-algebras such that the sequence of functions is measurable with respect to the filtration.

theorem MeasureTheory.Filtration.filtrationOfSet_eq_natural {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {β : ι → Type u_3} [(i : ι) → TopologicalSpace (β i)] [∀ (i : ι), TopologicalSpace.MetrizableSpace (β i)] [mβ : (i : ι) → MeasurableSpace (β i)] [∀ (i : ι), BorelSpace (β i)] [Preorder ι] [(i : ι) → MulZeroOneClass (β i)] [∀ (i : ι), Nontrivial (β i)] {s : ι → Set Ω} (hsm : ∀ (i : ι), MeasurableSet (s i)) : filtrationOfSet hsm = natural (fun (i : ι) => (s i).indicator fun (x : Ω) => 1) ⋯

noncomputable def MeasureTheory.Filtration.limitProcess {Ω : Type u_1} {ι : Type u_2} {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.

theorem MeasureTheory.Filtration.stronglyMeasurable_limitProcess {Ω : Type u_1} {ι : Type u_2} {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_2} {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 μ

Filtration of the first events

def MeasureTheory.Filtration.piLE {ι : Type u_2} [Preorder ι] {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] : Filtration ι MeasurableSpace.pi

The canonical filtration on the product space Π i, X i, where piLE i consists of measurable sets depending only on coordinates ≤ i.

theorem MeasureTheory.Filtration.piLE_eq_comap_frestrictLe {ι : Type u_2} [Preorder ι] {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] [LocallyFiniteOrderBot ι] (i : ι) : ↑piLE i = MeasurableSpace.comap (Preorder.frestrictLe i) MeasurableSpace.pi

def MeasureTheory.Filtration.piFinset {ι : Type u_4} {X : ι → Type u_5} [(i : ι) → MeasurableSpace (X i)] : Filtration (Finset ι) MeasurableSpace.pi

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

theorem MeasureTheory.Filtration.piFinset_eq_comap_restrict {ι : Type u_4} {X : ι → Type u_5} [(i : ι) → MeasurableSpace (X i)] (s : Finset ι) : ↑piFinset s = MeasurableSpace.comap (↑s).restrict MeasurableSpace.pi

def MeasureTheory.Filtration.cylinderEventsCompl {Ω : Type u_1} {m : MeasurableSpace Ω} {α : Type u_4} : Filtration (Finset α)ᵒᵈ MeasurableSpace.pi

The exterior σ-algebras of finite sets of α form a cofiltration indexed by Finset α.