OAI/NumberTheory/TwoPoint/Fourier/ModFiveHighZeros.lean

GitHub source file

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.

  1. lemma OAI.TwoPointCorrelations.modFive_principal_neg_logderiv_re line 17

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveHighZeros.lean:17 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.modFive_square_logderiv_bound line 26

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveHighZeros.lean:26 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.modFive_zero_free_arithmetic line 68

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveHighZeros.lean:68 (same declaration text).

  4. 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/TwoPointCorrelations/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
…