OAI/NumberTheory/DukePrimeDegree/Dynamics/DominatedAverages.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Moving sampling measures in ergodic averages

The sampling measure of a short orbit window can depend on the window. A uniform density bound is sufficient to pass an L1 error estimate to all these sampling measures at once, without a pointwise ergodic premise.

  1. lemma OAI.DukePrimeDegree.integral_sub_const_le_of_domination line 22
  2. theorem OAI.DukePrimeDegree.integral_tendsto_of_dominated_sampling line 46

    Source documentation

    An L1 ergodic-average error tends to zero under every sequence of probability sampling measures with the same density bound.

    theorem integral_tendsto_of_dominated_sampling
    (μ : Measure X) [IsFiniteMeasure μ]
    (ν : ℕ → Measure X) [∀ n, IsProbabilityMeasure (ν n)]
    (C c : ℝ) (hC : 0 ≤ C)
    (hdom : ∀ n, ν n ≤ ENNReal.ofReal C • μ)
    (F : ℕ → X → ℝ) (hF : ∀ n, Integrable (F n) μ)
    (hmean : Tendsto (fun n => ∫ x, |F n x - c| ∂μ) atTop (𝓝 0)) :
    Tendsto (fun n => ∫ x, F n x ∂ν n) atTop (𝓝 c) := by
…