OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMovingGrowth.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Normalize the weak Hurwitz growth bound without losing a power of the height. The logarithmic disk budget is O(1+log q+loglog |t|), uniformly in q.

  1. def OAI.TwoPointCorrelations.mrtVKWeight line 13
  2. lemma OAI.TwoPointCorrelations.mrt_moving_growth_budget line 16
  3. lemma OAI.TwoPointCorrelations.mrt_VKWeight_ge_one line 53
  4. theorem OAI.TwoPointCorrelations.MRTWeakHurwitzGrowthInput.normalized_disk line 61

    Source documentation

    A weak Hurwitz bound gives the normalized moving-disk growth budget, with a single absolute small-radius threshold.

    theorem MRTWeakHurwitzGrowthInput.normalized_disk (h : MRTWeakHurwitzGrowthInput) :
    ∃ C T r₀ : ℝ, 0 < C ∧ 0 < T ∧ 0 < r₀ ∧ r₀ ≤ 1 / 5 ∧
      ∀ t : ℝ, T ≤ |t| → 1 ≤ mrtVKLog t → mrtVKRadius t ≤ r₀ →
      ∀ (q : ℕ) [NeZero q], ∀ (χ : DirichletCharacter ℂ q),
      ∀ z ∈ Metric.closedBall (0 : ℂ) (15 / 16),
        ‖mrtMovingLFunction χ (mrtVKRadius t) t z‖ ≤
          Real.exp (C * mrtVKWeight q t) := by
…

    Mentions: OAI.TwoPointCorrelations.MRTWeakHurwitzGrowthInput, OAI.TwoPointCorrelations.mrtVKLog, OAI.TwoPointCorrelations.mrtVKRadius, OAI.TwoPointCorrelations.mrtMovingLFunction, OAI.TwoPointCorrelations.mrtVKWeight