ModFiveZeroCount.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Jensen's bound for the total multiplicity in the fixed normalized disk. This counts actual zeros, with their analytic multiplicities, and will control the entire logarithmic derivative once a zero-free strip supplies distance.+

theorem OAI.TwoPointCorrelations.modFive_normalized_zero_count line 14
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveZeroCount.lean:14 (same declaration text).

theorem OAI.TwoPointCorrelations.modFive_normalized_logderiv_norm line 55

Source documentation

A distance lower bound controls every pole term at once.

Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveZeroCount.lean:55 (same declaration text).

theorem modFive_normalized_logderiv_norm (χ : DirichletCharacter ℂ 5)
    (hχ : χ ≠ 1) (t : ℝ) {z : ℂ} (hz : ‖z‖ ≤ 3 / 4)
    (hn : modFiveNormalizedLFunction χ t z ≠ 0) {η : ℝ} (hη : 0 < η)
    (hd : ∀ ρ ∈ modFiveNormalizedZeros χ t, η ≤ ‖z - ρ‖) :
    ‖deriv (modFiveNormalizedLFunction χ t) z / modFiveNormalizedLFunction χ t z‖ ≤
      (modFiveLogDerivativeConstant +
        (1 / Real.log ((15 / 16 : ℝ) / (7 / 8))) / η) *
          Real.log (8 * modFiveInverseConstant * (|t| + 4)) := by
…

Mentions: OAI.TwoPointCorrelations.modFiveNormalizedLFunction, OAI.TwoPointCorrelations.modFiveNormalizedZeros, OAI.TwoPointCorrelations.modFiveLogDerivativeConstant, OAI.TwoPointCorrelations.modFiveInverseConstant