de Finetti's Theorem - L² Proof (Completed)

This file provides the completed L² proof of de Finetti's theorem by combining:

• ViaL2: Proves convergence A_n_m → α for each bounded f (Kallenberg Lemma 1.2)
• CommonEnding: Builds the kernel K from the map f ↦ α and completes the proof

This is Kallenberg's "second proof" (pages 26-27), which uses elementary L² contractability bounds and is the lightest-weight approach with minimal dependencies.

Proof architecture

The L² approach follows this structure:

1. ViaL2.weighted_sums_converge_L1: For contractable sequences X and bounded f, the weighted averages A_n_m(f∘X) = (1/m) Σᵢ f(X_{n+i+1}) converge in L¹ to a limit α_f : Ω → ℝ

2. Tail measurability: Each α_f is tail-measurable, i.e., measurable with respect to the tail σ-algebra (follows from contractability)

3. CommonEnding.conditional_iid_from_directing_measure: Given the family {α_f}, construct a directing measure ν : Ω → Measure ℝ such that:

   • ν is a probability kernel
   • ν is tail-measurable
   • X is conditionally i.i.d. given ν

This yields the three-way equivalence (Kallenberg Theorem 1.1):

• (i) X is contractable
• (ii) X is exchangeable
• (iii) X is conditionally i.i.d.

Alternative proofs

For other proof approaches, see:

• TheoremViaKoopman.lean: Proof via mean ergodic theorem
• TheoremViaMartingale.lean: Proof via reverse martingale convergence

References

• Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Theorem 1.1 (pages 26-27), "Second proof"

Main theorems (L² proof)

These are the user-facing theorems that complete Kallenberg Theorem 1.1. The actual proofs are in ViaL2.lean.

theorem Exchangeability.DeFinetti.deFinetti_RyllNardzewski_equivalence_viaL2 {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] (μ : 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

Kallenberg Theorem 1.1 (via L²): Contractable ⇔ (Exchangeable ∧ ConditionallyIID).

This is the completed three-way equivalence for real-valued sequences.

Proof structure:

• (i) → (iii): ViaL2 (L² contractability bounds) + CommonEnding
• (iii) → (ii): exchangeable_of_conditionallyIID (in ConditionallyIID.lean)
• (ii) → (i): contractable_of_exchangeable (in Contractability.lean)

Reference: Kallenberg (2005), Theorem 1.1 (pages 26-27), "Second proof".

theorem Exchangeability.DeFinetti.deFinetti_viaL2 {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] (μ : 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 (L² proof): Exchangeable ⇒ ConditionallyIID.

This is the standard statement of de Finetti's theorem for real-valued sequences.

Proof: Exchangeable → Contractable → ConditionallyIID via the L² approach.

Reference: Kallenberg (2005), Theorem 1.1.

theorem Exchangeability.DeFinetti.conditionallyIID_of_contractable_viaL2 {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] (μ : 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. (direct statement).

This is sometimes called the "contractable de Finetti" theorem.

Proof: Via L² bounds (Kallenberg Lemma 1.2) + CommonEnding.

Reference: Kallenberg (2005), page 27, "Second proof".