Cesàro L² Convergence: cesaro_to_condexp_L2

L² convergence of block Cesàro averages to the conditional expectation given the tail σ-algebra. Combines the Cauchy property from CesaroConvergence/Cauchy.lean with tail-measurability of the limit.

Main results

• cesaro_to_condexp_L2: L² convergence to the tail conditional expectation
• blockAvg_measurable_tailFamily: block averages are measurable w.r.t. tail σ-algebras

References

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

theorem Exchangeability.DeFinetti.ViaL2.blockAvg_measurable_tailFamily {Ω : Type u_3} [MeasurableSpace Ω] {f : ℝ → ℝ} (hf : Measurable f) {X : ℕ → Ω → ℝ} (m n : ℕ) : Measurable (blockAvg f X m n)

theorem Exchangeability.DeFinetti.ViaL2.cesaro_to_condexp_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) : ∃ (α_f : Ω → ℝ), MeasureTheory.MemLp α_f 2 μ ∧ MeasureTheory.AEStronglyMeasurable α_f μ ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (blockAvg f X 0 n - α_f) 2 μ) Filter.atTop (nhds 0) ∧ α_f =ᵐ[μ] μ[f ∘ X 0 | Tail.tailProcess X]

Cesàro averages converge in L² to a tail-measurable limit.

This is the elementary L² route to de Finetti (Kallenberg's "second proof"):

1. L² contractability bound → Cesàro averages are Cauchy in L²
2. Completeness of L² → limit α_f exists
3. Block averages A_{N,n} are σ(X_{>N})-measurable → α_f is tail-measurable
4. Tail measurability + L² limit → α_f = E[f(X_1) | tail σ-algebra]

No Mean Ergodic Theorem, no martingales - just elementary L² space theory!