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 μ] [StandardBorelSpace α] (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 Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] {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.

theorem Exchangeability.DeFinetti.ViaKoopman.MeasurePreserving.iterate' {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] (hT : MeasureTheory.MeasurePreserving PathSpace.shift μ μ) (k : ℕ) : MeasureTheory.MeasurePreserving PathSpace.shift^[k] μ μ

Iterate of a measure-preserving map is measure-preserving.

theorem Exchangeability.DeFinetti.ViaKoopman.iterate_shift_eval' {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] (k n : ℕ) (ω : Ω[α]) : PathSpace.shift^[k] ω n = ω (k + n)

General evaluation formula for shift iteration.

theorem Exchangeability.DeFinetti.ViaKoopman.iterate_shift_eval0' {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] (k : ℕ) (ω : Ω[α]) : PathSpace.shift^[k] ω 0 = ω k

Evaluate the k-th shift at 0: shift^[k] ω 0 = ω k.

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_Step3b_L2_to_L1 {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] (hσ : MeasureTheory.MeasurePreserving PathSpace.shift μ μ) (fL2 : ↥(MeasureTheory.Lp ℝ 2 μ)) (hfL2_tendsto : Filter.Tendsto (fun (n : ℕ) => birkhoffAverage ℝ (⇑(Ergodic.koopman PathSpace.shift hσ)) (fun (f : ↥(MeasureTheory.Lp ℝ 2 μ)) => f) n fL2) Filter.atTop (nhds (condexpL2 fL2))) (B : ℕ → Ω[α] → ℝ) (Y : Ω[α] → ℝ) (hB_eq_pos : ∀ (n : ℕ), 0 < n → (fun (ω : Ω[α]) => ↑↑(birkhoffAverage ℝ (⇑(Ergodic.koopman PathSpace.shift hσ)) (fun (f : ↥(MeasureTheory.Lp ℝ 2 μ)) => f) n fL2) ω) =ᵐ[μ] B n) (hY_eq : (fun (ω : Ω[α]) => ↑↑(condexpL2 fL2) ω) =ᵐ[μ] Y) : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω[α]), |B n ω - Y ω| ∂μ) Filter.atTop (nhds 0)

On a probability space, L² convergence of Koopman–Birkhoff averages to condexpL2 implies L¹ convergence of chosen representatives. This version is robust to older mathlib snapshots (no Subtype.aestronglyMeasurable, no tendsto_iff_*, and snorm is fully qualified).

theorem Exchangeability.DeFinetti.ViaKoopman.optionB_Step4b_AB_close {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] (g : α → ℝ) (hg_meas : Measurable g) (Cg : ℝ) (hCg_bd : ∀ (x : α), |g x| ≤ Cg) (A B : ℕ → Ω[α] → ℝ) (hA_def : A = fun (n : ℕ) (ω : Ω[α]) => 1 / (↑n + 1) * ∑ j ∈ Finset.range (n + 1), g (ω j)) (hB_def : B = fun (n : ℕ) (ω : Ω[α]) => if n = 0 then 0 else 1 / ↑n * ∑ j ∈ Finset.range n, g (ω j)) : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω[α]), |A n ω - B n ω| ∂μ) Filter.atTop (nhds 0)

Step 4b helper: A_n and B_n differ negligibly.

For bounded g, shows |A_n ω - B_n ω| ≤ 2·Cg/(n+1) → 0 via dominated convergence.

theorem Exchangeability.DeFinetti.ViaKoopman.optionB_Step4c_triangle {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] (g : α → ℝ) (hg_meas : Measurable g) (hg_bd : ∃ (Cg : ℝ), ∀ (x : α), |g x| ≤ Cg) (A B : ℕ → Ω[α] → ℝ) (Y G : Ω[α] → ℝ) (hA_def : A = fun (n : ℕ) (ω : Ω[α]) => 1 / (↑n + 1) * ∑ j ∈ Finset.range (n + 1), g (ω j)) (hB_def : B = fun (n : ℕ) (ω : Ω[α]) => if n = 0 then 0 else 1 / ↑n * ∑ j ∈ Finset.range n, g (ω j)) (hG_int : MeasureTheory.Integrable G μ) (hY_int : MeasureTheory.Integrable Y μ) (hB_L1_conv : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω[α]), |B n ω - Y ω| ∂μ) Filter.atTop (nhds 0)) (hA_B_close : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω[α]), |A n ω - B n ω| ∂μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω[α]), |A n ω - Y ω| ∂μ) Filter.atTop (nhds 0)

Step 4c helper: Triangle inequality to combine convergences.

Given ∫|B_n - Y| → 0 and ∫|A_n - B_n| → 0, proves ∫|A_n - Y| → 0 via squeeze theorem.

theorem Exchangeability.DeFinetti.ViaKoopman.optionB_L1_convergence_bounded {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] (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.