OrbitAverageFunctions.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Pointwise representatives of the orbit averages

The Hilbert-space Cesaro average agrees almost everywhere with the literal finite sum along the orbit. A bounded density transfers that agreement to a varying sampling law, so the dominated-average theorem applies to actual orbit samples.

lemma OAI.DukePrimeDegree.orbit_average_congr_ae line 22
lemma OAI.DukePrimeDegree.Lp_orbit_average_ae line 33
lemma OAI.DukePrimeDegree.Lp_orbit_average_ae_of_domination line 56

theorem OAI.DukePrimeDegree.actual_orbit_average_tendsto_integral line 65

Source documentation

A statement about the actual finite orbit sums, without any choice of representative for their Hilbert-space average.

theorem actual_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 ℝ T f N x ∂ν N)
      atTop (𝓝 (∫ x, f x ∂μ)) := by
…

theorem OAI.DukePrimeDegree.variable_orbit_average_tendsto_integral line 83

Source documentation

The window length may grow at any rate. Only divergence of the length and a uniform bound for the sampling densities are needed.

theorem variable_orbit_average_tendsto_integral
    (μ : Measure X) [IsProbabilityMeasure μ]
    (T : X → X) (hT : Ergodic T μ) (f : X → ℝ) (hf : MemLp f 2 μ)
    (ν : ℕ → Measure X) [∀ n, IsProbabilityMeasure (ν n)]
    (C : ℝ) (hC : 0 ≤ C) (hdom : ∀ n, ν n ≤ ENNReal.ofReal C • μ)
    (length : ℕ → ℕ) (hlength : Tendsto length atTop atTop) :
    Tendsto (fun n => ∫ x, birkhoffAverage ℝ T f (length n) x ∂ν n)
      atTop (𝓝 (∫ x, f x ∂μ)) := by
…