OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterDisk.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Fixed-radius logarithmic-derivative expansion for every nonprincipal Dirichlet L-function. The exact finite zero sum is retained and the growth cost is logarithmic in q * (abs(t)+4).

  1. def OAI.TwoPointCorrelations.mrtCharacterNormalizedZeros line 17
  2. lemma OAI.TwoPointCorrelations.mrtCharacterNormalizedZeros_finite line 20
  3. def OAI.TwoPointCorrelations.mrtCharacterLogDerivativeConstant line 30
  4. theorem OAI.TwoPointCorrelations.mrtCharacterNormalized_logderiv line 35

    Source documentation

    Exact finite zero-sum approximation on the inner disk.

    theorem mrtCharacterNormalized_logderiv (χ : DirichletCharacter ℂ q)
    (hχ : χ ≠ 1) (t : ℝ) {z : ℂ} (hz : ‖z‖ ≤ 3 / 4)
    (hn : mrtCharacterNormalizedLFunction χ t z ≠ 0) :
    ‖deriv (mrtCharacterNormalizedLFunction χ t) z / mrtCharacterNormalizedLFunction χ t z -
      ∑ ρ ∈ (mrtCharacterNormalizedZeros_finite χ hχ t).toFinset,
        (analyticOrderAt (mrtCharacterNormalizedLFunction χ t) ρ).toNat / (z - ρ)‖ ≤
      mrtCharacterLogDerivativeConstant *
        Real.log ((2 * q : ℝ) * mrtCharacterInverseConstant * (|t| + 4)) := by
…

    Mentions: OAI.TwoPointCorrelations.mrtCharacterNormalizedLFunction, OAI.TwoPointCorrelations.mrtCharacterNormalizedZeros_finite, OAI.TwoPointCorrelations.mrtCharacterLogDerivativeConstant, OAI.TwoPointCorrelations.mrtCharacterInverseConstant