OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMovingSelectedZero.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A selected zero supplies its entire reciprocal horizontal distance in the shrinking-disk logarithmic derivative. This is the quantitative input for the three-factor positivity contradiction.

  1. lemma OAI.TwoPointCorrelations.mrt_disk_zero_multiplicity line 14
  2. lemma OAI.TwoPointCorrelations.mrt_moving_real_zero_mem line 28
  3. lemma OAI.TwoPointCorrelations.mrt_moving_selected_zero_sum line 39
  4. theorem OAI.TwoPointCorrelations.mrt_moving_neg_logderiv_of_zero line 75

    Source documentation

    The same bound with the full negative reciprocal of a selected zero.

    theorem mrt_moving_neg_logderiv_of_zero (χ : DirichletCharacter ℂ q)
    {r t B σ β : ℝ} (hr : 0 < r) (ht : 3 * r < |t|) (hB : 0 < B)
    (hg : ∀ z ∈ Metric.closedBall (0 : ℂ) (15 / 16),
      ‖mrtMovingLFunction χ r t z‖ ≤ Real.exp B)
    (hσ : 1 < σ) (hσ2 : σ ≤ 1 + r)
    (hβ : 1 - r / 4 ≤ β) (hβ1 : β ≤ 1)
    (hz : DirichletCharacter.LFunction χ ((β : ℂ) + Complex.I * (t : ℂ)) = 0) :
    (-deriv (DirichletCharacter.LFunction χ) ((σ : ℂ) + Complex.I * (t : ℂ)) /
      DirichletCharacter.LFunction χ ((σ : ℂ) + Complex.I * (t : ℂ))).re ≤
        mrtCharacterLogDerivativeConstant * B / (3 * r) - 1 / (σ - β) := by
…

    Mentions: OAI.TwoPointCorrelations.mrtMovingLFunction, OAI.TwoPointCorrelations.mrtCharacterLogDerivativeConstant