MRTCharacterHighZeros.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A classical logarithmic zero-free strip, uniform in the character modulus. This is the high-height part only; it makes no Vinogradov--Korobov claim.

lemma OAI.TwoPointCorrelations.mrt_character_principal_neg_logderiv_re line 16
lemma OAI.TwoPointCorrelations.mrt_character_square_logderiv_bound line 28
lemma OAI.TwoPointCorrelations.mrt_character_zero_free_arithmetic line 63

theorem OAI.TwoPointCorrelations.mrt_character_nonprincipal_high_zero_free line 83

Source documentation

Absolute constants give the usual logarithmic strip at high height, uniformly over all positive moduli and nonprincipal characters.

theorem mrt_character_nonprincipal_high_zero_free : ∃ c : ℝ, 0 < c ∧
    ∃ T : ℝ, 2 < T ∧ ∀ (q : ℕ) [NeZero q],
    ∀ (χ : DirichletCharacter ℂ q), χ ≠ 1 → ∀ (t beta : ℝ), T ≤ |t| →
      1 - c / mrtCharacterHeight q t ≤ beta →
      DirichletCharacter.LFunction χ ((beta : ℂ) + Complex.I * (t : ℂ)) ≠ 0 := by
…

Mentions: OAI.TwoPointCorrelations.mrtCharacterHeight