Cesàro Cauchy Property: blockAvg_cauchy_in_L2

Block Cesàro averages of a contractable sequence form a Cauchy sequence in L². This is the L²-side conclusion of Kallenberg's "second proof" — proved here via l2_contractability_bound (from L2Helpers.lean), avoiding the circular use of full exchangeability that kallenberg_L2_bound would require.

Main results

• blockAvg_cauchy_in_L2: Block averages form a Cauchy sequence in L² (used by CesaroConvergence.L2.cesaro_to_condexp_L2)
• blockAvgFrozen: Block average with a "frozen" denominator (helper for the Cauchy proof)

References

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

Performance wrappers to stop unfolding blockAvg inside eLpNorm

theorem Exchangeability.DeFinetti.ViaL2.blockAvg_cauchy_in_L2 {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → ℝ} (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (f : ℝ → ℝ) (hf_meas : Measurable f) (hf_bdd : ∀ (x : ℝ), |f x| ≤ 1) (ε : ENNReal) : ε > 0 → ∃ (N : ℕ), ∀ {n n' : ℕ}, n ≥ N → n' ≥ N → MeasureTheory.eLpNorm (fun (ω : Ω) => blockAvg f X 0 n ω - blockAvg f X 0 n' ω) 2 μ < ε

Block averages form a Cauchy sequence in L².

Given contractable X and bounded f, the block Cesàro averages blockAvg f X 0 n form a Cauchy sequence in L²(μ). The proof goes through the L² contractability bound (no full exchangeability assumed).