Reverse Filtration and Tail σ-Algebra

This file defines the reverse filtration (decreasing σ-algebras generated by shifts) and the tail σ-algebra (their intersection).

Main definitions

• revFiltration X m - σ(θₘ X) = σ(ω ↦ (n ↦ X (m+n) ω))
• tailSigma X - ⋂ₙ σ(Xₙ, Xₙ₊₁, ...), the tail σ-algebra

Main results

• revFiltration_le - revFiltration is a sub-σ-algebra of the ambient
• revFiltration_antitone - revFiltration is decreasing in m
• tailSigma_eq_canonical - matches Tail.tailProcess

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

Reverse Filtration

@[reducible, inline]

abbrev Exchangeability.DeFinetti.ViaMartingale.revFiltration {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ → Ω → α) (m : ℕ) : MeasurableSpace Ω

𝔽ₘ := σ(θₘ X) = σ(ω ↦ (n ↦ X (m+n) ω)).

Equations

• Exchangeability.DeFinetti.ViaMartingale.revFiltration X m = MeasurableSpace.comap (Exchangeability.DeFinetti.ViaMartingale.shiftRV X m) inferInstance

@[simp]

theorem Exchangeability.DeFinetti.ViaMartingale.revFiltration_zero {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ → Ω → α) : revFiltration X 0 = MeasurableSpace.comap (path X) inferInstance

theorem Exchangeability.DeFinetti.ViaMartingale.revFiltration_le {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (X : ℕ → Ω → α) (hX : ∀ (n : ℕ), Measurable (X n)) (m : ℕ) : revFiltration X m ≤ inferInstance

Tail σ-Algebra

def Exchangeability.DeFinetti.ViaMartingale.tailSigma {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ → Ω → α) : MeasurableSpace Ω

The tail σ-algebra for a process X: ⋂ₙ σ(Xₙ, Xₙ₊₁, ...).

Equations

• Exchangeability.DeFinetti.ViaMartingale.tailSigma X = ⨅ (m : ℕ), Exchangeability.DeFinetti.ViaMartingale.revFiltration X m

@[simp]

theorem Exchangeability.DeFinetti.ViaMartingale.tailSigma_eq_iInf_rev {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ → Ω → α) : tailSigma X = ⨅ (m : ℕ), revFiltration X m

theorem Exchangeability.DeFinetti.ViaMartingale.revFiltration_eq_tailFamily {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ → Ω → α) (m : ℕ) : revFiltration X m = ⨆ (k : ℕ), MeasurableSpace.comap (fun (ω : Ω) => X (m + k) ω) inferInstance

Bridge to canonical tail definition: ViaMartingale's revFiltration matches the pattern required by Tail.tailProcess_eq_iInf_revFiltration.

theorem Exchangeability.DeFinetti.ViaMartingale.tailSigma_eq_canonical {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ → Ω → α) : tailSigma X = Tail.tailProcess X

ViaMartingale's tailSigma equals the canonical Tail.tailProcess.

Monotonicity

theorem Exchangeability.DeFinetti.ViaMartingale.revFiltration_antitone {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (X : ℕ → Ω → α) : Antitone (revFiltration X)