ModFiveHighZeros.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The high-height logarithmic zero-free strip for nonprincipal characters modulo five. The zeta estimates are existing proved theorems; all character estimates come from the finite-period Abel bounds and the disk expansion.

lemma OAI.TwoPointCorrelations.modFive_principal_neg_logderiv_re line 17
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveHighZeros.lean:17 (same declaration text).
lemma OAI.TwoPointCorrelations.modFive_square_logderiv_bound line 26
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveHighZeros.lean:26 (same declaration text).
lemma OAI.TwoPointCorrelations.modFive_zero_free_arithmetic line 68
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveHighZeros.lean:68 (same declaration text).
theorem OAI.TwoPointCorrelations.modFive_nonprincipal_high_zero_free line 87
Source documentation
A uniform logarithmic zero-free strip at sufficiently large height. All constants are independent of the choice of nonprincipal character.
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveHighZeros.lean:87 (same declaration text).
```
theorem modFive_nonprincipal_high_zero_free : ∃ c : ℝ, 0 < c ∧ ∃ T : ℝ, 2 < T ∧
    ∀ (χ : DirichletCharacter ℂ 5), χ ≠ 1 → ∀ (t β : ℝ), T ≤ |t| →
      1 - c / Real.log (|t| + 2) ≤ β →
      DirichletCharacter.LFunction χ ((β : ℂ) + Complex.I * (t : ℂ)) ≠ 0 := by
…
```