OAI/NumberTheory/DukePrimeDegree/Dynamics/OrbitCoboundary.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Bounded coboundary approximations to an orbit observable

The difference between a bounded observable and any one of its finite orbit averages is an explicit bounded coboundary. This is the uniform part of the maximal-inequality proof of a common generic set.

  1. def OAI.DukePrimeDegree.orbitAveragePotential line 21
  2. lemma OAI.DukePrimeDegree.sub_orbit_average_eq_coboundary line 24
  3. lemma OAI.DukePrimeDegree.birkhoffSum_abs_le line 41
  4. lemma OAI.DukePrimeDegree.orbitAveragePotential_abs_le line 50
  5. lemma OAI.DukePrimeDegree.orbit_average_coboundary_bound line 73

    Source documentation

    A bounded coboundary has a uniformly small Cesaro average.

    lemma orbit_average_coboundary_bound
    (T : X → X) (g : X → ℝ) (B : ℝ) (hg : ∀ x, |g x| ≤ B)
    (N : ℕ) (x : X) :
    |birkhoffAverage ℝ T (fun y => g y - g (T y)) N x| ≤
      (N : ℝ)⁻¹ * (2 * B) := by
…