Main Convergence Theorems via L² Approach

This file contains the main L¹ convergence theorem for the L² proof of de Finetti's theorem. The directing measure itself and the packaging theorem directing_measure_satisfies_requirements now live in DirectingMeasureCore.lean and MoreL2Helpers.lean respectively.

Main results

• weighted_sums_converge_L1: Weighted sums converge in L¹ for contractable sequences

References

• Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Chapter 1, "Second proof of Theorem 1.1"

L¹ convergence via reverse martingale (main convergence theorem)

theorem Exchangeability.DeFinetti.ViaL2.weighted_sums_converge_L1 {Ω : 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) : ∃ (alpha : Ω → ℝ), Measurable alpha ∧ MeasureTheory.MemLp alpha 1 μ ∧ ∀ (n : ℕ), ∀ ε > 0, ∃ (M : ℕ), ∀ m ≥ M, ∫ (ω : Ω), |1 / ↑m * ∑ k : Fin m, f (X (n + ↑k + 1) ω) - alpha ω| ∂μ < ε

Weighted sums converge in L¹ for contractable sequences.

For a contractable sequence X and bounded measurable f, the Cesàro averages (1/m) * ∑_{i<m} f(X_{n+i+1}) converge in L¹ to a limit α : Ω → ℝ that does not depend on n.

This is the key convergence result needed for de Finetti's theorem via the L² approach. The proof uses L² contractability bounds to show the averages form a Cauchy sequence in L¹.