Cesàro Helper Lemmas

Helper lemmas for the L¹ Cesàro convergence framework:

• condexp_precomp_iterate_eq - CE of shifted function equals CE of original
• shift_iterate_apply - evaluation formula for shift iteration
• cesaro_ce_eq_condexp - Cesàro average CE equals point CE
• condexp_product_eq_at_one - lag constancy for products
• product_ce_constant_of_lag_const - full lag constancy
• product_ce_constant_of_lag_const_from_one - tower from lag constancy

These lemmas are used by both the Cesàro convergence section and the kernel independence framework.

theorem Exchangeability.DeFinetti.ViaKoopman.condexp_precomp_iterate_eq {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] (hσ : MeasureTheory.MeasurePreserving PathSpace.shift μ μ) {k : ℕ} {f : Ω[α] → ℝ} (hf : MeasureTheory.Integrable f μ) : μ[fun (ω : Ω[α]) => f (PathSpace.shift^[k] ω)|shiftInvariantSigma] =ᵐ[μ] μ[f|shiftInvariantSigma]

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

theorem Exchangeability.DeFinetti.ViaKoopman.cesaro_ce_eq_condexp {α : 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) (n : ℕ) : μ[fun (ω : Ω[α]) => 1 / (↑n + 1) * ∑ j ∈ Finset.range (n + 1), g (ω j)|shiftInvariantSigma] =ᵐ[μ] μ[fun (ω : Ω[α]) => g (ω 0)|shiftInvariantSigma]

theorem Exchangeability.DeFinetti.ViaKoopman.condexp_product_eq_at_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] (hExch : ∀ (π : Equiv.Perm ℕ), MeasureTheory.Measure.map (reindex π) μ = μ) (f g : α → ℝ) (hf_meas : Measurable f) (hf_bd : ∃ (Cf : ℝ), ∀ (x : α), |f x| ≤ Cf) (hg_meas : Measurable g) (hg_bd : ∃ (Cg : ℝ), ∀ (x : α), |g x| ≤ Cg) (j : ℕ) (hj : 1 ≤ j) : μ[fun (ω : Ω[α]) => f (ω 0) * g (ω j)|shiftInvariantSigma] =ᵐ[μ] μ[fun (ω : Ω[α]) => f (ω 0) * g (ω 1)|shiftInvariantSigma]

Lag constancy chain for j ≥ 1: CE[f(ω₀)·g(ω_j)|ℐ] = CE[f(ω₀)·g(ω₁)|ℐ] for j ≥ 1.

This uses only k ≥ 1 lag constancy (avoiding the false k=0 case). The induction has base case j=1 (reflexivity) and step uses k = j-1 ≥ 1.

theorem Exchangeability.DeFinetti.ViaKoopman.product_ce_constant_of_lag_const {α : 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) (lag_const : ∀ (k : ℕ), μ[fun (ω : Ω[α]) => f (ω 0) * g (ω (k + 1))|shiftInvariantSigma] =ᵐ[μ] μ[fun (ω : Ω[α]) => f (ω 0) * g (ω k)|shiftInvariantSigma]) (n : ℕ) : have A := fun (ω : Ω[α]) => 1 / (↑n + 1) * ∑ j ∈ Finset.range (n + 1), g (ω j); μ[fun (ω : Ω[α]) => f (ω 0) * A ω|shiftInvariantSigma] =ᵐ[μ] μ[fun (ω : Ω[α]) => f (ω 0) * g (ω 0)|shiftInvariantSigma]

Section 2 helper: Product CE is constant in n under lag-constancy.

Given lag-constancy (CE[f·g_{k+1}] = CE[f·g_k] for all k), proves that CE[f·A_n | mSI] = CE[f·g₀ | mSI] for all n, where A_n is the Cesàro average.

This uses the lag-constancy hypothesis to collapse the sum termwise.

theorem Exchangeability.DeFinetti.ViaKoopman.product_ce_constant_of_lag_const_from_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] (hExch : ∀ (π : Equiv.Perm ℕ), MeasureTheory.Measure.map (reindex π) μ = μ) (f g : α → ℝ) (hf_meas : Measurable f) (hf_bd : ∃ (Cf : ℝ), ∀ (x : α), |f x| ≤ Cf) (hg_meas : Measurable g) (hg_bd : ∃ (Cg : ℝ), ∀ (x : α), |g x| ≤ Cg) (n : ℕ) (hn : 0 < n) : have A' := fun (ω : Ω[α]) => 1 / ↑n * ∑ j ∈ Finset.range n, g (ω (j + 1)); μ[fun (ω : Ω[α]) => f (ω 0) * A' ω|shiftInvariantSigma] =ᵐ[μ] μ[fun (ω : Ω[α]) => f (ω 0) * g (ω 1)|shiftInvariantSigma]

Product CE constant from index 1: CE[f·A'_n | mSI] = CE[f·g₁ | mSI] where A'n = (1/n)·Σ{j=1}^n g(ω_j) is the Cesàro average starting from index 1.

This avoids the false k=0 lag constancy by only using k ≥ 1. Each term CE[f·g_{j+1}] = CE[f·g₁] for j ∈ range n (so j+1 ≥ 1).