OAI/NumberTheory/DukePrimeDegree/Geometry/DiscreteMaximal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform discrete orbit averages

The finite Hopf inequality bounds the union over all averaging lengths. The resulting measurable good set controls every positive integer time, as needed before passing to the continuous diagonal flow.

  1. theorem OAI.DukePrimeDegree.positiveRunningSum_measure_bound line 19
  2. theorem OAI.DukePrimeDegree.exists_discrete_average_good_set line 51

    Source documentation

    The complement of one measurable exceptional set controls all finite averages, with the sharp Hopf bound on its measure.

    theorem exists_discrete_average_good_set
    {Y : Type*} [MeasurableSpace Y] (μ : Measure Y) [IsFiniteMeasure μ]
    {T : Y → Y} (hT : MeasurePreserving T μ μ)
    {g : Y → ℝ} (hg : Integrable g μ) (hgmeas : Measurable g)
    (hgnonneg : ∀ x, 0 ≤ g x) (c : ℝ) (hc : 0 < c) :
    ∃ G : Set Y, MeasurableSet G ∧
      μ Gᶜ ≤ ENNReal.ofReal ((∫ x, g x ∂μ) / c) ∧
      ∀ x ∈ G, ∀ n : ℕ, birkhoffSum T g n x ≤ c * n := by
…