de Finetti's Theorem via L² Contractability

Kallenberg's "second proof" of de Finetti's theorem using the elementary L² contractability bound (Lemma 1.2). This is the lightest-dependency proof.

Proof approach

Starting from a contractable sequence ξ:

1. Fix a bounded measurable function f ∈ L¹
2. Use Lemma 1.2 (L² contractability bound) and completeness of L¹:
   • Show ‖E_m ∑{k=n+1}^{n+m} (f(ξ{n+k}) - α_{k-1})‖₁² → 0
3. Extract limit α_∞ = lim_n α_n in L¹
4. Show α_n is a reverse martingale (subsequence convergence a.s.)
5. Use contractability + dominated convergence:
   • E[f(ξ_i); ∩I_k] = E[α_{k-1}; ∩I_k] → E[α_∞; ∩I_k]
6. Conclude α_n = E_n f(ξ_{n+1}) = ν^f a.s.
7. Complete using the common ending (monotone class argument)

Main results

• deFinetti_viaL2: Main theorem - contractable implies conditionally i.i.d.
• deFinetti: Canonical name (alias for deFinetti_viaL2)

Supporting lemmas:

• weighted_sums_converge_L1: L² bound implies L¹ convergence
• reverse_martingale_limit: Tail-measurable limit via reverse martingale

Why this proof is default

✅ Elementary - Only uses basic L² space theory and Cauchy-Schwarz ✅ Direct - Proves convergence via explicit bounds ✅ Quantitative - Gives explicit rates of convergence ✅ Lightest dependencies - No ergodic theory required

References

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

Step 1: L² bound is the key tool

Covariance and Lp utility lemmas are now in L2Helpers.lean.

Covariance structure lemma

This auxiliary result characterizes the complete second-moment structure of contractable sequences. It's included here for use in applying l2_contractability_bound.

theorem Exchangeability.DeFinetti.ViaL2.contractable_covariance_structure {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) : ∃ (m : ℝ) (σSq : ℝ) (ρ : ℝ), (∀ (k : ℕ), ∫ (ω : Ω), X k ω ∂μ = m) ∧ (∀ (k : ℕ), ∫ (ω : Ω), (X k ω - m) ^ 2 ∂μ = σSq) ∧ (∀ (i j : ℕ), i ≠ j → ∫ (ω : Ω), (X i ω - m) * (X j ω - m) ∂μ = σSq * ρ) ∧ 0 ≤ σSq ∧ -1 ≤ ρ ∧ ρ ≤ 1

Uniform covariance structure for contractable L² sequences.

A contractable sequence X in L²(μ) has uniform second-moment structure:

• All X_i have the same mean m
• All X_i have the same variance σ²
• All distinct pairs (X_i, X_j) have the same covariance σ²·ρ
• The correlation coefficient satisfies |ρ| ≤ 1

This is proved using the Cauchy-Schwarz inequality and the fact that contractability forces all marginals of the same dimension to have identical distributions.

