Finite Cylinder Machinery for Kallenberg Lemma 1.3

This file provides the finite approximation infrastructure for proving conditional independence from contractability.

Main definitions

• finFutureSigma X m k - Finite approximation of the future σ-algebra
• contractable_finite_cylinder_measure - Cylinder measure formula from contractability
• contractable_triple_pushforward - Triple pushforward equality
• join_eq_comap_pair_finFuture - σ-algebra join characterization

Strategy

We prove conditional independence by working with finite future approximations. The key insight is that contractability implies distributional equality for cylinder sets, which extends to the full σ-algebra via π-λ theorem.

Finite Future σ-Algebra

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

Finite future σ-algebra.

Approximates the infinite future σ(X_{m+1}, X_{m+2}, ...) by finite truncation.

Equations

• Exchangeability.DeFinetti.ViaMartingale.finFutureSigma X m k = MeasurableSpace.comap (fun (ω : Ω) (i : Fin k) => X (m + 1 + ↑i) ω) inferInstance

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

theorem Exchangeability.DeFinetti.ViaMartingale.finFutureSigma_le_futureFiltration {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ → Ω → α) (m k : ℕ) : finFutureSigma X m k ≤ futureFiltration X m

Cylinder Set Measure Formula

theorem Exchangeability.DeFinetti.ViaMartingale.contractable_finite_cylinder_measure {Ω : Type u_3} {α : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → α) (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) {r m k : ℕ} (hrm : r < m) (A : Fin r → Set α) (hA : ∀ (i : Fin r), MeasurableSet (A i)) (B : Set α) (hB : MeasurableSet B) (C : Fin k → Set α) (hC : ∀ (i : Fin k), MeasurableSet (C i)) : μ {ω : Ω | (∀ (i : Fin r), X (↑i) ω ∈ A i) ∧ X r ω ∈ B ∧ ∀ (j : Fin k), X (m + 1 + ↑j) ω ∈ C j} = μ {ω : Ω | (∀ (i : Fin r), X (↑i) ω ∈ A i) ∧ X r ω ∈ B ∧ ∀ (j : Fin k), X (r + 1 + ↑j) ω ∈ C j}

Cylinder set measure formula from contractability (finite approximation).

For contractable sequences with r < m, the measure of joint cylinder events involving the first r coordinates, coordinate r, and k future coordinates can be expressed using contractability properties.

This provides the distributional foundation for proving conditional independence in the finite approximation setting.

Triple Pushforward

theorem Exchangeability.DeFinetti.ViaMartingale.contractable_triple_pushforward {Ω : Type u_3} {α : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → α) (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) {r m k : ℕ} (hrm : r < m) : have Z_r := fun (ω : Ω) (i : Fin r) => X (↑i) ω; have Y_future := fun (ω : Ω) (j : Fin k) => X (m + 1 + ↑j) ω; have Y_tail := fun (ω : Ω) (j : Fin k) => X (r + 1 + ↑j) ω; MeasureTheory.Measure.map (fun (ω : Ω) => (Z_r ω, X r ω, Y_future ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (Z_r ω, X r ω, Y_tail ω)) μ

Contractability implies equality of the joint law of (X₀,…,X_{r-1}, X_r, X_{m+1}, …, X_{m+k}) and (X₀,…,X_{r-1}, X_r, X_{r+1}, …, X_{r+k}).

σ-Algebra Join Characterization

theorem Exchangeability.DeFinetti.ViaMartingale.join_eq_comap_pair_finFuture {Ω : Type u_3} {α : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] (X : ℕ → Ω → α) (r m k : ℕ) : PathSpace.firstRSigma X r ⊔ finFutureSigma X m k = MeasurableSpace.comap (fun (ω : Ω) => (fun (i : Fin r) => X (↑i) ω, fun (j : Fin k) => X (m + 1 + ↑j) ω)) inferInstance

Join with a finite future equals the comap of the paired map (Z_r, θ_future^k).