OAI/NumberTheory/DukePrimeDegree/Geometry/HeightBoundaryCount.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Averaging the boundaries of shifted height bins

A natural height crosses exactly one of the q shifted bin boundaries when incremented by one. Integrating this identity controls boundary frequencies without requiring the height itself to be integrable.

  1. lemma OAI.DukePrimeDegree.sum_shifted_height_boundaries line 17
  2. def OAI.DukePrimeDegree.heightBoundary line 41
  3. lemma OAI.DukePrimeDegree.measurableSet_heightBoundary line 44
  4. theorem OAI.DukePrimeDegree.sum_heightBoundary_measures line 55
  5. theorem OAI.DukePrimeDegree.exists_shift_heightBoundary_le line 77
  6. lemma OAI.DukePrimeDegree.height_bin_change_subset line 94
  7. theorem OAI.DukePrimeDegree.exists_shift_rare_height_changes line 118

    Source documentation

    Coarse height bins can be shifted so their one-step changes have arbitrarily small probability, even when the height has infinite mean.

    theorem exists_shift_rare_height_changes
    (μ : Measure Y) [IsProbabilityMeasure μ] {T : Y → Y}
    (hT : MeasurePreserving T μ μ) (H : Y → ℕ) (hH : Measurable H)
    (hstep : ∀ x, H (T x) ≤ H x+1 ∧ H x ≤ H (T x)+1)
    (q : ℕ) (hq : 0 < q) :
    ∃ r < q, μ.real {x | (H (T x)+r)/q ≠ (H x+r)/q} ≤ 2/(q:ℝ) := by
…