theorem Exchangeability.DeFinetti.ViaL2.l2_bound_two_windows_uniform {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (_hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (_hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) (f : ℝ → ℝ) (hf_meas : Measurable f) (hf_bdd : ∃ (M : ℝ), ∀ (x : ℝ), |f x| ≤ M) (Cf mf σSqf ρf : ℝ) (hCf_def : Cf = 2 * σSqf * (1 - ρf)) (_hCf_nonneg : 0 ≤ Cf) (hmean : ∀ (n : ℕ), ∫ (ω : Ω), f (X n ω) ∂μ = mf) (hvar : ∀ (n : ℕ), ∫ (ω : Ω), (f (X n ω) - mf) ^ 2 ∂μ = σSqf) (hcov : ∀ (n m : ℕ), n ≠ m → ∫ (ω : Ω), (f (X n ω) - mf) * (f (X m ω) - mf) ∂μ = σSqf * ρf) (hσSq_nonneg : 0 ≤ σSqf) (hρ_bd : -1 ≤ ρf ∧ ρf ≤ 1) (n m k : ℕ) : 0 < k → ∫ (ω : Ω), (1 / ↑k * ∑ i : Fin k, f (X (n + ↑i + 1) ω) - 1 / ↑k * ∑ i : Fin k, f (X (m + ↑i + 1) ω)) ^ 2 ∂μ ≤ Cf / ↑k

theorem Exchangeability.DeFinetti.ViaL2.get_covariance_constant {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) (f : ℝ → ℝ) (hf_meas : Measurable f) (hf_bdd : ∃ (M : ℝ), ∀ (x : ℝ), |f x| ≤ M) : ∃ (Cf : ℝ) (mf : ℝ) (σSqf : ℝ) (ρf : ℝ), Cf = 2 * σSqf * (1 - ρf) ∧ 0 ≤ Cf ∧ (∀ (n : ℕ), ∫ (ω : Ω), f (X n ω) ∂μ = mf) ∧ (∀ (n : ℕ), ∫ (ω : Ω), (f (X n ω) - mf) ^ 2 ∂μ = σSqf) ∧ (∀ (n m : ℕ), n ≠ m → ∫ (ω : Ω), (f (X n ω) - mf) * (f (X m ω) - mf) ∂μ = σSqf * ρf) ∧ 0 ≤ σSqf ∧ -1 ≤ ρf ∧ ρf ≤ 1

Compute the L² contractability constant for f ∘ X.

This helper extracts the common covariance structure computation needed by both l2_bound_two_windows_uniform and l2_bound_long_vs_tail.

Returns Cf = 2σ²(1-ρ) where (mf, σ², ρ) is the covariance structure of f ∘ X obtained from contractable_covariance_structure.

Design rationale: Computing the covariance structure once and passing it to both bound lemmas ensures they use the same constant, avoiding the need to prove equality of opaque existential witnesses.

theorem Exchangeability.DeFinetti.ViaL2.l2_bound_two_windows {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) (f : ℝ → ℝ) (hf_meas : Measurable f) (hf_bdd : ∃ (M : ℝ), ∀ (x : ℝ), |f x| ≤ M) (n m : ℕ) {k : ℕ} (hk : 0 < k) (_hdisj : Disjoint (window n k) (window m k)) : ∃ (Cf : ℝ), 0 ≤ Cf ∧ ∫ (ω : Ω), (1 / ↑k * ∑ i : Fin k, f (X (n + ↑i + 1) ω) - 1 / ↑k * ∑ i : Fin k, f (X (m + ↑i + 1) ω)) ^ 2 ∂μ ≤ Cf / ↑k

L² bound wrapper for two starting windows.

For contractable sequences, the L² difference between averages starting at different indices n and m is uniformly small. This gives us the key uniform bound we need.

NOTE: This wrapper is not used in the main proof. The uniform version with disjointness hypothesis is used instead. This wrapper is left for potential future use.

theorem Exchangeability.DeFinetti.ViaL2.l2_bound_long_vs_tail {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (_hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (_hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) (f : ℝ → ℝ) (hf_meas : Measurable f) (hf_bdd : ∃ (M : ℝ), ∀ (x : ℝ), |f x| ≤ M) (Cf mf σSqf ρf : ℝ) (hCf_def : Cf = 2 * σSqf * (1 - ρf)) (_hCf_nonneg : 0 ≤ Cf) (hmean : ∀ (n : ℕ), ∫ (ω : Ω), f (X n ω) ∂μ = mf) (hvar : ∀ (n : ℕ), ∫ (ω : Ω), (f (X n ω) - mf) ^ 2 ∂μ = σSqf) (hcov : ∀ (n m : ℕ), n ≠ m → ∫ (ω : Ω), (f (X n ω) - mf) * (f (X m ω) - mf) ∂μ = σSqf * ρf) (hσSq_nonneg : 0 ≤ σSqf) (hρ_bd : -1 ≤ ρf ∧ ρf ≤ 1) (n m k : ℕ) (hk : 0 < k) (hkm : k ≤ m) : ∫ (ω : Ω), (1 / ↑m * ∑ i : Fin m, f (X (n + ↑i + 1) ω) - 1 / ↑k * ∑ i : Fin k, f (X (n + (m - k) + ↑i + 1) ω)) ^ 2 ∂μ ≤ Cf / ↑k

Long average vs tail average bound: Comparing the average of the first m terms with the average of the last k terms (where k ≤ m) has the same L² contractability bound.

This is the key lemma needed to complete the Cauchy argument in weighted_sums_converge_L1.

Tail σ-algebra for sequences

Now using the canonical definitions from Exchangeability.Tail.TailSigma.

For backward compatibility in this file, we create a namespace with re-exports:

• TailSigma.tailFamily X n := Tail.tailFamily X n (future σ-algebra from index n onward)
• TailSigma.tailSigma X := Tail.tailProcess X (tail σ-algebra)

def Exchangeability.DeFinetti.ViaL2.TailSigma.tailFamily {Ω : Type u_3} {α : Type u_4} [MeasurableSpace α] (X : ℕ → Ω → α) (n : ℕ) : MeasurableSpace Ω

Re-export of Tail.tailFamily for backward compatibility.

Equations

• @Exchangeability.DeFinetti.ViaL2.TailSigma.tailFamily = @Exchangeability.Tail.tailFamily

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

Re-export of Tail.tailProcess for backward compatibility.

Equations

• @Exchangeability.DeFinetti.ViaL2.TailSigma.tailSigma = @Exchangeability.Tail.tailProcess

theorem Exchangeability.DeFinetti.ViaL2.TailSigma.antitone_tailFamily {Ω : Type u_3} {β : Type u_4} [MeasurableSpace Ω] [MeasurableSpace β] (X : ℕ → Ω → β) : Antitone (tailFamily X)

theorem Exchangeability.DeFinetti.ViaL2.TailSigma.tailSigma_le_tailFamily {Ω : Type u_3} {β : Type u_4} [MeasurableSpace Ω] [MeasurableSpace β] (X : ℕ → Ω → β) (n : ℕ) : tailSigma X ≤ tailFamily X n

theorem Exchangeability.DeFinetti.ViaL2.TailSigma.tailSigma_le {Ω : Type u_3} {β : Type u_4} [MeasurableSpace Ω] [MeasurableSpace β] (X : ℕ → Ω → β) (hX_meas : ∀ (i : ℕ), Measurable (X i)) : tailSigma X ≤ inferInstance

Helper axioms (early section)

Axioms that don't depend on later definitions can go here.

theorem Exchangeability.DeFinetti.ViaL2.Helpers.subseq_ae_of_L1 {Ω : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (alpha : ℕ → Ω → ℝ) (alpha_inf : Ω → ℝ) (h_alpha_meas : ∀ (n : ℕ), Measurable (alpha n)) (h_alpha_inf_meas : Measurable alpha_inf) (h_integrable : ∀ (n : ℕ), MeasureTheory.Integrable (fun (ω : Ω) => alpha n ω - alpha_inf ω) μ) (h_L1_conv : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ∫ (ω : Ω), |alpha n ω - alpha_inf ω| ∂μ < ε) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (k : ℕ) => alpha (φ k) ω) Filter.atTop (nhds (alpha_inf ω))

THEOREM (Subsequence a.e. convergence from L¹): If αₙ → α in L¹ (with measurability), there is a subsequence converging to α almost everywhere.

This follows from the standard result that L¹ convergence implies convergence in measure, and convergence in measure implies existence of an a.e. convergent subsequence.

Note: The complete alpha_is_conditional_expectation_packaged is in MoreL2Helpers.lean (at the ViaL2 namespace level, not Helpers). A stub was previously here but has been removed since it wasn't used in the critical path.