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

• futureFiltration X m - σ(θ_{m+1} X) = σ(X_{m+1}, X_{m+2}, ...)
• tailSigmaFuture X - ⨅ m, futureFiltration X m (equals tailSigma X)

Main results

• futureFiltration_le - futureFiltration is a sub-σ-algebra of the ambient
• futureFiltration_antitone - futureFiltration is decreasing in m
• tailSigma_le_futureFiltration - tail is coarser than any future filtration
• tailSigmaFuture_eq_tailSigma - the two tail definitions coincide

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

Future Filtration Definition

@[reducible, inline]

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

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

Equations

• Exchangeability.DeFinetti.ViaMartingale.futureFiltration X m = MeasurableSpace.comap (Exchangeability.DeFinetti.ViaMartingale.shiftRV X (m + 1)) inferInstance

Future Filtration Properties

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

The future filtration is decreasing (antitone).

@[reducible]

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

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

Equations

• Exchangeability.DeFinetti.ViaMartingale.tailSigmaFuture X = ⨅ (m : ℕ), Exchangeability.DeFinetti.ViaMartingale.futureFiltration X m

@[simp]

theorem Exchangeability.DeFinetti.ViaMartingale.tailSigmaFuture_eq_iInf {Ω : Type u_3} {α : Type u_4} [MeasurableSpace α] (X : ℕ → Ω → α) : tailSigmaFuture X = ⨅ (m : ℕ), futureFiltration X m

@[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)

theorem Exchangeability.DeFinetti.ViaMartingale.tailSigmaFuture_eq_tailSigma {Ω : Type u_3} {α : Type u_4} [MeasurableSpace α] (X : ℕ → Ω → α) : tailSigmaFuture X = tailSigma X

Helper lemmas for tail σ-algebra

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.

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.

Helper lemmas for futureFiltration properties

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.