OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterMovingCenter.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Normalization of Dirichlet L-functions on a moving disk. The radius is an explicit parameter; all characters, including the principal character, are allowed when the disk stays away from the real axis.

  1. def OAI.TwoPointCorrelations.mrtMovingPoint line 16
  2. def OAI.TwoPointCorrelations.mrtMovingLFunction line 19
  3. lemma OAI.TwoPointCorrelations.mrt_moving_point_ne_one line 24
  4. lemma OAI.TwoPointCorrelations.mrt_moving_point_center_ne_zero line 35
  5. lemma OAI.TwoPointCorrelations.mrt_moving_LFunction_zero line 47
  6. lemma OAI.TwoPointCorrelations.mrt_moving_LFunction_analytic line 51
  7. lemma OAI.TwoPointCorrelations.mrt_moving_LFunction_growth line 66
  8. lemma OAI.TwoPointCorrelations.mrt_moving_LFunction_deriv line 80
  9. lemma OAI.TwoPointCorrelations.mrt_moving_logderiv_eq line 94
  10. theorem OAI.TwoPointCorrelations.mrt_moving_logderiv_norm line 108

    Source documentation

    A separated normalized zero set bounds the actual logarithmic derivative. The factor 1/(3r) is the only cost of changing the disk radius.

    theorem mrt_moving_logderiv_norm (χ : 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)
    {z : ℂ} (hz : ‖z‖ ≤ 3 / 4)
    (hn : DirichletCharacter.LFunction χ (mrtMovingPoint r t z) ≠ 0)
    (hη : 0 < η)
    (hd : ∀ ρ ∈ mrtDiskZeros (mrtMovingLFunction χ r t), η ≤ ‖z - ρ‖) :
    ‖deriv (DirichletCharacter.LFunction χ) (mrtMovingPoint r t z) /
      DirichletCharacter.LFunction χ (mrtMovingPoint r t z)‖ ≤
      ((mrtCharacterLogDerivativeConstant +
        (1 / Real.log ((15 / 16 : ℝ) / (7 / 8))) / η) * B) / (3 * r) := by
…

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