L2ToL1Averages.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

L1 control of actual ergodic orbit averages

Probability normalization gives the L2-to-L1 bound with constant one. Combining it with the identified mean and the uniform-density transfer allows the sampling law of an orbit average to vary with its length.

lemma OAI.DukePrimeDegree.integral_norm_le_L2_norm line 22
lemma OAI.DukePrimeDegree.L1_tendsto_of_L2_tendsto_constant line 29

theorem OAI.DukePrimeDegree.L1_orbit_average_tendsto_integral line 47

Source documentation

The actual L2 Cesaro averages have vanishing L1 error from the original integral.

theorem L1_orbit_average_tendsto_integral
    (μ : Measure X) [IsProbabilityMeasure μ]
    (T : X → X) (hT : Ergodic T μ) (f : Lp ℝ 2 μ) :
    Tendsto (fun N => ∫ x,
      |(birkhoffAverage ℝ (Lp.compMeasurePreserving T hT.toMeasurePreserving) id N f) x -
        ∫ y, f y ∂μ| ∂μ) atTop (𝓝 0) :=
…

theorem OAI.DukePrimeDegree.dominated_orbit_average_tendsto_integral line 57

Source documentation

Uniformly dominated initial sampling laws have the same average limit even when their law changes at each averaging length.

theorem dominated_orbit_average_tendsto_integral
    (μ : Measure X) [IsProbabilityMeasure μ]
    (T : X → X) (hT : Ergodic T μ) (f : Lp ℝ 2 μ)
    (ν : ℕ → Measure X) [∀ n, IsProbabilityMeasure (ν n)]
    (C : ℝ) (hC : 0 ≤ C) (hdom : ∀ n, ν n ≤ ENNReal.ofReal C • μ) :
    Tendsto (fun N => ∫ x,
      (birkhoffAverage ℝ (Lp.compMeasurePreserving T hT.toMeasurePreserving) id N f) x ∂ν N)
      atTop (𝓝 (∫ x, f x ∂μ)) := by
…