Birkhoff Averages as Continuous Linear Maps

This file develops Birkhoff averages at the operator level, working entirely with continuous linear maps (CLMs) on Lp spaces. This avoids coercion issues that arise when mixing Lp-level and function-level operations.

Main definitions

• powCLM U k: The k-th iterate of a CLM U as a CLM
• birkhoffAvgCLM U n: The n-th Birkhoff average as a CLM

Main results

• powCLM_koopman_coe_ae: Iterating Koopman and coercing equals coercing and iterating (a.e.)
• birkhoffAvgCLM_coe_ae_eq_function_avg: CLM Birkhoff average equals function-level average (a.e.)

Implementation notes

This infrastructure solves the coercion mismatch issue where Lean distinguishes between:

• ↑↑(birkhoffAverage ℝ U (fun f => f) n g) (coerce the Lp average)
• birkhoffAverage ℝ U (fun f => ↑↑f) n g (average the coerced functions)

By working entirely at the CLM level and only coercing at the end, we avoid this issue.

def Exchangeability.Ergodic.powCLM {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (U : E →L[ℝ] E) : ℕ → E →L[ℝ] E

The k-th iterate of a continuous linear map, defined as a CLM.

Equations

• Exchangeability.Ergodic.powCLM U 0 = ContinuousLinearMap.id ℝ E
• Exchangeability.Ergodic.powCLM U k.succ = U.comp (Exchangeability.Ergodic.powCLM U k)

@[simp]

theorem Exchangeability.Ergodic.powCLM_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (U : E →L[ℝ] E) : powCLM U 0 = ContinuousLinearMap.id ℝ E

@[simp]

theorem Exchangeability.Ergodic.powCLM_succ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (U : E →L[ℝ] E) (k : ℕ) : powCLM U (k + 1) = U.comp (powCLM U k)

theorem Exchangeability.Ergodic.powCLM_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (U : E →L[ℝ] E) (k : ℕ) (v : E) : (powCLM U k) v = (⇑U)^[k] v

Lp Coercion Helper Lemmas

theorem Exchangeability.Ergodic.Lp.coeFn_smul' {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (c : ℝ) (f : ↥(MeasureTheory.Lp ℝ 2 μ)) : ↑↑(c • f) =ᵐ[μ] fun (ω : Ω) => c * ↑↑f ω

Coercion distributes through Lp scalar multiplication (a.e.).

theorem Exchangeability.Ergodic.Lp.coeFn_sum' {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {ι : Type u_3} [Fintype ι] (fs : ι → ↥(MeasureTheory.Lp ℝ 2 μ)) : ↑↑(∑ i : ι, fs i) =ᵐ[μ] fun (ω : Ω) => ∑ i : ι, ↑↑(fs i) ω

Coercion distributes through finite sums in Lp (a.e.).

theorem Exchangeability.Ergodic.EventuallyEq.sum' {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {ι : Type u_3} [Fintype ι] {fs gs : ι → Ω → ℝ} (h : ∀ (i : ι), fs i =ᵐ[μ] gs i) : (fun (ω : Ω) => ∑ i : ι, fs i ω) =ᵐ[μ] fun (ω : Ω) => ∑ i : ι, gs i ω

A.e. equality is preserved under finite sums.

def Exchangeability.Ergodic.birkhoffAvgCLM {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (U : E →L[ℝ] E) (n : ℕ) : E →L[ℝ] E

Birkhoff average as a continuous linear map.

Equations

• Exchangeability.Ergodic.birkhoffAvgCLM U n = if n = 0 then 0 else (↑n)⁻¹ • ∑ k : Fin n, Exchangeability.Ergodic.powCLM U ↑k

theorem Exchangeability.Ergodic.birkhoffAvgCLM_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (U : E →L[ℝ] E) : birkhoffAvgCLM U 0 = 0

theorem Exchangeability.Ergodic.birkhoffAvgCLM_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (U : E →L[ℝ] E) (n : ℕ) (v : E) : (birkhoffAvgCLM U n) v = if n = 0 then 0 else (↑n)⁻¹ • ∑ k : Fin n, (powCLM U ↑k) v

theorem Exchangeability.Ergodic.powCLM_koopman_coe_ae {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (T : Ω → Ω) (hT_meas : Measurable T) (hT_mp : MeasureTheory.MeasurePreserving T μ μ) (k : ℕ) (fL2 : ↥(MeasureTheory.Lp ℝ 2 μ)) : ↑↑((powCLM (koopman T hT_mp) k) fL2) =ᵐ[μ] fun (ω : Ω) => ↑↑fL2 (T^[k] ω)

For Lp spaces: iterating Koopman and then coercing equals coercing and then composing with T^[k] (almost everywhere).

theorem Exchangeability.Ergodic.birkhoffAvgCLM_coe_ae_eq_function_avg {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (T : Ω → Ω) (hT_meas : Measurable T) (hT_mp : MeasureTheory.MeasurePreserving T μ μ) (n : ℕ) (fL2 : ↥(MeasureTheory.Lp ℝ 2 μ)) : ↑↑((birkhoffAvgCLM (koopman T hT_mp) n) fL2) =ᵐ[μ] fun (ω : Ω) => if n = 0 then 0 else (↑n)⁻¹ * ∑ k : Fin n, ↑↑fL2 (T^[↑k] ω)

CLM Birkhoff average equals function-level average (almost everywhere).

This is the key lemma showing that coercing the Lp Birkhoff average equals averaging the coerced functions.

Strategy:

1. Unfold birkhoffAvgCLM and show coercion distributes through scalar mult and sum
2. For each k, use powCLM_koopman_coe_ae to show: ((powCLM (koopman T hT_mp) k) fL2 : Ω → ℝ) =ᵐ[μ] (fun ω => (fL2 : Ω → ℝ) (T^[k] ω))
3. Combine using a.e. equality for sums
4. Simplify scalar multiplication to regular multiplication

This lemma would resolve the coercion issues at ViaKoopman lines 3999-4051.