OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMovingZeroTerms.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The one-zero de la Vallée Poussin estimate on a shrinking disk. All constants retain the physical radius and logarithmic growth budget.

  1. def OAI.TwoPointCorrelations.mrtMovingRealPoint line 15
  2. lemma OAI.TwoPointCorrelations.mrt_moving_real_point line 18
  3. lemma OAI.TwoPointCorrelations.mrt_moving_real_point_norm line 26
  4. lemma OAI.TwoPointCorrelations.mrt_moving_zero_physical line 37
  5. lemma OAI.TwoPointCorrelations.mrt_moving_zero_re line 43
  6. lemma OAI.TwoPointCorrelations.mrt_moving_zero_term_nonneg line 56
  7. theorem OAI.TwoPointCorrelations.mrt_moving_neg_logderiv line 73

    Source documentation

    Dropping the nonnegative zero terms gives an upper bound for -L'/L.

    theorem mrt_moving_neg_logderiv (χ : 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) :
    (-deriv (DirichletCharacter.LFunction χ) ((σ : ℂ) + Complex.I * (t : ℂ)) /
      DirichletCharacter.LFunction χ ((σ : ℂ) + Complex.I * (t : ℂ))).re ≤
        mrtCharacterLogDerivativeConstant * B / (3 * r) := by
…

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