L² to L¹ Cesàro Convergence Helpers

This file contains helper lemmas for L² to L¹ Cesàro convergence:

• condexpL2_ae_eq_condExp - connects L² conditional expectation to classical CE
• optionB_Step3b_L2_to_L1 - L² convergence implies L¹ convergence
• optionB_Step4b_AB_close - A_n and B_n differ negligibly
• optionB_Step4c_triangle - triangle inequality combining convergences
• optionB_L1_convergence_bounded - bounded case convergence implementation

This is part of "Option B" from the proof plan, avoiding the projected MET approach.

Option B: L¹ Convergence via Cylinder Functions

These lemmas implement the bounded and general cases for L¹ convergence of Cesàro averages using the cylinder function approach (Option B). This avoids MET and sub-σ-algebra typeclass issues.

theorem Exchangeability.DeFinetti.ViaKoopman.condexpL2_ae_eq_condExp {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] (f : ↥(MeasureTheory.Lp ℝ 2 μ)) : ↑↑(condexpL2 f) =ᵐ[μ] μ[↑↑f | shiftInvariantSigma]

Our condexpL2 operator agrees a.e. with classical conditional expectation.

Mathematical content: This is a standard fact in measure theory. Our condexpL2 is defined as:

condexpL2 := (lpMeas ℝ ℝ shiftInvariantSigma 2 μ).subtypeL.comp
             (MeasureTheory.condExpL2 ℝ ℝ shiftInvariantSigma_le)

The composition of mathlib's condExpL2 with the subspace inclusion subtypeL should equal the classical condExp a.e., since:

1. Mathlib's condExpL2 equals condExp a.e. (by MemLp.condExpL2_ae_eq_condExp)
2. The subspace inclusion preserves a.e. classes

Lean challenge: Requires navigating Lp quotient types and finding the correct API to convert between Lp ℝ 2 μ and MemLp _ 2 μ representations. The Lp.memℒp constant doesn't exist in the current mathlib API.

theorem Exchangeability.DeFinetti.ViaKoopman.eventuallyEq_comp_measurePreserving {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} {f g : Ω[α] → ℝ} (hT : MeasureTheory.MeasurePreserving PathSpace.shift μ μ) (hfg : f =ᵐ[μ] g) : f ∘ PathSpace.shift =ᵐ[μ] g ∘ PathSpace.shift

Pull a.e. equality back along a measure-preserving map. Standard fact: if f =ᵐ g and T preserves μ, then f ∘ T =ᵐ g ∘ T. Proof: Use QuasiMeasurePreserving.ae_eq_comp from mathlib.

Option B Helper Lemmas

These lemmas extract Steps 4a-4c from the main theorem to reduce elaboration complexity. Each lemma is self-contained with ~50-80 lines, well below timeout thresholds.

theorem Exchangeability.DeFinetti.ViaKoopman.optionB_L1_convergence_bounded {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] (hσ : MeasureTheory.MeasurePreserving PathSpace.shift μ μ) (g : α → ℝ) (hg_meas : Measurable g) (hg_bd : ∃ (Cg : ℝ), ∀ (x : α), |g x| ≤ Cg) : have A := fun (n : ℕ) (ω : Ω[α]) => 1 / (↑n + 1) * ∑ j ∈ Finset.range (n + 1), g (ω j); Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω[α]), |A n ω - μ[fun (ω : Ω[α]) => g (ω 0) | shiftInvariantSigma] ω| ∂μ) Filter.atTop (nhds 0)

Option B bounded case implementation: L¹ convergence for bounded functions.

For a bounded measurable function g : α → ℝ, the Cesàro averages A_n(ω) = (1/(n+1)) ∑_j g(ω j) converge in L¹ to CE[g(ω₀) | mSI]. Uses the fact that g(ω 0) is a cylinder function.