Documentation

Exchangeability.DeFinetti.ViaMartingale.FutureFiltration

Future Filtration #

The future filtration at level m is σ(θ_{m+1} X), i.e., σ(X_{m+1}, X_{m+2}, ...). This is the σ-algebra generated by coordinates after position m.

Main definitions #

Main results #

These are extracted from ViaMartingale.lean to enable modular imports.

Future Filtration Definition #

source
@[reducible, inline]
abbrev Exchangeability.DeFinetti.ViaMartingale.futureFiltration {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ → Ω → α) (m : ℕ) :
MeasurableSpace Ω

Future reverse filtration: 𝔽ᶠᵘᵗₘ = σ(θ_{m+1} X).

Equations
Instances For

    Future Filtration Properties #

    source
    theorem Exchangeability.DeFinetti.ViaMartingale.futureFiltration_antitone {Ω : Type u_3} {α : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] (X : ℕ → Ω → α) :
    Antitone (futureFiltration X)

    The future filtration is decreasing (antitone).

    source
    def Exchangeability.DeFinetti.ViaMartingale.tailSigmaFuture {Ω : Type u_3} {α : Type u_4} [MeasurableSpace α] (X : ℕ → Ω → α) :
    MeasurableSpace Ω

    Tail σ-algebra via the future filtration. (Additive alias.)

    Equations
    Instances For
      source
      @[simp]
      theorem Exchangeability.DeFinetti.ViaMartingale.tailSigmaFuture_eq_iInf {Ω : Type u_3} {α : Type u_4} [MeasurableSpace α] (X : ℕ → Ω → α) :
      tailSigmaFuture X = ⨅ (m : ℕ), futureFiltration X m
      source
      @[simp]
      theorem Exchangeability.DeFinetti.ViaMartingale.futureFiltration_eq_rev_succ {Ω : Type u_3} {α : Type u_4} [MeasurableSpace α] (X : ℕ → Ω → α) (m : ℕ) :
      futureFiltration X m = revFiltration X (m + 1)
      source
      theorem Exchangeability.DeFinetti.ViaMartingale.tailSigmaFuture_eq_tailSigma {Ω : Type u_3} {α : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] (X : ℕ → Ω → α) :
      tailSigmaFuture X = tailSigma X

      Helper lemmas for tail σ-algebra #

      source
      theorem Exchangeability.DeFinetti.ViaMartingale.tailSigma_le {Ω : Type u_5} {α : Type u_6} [MeasurableSpace Ω] [MeasurableSpace α] (X : ℕ → Ω → α) (hX : ∀ (n : ℕ), Measurable (X n)) :
      tailSigma X ≤ inferInstance

      The tail σ-algebra is a sub-σ-algebra of the ambient σ-algebra.

      source
      theorem Exchangeability.DeFinetti.ViaMartingale.tailSigma_le_futureFiltration {Ω : Type u_5} {α : Type u_6} [MeasurableSpace Ω] [MeasurableSpace α] (X : ℕ → Ω → α) (m : ℕ) :
      tailSigma X ≤ futureFiltration X m

      Tail σ-algebra is sub-σ-algebra of future filtration.

      source
      theorem Exchangeability.DeFinetti.ViaMartingale.indicator_tailMeasurable {Ω : Type u_5} {α : Type u_6} [MeasurableSpace Ω] [MeasurableSpace α] (X : ℕ → Ω → α) (A : Set Ω) (hA : MeasurableSet A) :
      MeasureTheory.StronglyMeasurable (A.indicator fun (x : Ω) => 1)

      Indicators of tail-measurable sets are tail-measurable functions.

      source
      theorem Exchangeability.DeFinetti.ViaMartingale.sigmaFinite_trim_tailSigma {Ω : Type u_5} {α : Type u_6} {m₀ : MeasurableSpace Ω} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (X : ℕ → Ω → α) (hX : ∀ (n : ℕ), Measurable (X n)) :
      MeasureTheory.SigmaFinite (μ.trim ⋯)

      If each coordinate is measurable, then the tail σ-algebra is sigma-finite when the base measure is finite.

      Note: While this could be stated for general sigma-finite measures, we only need the finite case for de Finetti's theorem (which works with probability measures). The general sigma-finite case requires manual construction of spanning sets and is a mathlib gap.

      Helper lemmas for futureFiltration properties #

      source
      theorem Exchangeability.DeFinetti.ViaMartingale.futureFiltration_le {Ω : Type u_5} {α : Type u_6} [MeasurableSpace Ω] [MeasurableSpace α] (X : ℕ → Ω → α) (m : ℕ) (hX : ∀ (n : ℕ), Measurable (X n)) :
      futureFiltration X m ≤ inferInstance

      Future filtration is sub-σ-algebra of ambient.

      source
      theorem Exchangeability.DeFinetti.ViaMartingale.preimage_measurable_in_futureFiltration {Ω : Type u_5} {α : Type u_6} [MeasurableSpace Ω] [MeasurableSpace α] (X : ℕ → Ω → α) (m k : ℕ) (hk : 1 ≤ k) {A : Set α} (hA : MeasurableSet A) :
      MeasurableSet (X (m + k) ⁻¹' A)

      The preimage of a measurable set under X_{m+k} is measurable in futureFiltration X m. Note: This requires k ≥ 1 since futureFiltration X m = σ(X_{m+1}, X_{m+2}, ...).

      source
      theorem Exchangeability.DeFinetti.ViaMartingale.measurableSet_of_futureFiltration {Ω : Type u_5} {α : Type u_6} [MeasurableSpace Ω] [MeasurableSpace α] (X : ℕ → Ω → α) {m n : ℕ} (hmn : m ≤ n) {A : Set Ω} (hA : MeasurableSet A) :
      MeasurableSet A

      Events measurable in a future filtration remain measurable in earlier filtrations.