ErgodicL2Averages.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

L2 averaging for the orbit-window argument

For an ergodic probability-preserving transformation, the Hilbert-space mean ergodic theorem has a constant limit. This supplies actual Cesaro averages, rather than an extra generic-point or averaging hypothesis.

theorem OAI.DukePrimeDegree.exists_constant_L2_orbit_average line 25

Source documentation

The Koopman fixed subspace of an ergodic map consists of constants, so its actual Cesaro averages converge in L2 to a constant.

theorem exists_constant_L2_orbit_average
    (μ : Measure X) [IsProbabilityMeasure μ]
    (T : X → X) (hT : Ergodic T μ) (f : Lp ℝ 2 μ) :
    ∃ c : ℝ, Tendsto
      (fun N => birkhoffAverage ℝ (Lp.compMeasurePreserving T hT.toMeasurePreserving)
        id N f) atTop
      (𝓝 ((memLp_const c : MemLp (fun _ : X => c) 2 μ).toLp (fun _ => c))) := by
…