Kallenberg's L² Bound (Lemma 1.2)

The L² distance bound for weighted averages of an exchangeable sequence — the "Lemma 1.2" of Kallenberg (2005). Self-contained algebraic statement; this file is not used by the rest of the ViaL2 proof (which proceeds through l2_contractability_bound to avoid the Exchangeable hypothesis), but it is the clean form of the original Kallenberg argument and is retained here for documentation.

Main results

• kallenberg_L2_bound: the L² distance bound, with full Exchangeable hypothesis

References

• Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Chapter 1, Lemma 1.2

Kallenberg's L² Approach (Lemma 1.2 + Second Proof)

This section implements Kallenberg's "second proof" of de Finetti's theorem using elementary L² bounds. The key is Lemma 1.2: for exchangeable sequences, weighted averages satisfy a simple variance bound that makes Cesàro averages Cauchy in L².

No ergodic theory is used - only:

1. Exchangeability → constant pairwise second moments
2. Algebraic identity for variance of weighted sums
3. Completeness of L²

This is the lightest-dependency route to de Finetti.

References:

• Kallenberg (2005), Probabilistic Symmetries, Chapter 1, pp. 27-28
  • Lemma 1.2 (L² bound for exchangeable weighted sums)
  • "Second proof of Theorem 1.1" (the L² route to de Finetti)

theorem Exchangeability.DeFinetti.ViaL2.kallenberg_L2_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (Z : ℕ → Ω → ℝ) (hZ_exch : Exchangeable μ Z) (hZ_meas : ∀ (i : ℕ), Measurable (Z i)) (p q : ℕ → ℝ) (s : Finset ℕ) (hs : s.Nonempty) (hp_prob : s.sum p = 1 ∧ ∀ i ∈ s, 0 ≤ p i) (hq_prob : s.sum q = 1 ∧ ∀ i ∈ s, 0 ≤ q i) (hZ_L2 : ∀ i ∈ s, MeasureTheory.MemLp (Z i) 2 μ) : ∫ (ω : Ω), (∑ i ∈ s, (p i - q i) * Z i ω) ^ 2 ∂μ ≤ (∫ (ω : Ω), (Z 0 ω - Z 1 ω) ^ 2 ∂μ) * s.sup' hs fun (i : ℕ) => |p i - q i|

Kallenberg's L² bound (Lemma 1.2) - Core of the elementary proof.

For an exchangeable sequence and centered variables Z_i := f(X_i) - E[f(X_1)], the L² distance between any two weighted averages satisfies:

‖∑ p_i Z_i - ∑ q_i Z_i‖²_L² ≤ C_f · sup_i |p_i - q_i|

where C_f := E[(Z_1 - Z_2)²].

Key application: For uniform block averages of length n, ‖A_{m,n} - A_{m',n}‖_L² ≤ √(C_f/n)

making the family {A_{m,n}}_m Cauchy in L² as n→∞.

Proof: Pure algebra + exchangeability:

1. Expand ‖∑ c_i Z_i‖² = ∑ c_i² E[Z_i²] + ∑_{i≠j} c_i c_j E[Z_i Z_j]
2. By exchangeability: E[Z_i²] = E[Z_1²], E[Z_i Z_j] = E[Z_1 Z_2] for i≠j
3. For c_i = p_i - q_i (differences of probability weights): ∑ c_i = 0
4. Algebraic bound: ∑ c_i² ≤ (∑|c_i|) · sup|c_i| ≤ 2 · sup|c_i|
5. Substitute and simplify to get the bound

This is exactly Kallenberg's Lemma 1.2. No ergodic theory needed!

Why this proof uses l2_contractability_bound instead of kallenberg_L2_bound

The Circularity Problem:

The de Finetti theorem we're proving establishes: Contractable ↔ Exchangeable

• contractable_of_exchangeable (✓ proved in Contractability.lean): Exchangeable → Contractable
• cesaro_to_condexp_L2 (this file): Contractable → Exchangeable (via conditionally i.i.d.)

Since we're trying to prove Contractable → Exchangeable, we cannot assume exchangeability in this proof - that would be circular!

Why kallenberg_L2_bound requires exchangeability:

kallenberg_L2_bound needs Exchangeable μ Z to establish uniform second moments:

• E[Z_i²] = E[Z_0²] for all i (uniform variance)
• E[Z_i Z_j] = E[Z_0 Z_1] for all i≠j (uniform pairwise covariance)

Exchangeability gives this via permutation invariance: swapping indices doesn't change the distribution.

Why contractability is insufficient for kallenberg_L2_bound:

Contractability only tells us about increasing subsequences:

• For any increasing k : Fin m → ℕ, the subsequence (Z_{k(0)}, ..., Z_{k(m-1)}) has the same distribution as (Z_0, ..., Z_{m-1})

This is weaker than exchangeability:

• ✓ We know (Z_0, Z_1) has same distribution as (Z_1, Z_2), (Z_2, Z_3), etc.
• ✗ We DON'T know (Z_0, Z_1) has same distribution as (Z_1, Z_0) - contractability doesn't give permutation invariance!

However: contractability DOES give uniform covariance!

Even though contractability ≠ exchangeability, contractability is sufficient for:

• E[Z_i²] = E[Z_0²] for all i (from the increasing subsequence {i})
• E[Z_i Z_j] = E[Z_0 Z_1] for all i<j (from the increasing subsequence {i,j})

This is exactly the covariance structure needed by l2_contractability_bound from L2Helpers.lean, which doesn't assume full exchangeability.

Note: By the end of this proof, we'll have shown Contractable → Exchangeable, so contractable sequences ARE exchangeable. But we can't use that equivalence while proving it - that would be begging the question!