OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMovingGrowthWindow.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The same weak Hurwitz estimate controls all nearby character disks. Using radius R(2t)/16 leaves room for both the first and doubled heights.

  1. lemma OAI.TwoPointCorrelations.mrt_VKLog_pos line 13
  2. lemma OAI.TwoPointCorrelations.mrt_VKLog_double line 16
  3. lemma OAI.TwoPointCorrelations.mrt_VKRadius_double line 21
  4. lemma OAI.TwoPointCorrelations.mrt_moving_shifted_region line 24
  5. theorem OAI.TwoPointCorrelations.MRTWeakHurwitzGrowthInput.local_disks line 39

    Source documentation

    The actual nearby disks satisfy a common logarithmic growth budget; there is no independent regularity-in-height premise.

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

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