L¹ Cesàro Convergence for Bounded and Integrable Functions

This file contains:

• L1_cesaro_convergence_bounded - bounded case public lemma
• L1_cesaro_convergence - general integrable case via truncation
• ce_lipschitz_convergence - L¹ convergence through conditional expectation

theorem Exchangeability.DeFinetti.ViaKoopman.L1_cesaro_convergence_bounded {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {μ : 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)

L¹ Cesàro convergence for bounded functions.

For a bounded measurable function g : α → ℝ, the Cesàro averages A_n(ω) = (1/(n+1)) ∑_{j=0}^n g(ω_j) converge in L¹ to the conditional expectation μ[g(ω₀) | mSI].

This is a key ingredient for de Finetti's theorem via contractability.

theorem Exchangeability.DeFinetti.ViaKoopman.L1_cesaro_convergence {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] (hσ : MeasureTheory.MeasurePreserving PathSpace.shift μ μ) (g : α → ℝ) (hg_meas : Measurable g) (hg_int : MeasureTheory.Integrable (fun (ω : Ω[α]) => g (ω 0)) μ) : 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)

L¹ Cesàro convergence for integrable functions.

Extends the bounded case to general integrable functions by truncating g_M := max(min(g, M), -M), applying the bounded case to each g_M, and letting M → ∞ using dominated convergence.

theorem Exchangeability.DeFinetti.ViaKoopman.ce_lipschitz_convergence {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] (f g : α → ℝ) (hf_meas : Measurable f) (hf_bd : ∃ (Cf : ℝ), ∀ (x : α), |f x| ≤ Cf) (hg_meas : Measurable g) (hg_bd : ∃ (Cg : ℝ), ∀ (x : α), |g x| ≤ Cg) (h_L1_An_to_CE : 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)) : have A := fun (n : ℕ) (ω : Ω[α]) => 1 / (↑n + 1) * ∑ j ∈ Finset.range (n + 1), g (ω j); Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω[α]), |μ[fun (ω' : Ω[α]) => f (ω' 0) * A n ω'|shiftInvariantSigma] ω - μ[fun (ω' : Ω[α]) => f (ω' 0) * μ[fun (ω : Ω[α]) => g (ω 0)|shiftInvariantSigma] ω'|shiftInvariantSigma] ω| ∂μ) Filter.atTop (nhds 0)

CE Lipschitz convergence: Pull L¹ convergence through conditional expectation.

Given that A_n → CE[g(ω₀) | mSI] in L¹ and f is bounded, proves that CE[f·A_n | mSI] → CE[f·CE[g | mSI] | mSI] in L¹.