OAI/NumberTheory/DukePrimeDegree/Dynamics/HopfMaximal.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The finite maximal ergodic inequality

The maximal recurrence estimate used in EKL (2006), Section 4.3, follows from this elementary finite Hopf inequality. The running maximum is built recursively, so its integrability and its coboundary bound require no pointwise ergodic theorem.

  1. def OAI.DukePrimeDegree.positiveRunningSum line 21
  2. lemma OAI.DukePrimeDegree.positiveRunningSum_nonneg line 25
  3. lemma OAI.DukePrimeDegree.positiveRunningSum_mono line 31
  4. lemma OAI.DukePrimeDegree.birkhoffSum_le_positiveRunningSum line 42
  5. lemma OAI.DukePrimeDegree.measurable_positiveRunningSum line 50
  6. lemma OAI.DukePrimeDegree.integrable_positiveRunningSum line 57
  7. theorem OAI.DukePrimeDegree.finite_hopf_maximal line 67

    Source documentation

    A finite running maximum has nonnegative signed mass on its positive set.

    theorem finite_hopf_maximal {Y : Type*} [MeasurableSpace Y]
    {μ : Measure Y} {T : Y → Y} {f : Y → ℝ}
    (hT : MeasurePreserving T μ μ) (hf : Integrable f μ)
    (hfmeas : Measurable f) (n : ℕ) :
    0 ≤ ∫ x in {x | 0 < positiveRunningSum T f n x}, f x ∂μ := by
…

    Mentions: OAI.DukePrimeDegree.positiveRunningSum