MRTCharacterZeroCount.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.mrt_character_normalized_zero_count line 16

theorem OAI.TwoPointCorrelations.mrt_character_normalized_logderiv_norm line 60

Source documentation

A distance lower bound controls every pole term at once.

theorem mrt_character_normalized_logderiv_norm (χ : DirichletCharacter ℂ q)
    (hχ : χ ≠ 1) (t : ℝ) {z : ℂ} (hz : ‖z‖ ≤ 3 / 4)
    (hn : mrtCharacterNormalizedLFunction χ t z ≠ 0) {η : ℝ} (hη : 0 < η)
    (hd : ∀ ρ ∈ mrtCharacterNormalizedZeros χ t, η ≤ ‖z - ρ‖) :
    ‖deriv (mrtCharacterNormalizedLFunction χ t) z / mrtCharacterNormalizedLFunction χ t z‖ ≤
      (mrtCharacterLogDerivativeConstant +
        (1 / Real.log ((15 / 16 : ℝ) / (7 / 8))) / η) *
          Real.log ((2 * q : ℝ) * mrtCharacterInverseConstant * (|t| + 4)) := by
…

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