de Finetti's Theorem - Koopman/Ergodic Proof

This file provides the completed Koopman proof of de Finetti's theorem using ViaKoopman which proves conditional i.i.d. via block averaging and the Mean Ergodic Theorem.

This is Kallenberg's "first proof" (page 26), which uses the Mean Ergodic Theorem applied to the Koopman operator on L²(μ).

Proof architecture

The Koopman approach follows this structure:

1. ViaKoopman: Apply the Mean Ergodic Theorem to the Koopman operator U : L²(μ) → L²(μ) defined by (Uf)(ω) = f(shift(ω)).

   For contractable sequences, the shift operator preserves the measure μ (up to contractability), and ergodic theory gives convergence of Cesàro averages to the projection onto shift-invariant functions.

2. Tail measurability: The limit functions α_f are tail-measurable (shift-invariant functions live in the tail σ-algebra)

3. CommonEnding.conditional_iid_from_directing_measure: Given the family {α_f}, construct the directing measure ν and complete the proof

Dependencies

This approach requires:

• Mean Ergodic Theorem from mathlib (heavy ergodic theory dependencies)
• Koopman operator theory
• Connection between contractability and shift-invariance

References

• Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Theorem 1.1 (page 26), "First proof"
• Yosida (1980), Functional Analysis, Mean Ergodic Theorem

Main theorems (Koopman proof)

These theorems connect the general theory to the classical de Finetti result.

Status: The Koopman proof uses the Mean Ergodic Theorem approach. The key insight is that exchangeability implies full exchangeability (via exchangeable_iff_fullyExchangeable), which gives path measure exchangeability needed for the ergodic machinery.

theorem Exchangeability.DeFinetti.exchangeable_path_of_exchangeable {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hExch : Exchangeable μ X) (π : Equiv.Perm ℕ) : MeasureTheory.Measure.map (reindex π) (Bridge.μ_path μ X) = Bridge.μ_path μ X

Exchangeability of X implies exchangeability of the path measure μ_path.

This follows from exchangeable_iff_fullyExchangeable and fullyExchangeable_iff_pathLaw_invariant.

theorem Exchangeability.DeFinetti.deFinetti_RyllNardzewski_equivalence_viaKoopman {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) : Contractable μ X ↔ Exchangeable μ X ∧ ConditionallyIID μ X

theorem Exchangeability.DeFinetti.deFinetti_viaKoopman {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hX_exch : Exchangeable μ X) (hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) : ConditionallyIID μ X

De Finetti's Theorem (Koopman proof): Exchangeable ⇒ ConditionallyIID.

Reference: Kallenberg (2005), Theorem 1.1 (page 26), "First proof".

Proof: Direct proof using the Mean Ergodic Theorem approach:

1. Get contractability from exchangeability (for shift invariance)
2. Get path exchangeability from exchangeability (via fullyExchangeable)
3. Apply Koopman ergodic machinery
4. Transfer from path space to original space

theorem Exchangeability.DeFinetti.conditionallyIID_of_contractable_viaKoopman {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hContract : Contractable μ X) (hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) : ConditionallyIID μ X

Contractable implies conditionally i.i.d. (via Koopman).

Reference: Kallenberg (2005), page 26, "First proof".

Proof: Follows directly from the equivalence theorem.