ModFiveLogGrowth.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform logarithmic growth constants for the fixed disk estimate. These elementary inequalities expose a single constant independent of the character and the height, ready for the zero-free-region calculation.

lemma OAI.TwoPointCorrelations.modFiveLogDerivativeConstant_pos line 12
Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveLogGrowth.lean:12 (same declaration text).
lemma OAI.TwoPointCorrelations.modFive_log_height_pos line 17
Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveLogGrowth.lean:17 (same declaration text).
lemma OAI.TwoPointCorrelations.modFive_log_double_height line 20
Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveLogGrowth.lean:20 (same declaration text).
lemma OAI.TwoPointCorrelations.modFive_log_disk_growth line 29
Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveLogGrowth.lean:29 (same declaration text).

theorem OAI.TwoPointCorrelations.modFive_logderiv_growth_constant line 58

Source documentation

One absolute constant controls every nonprincipal modulus-five logarithmic derivative to the right of one.

Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveLogGrowth.lean:58 (same declaration text).

theorem modFive_logderiv_growth_constant : ∃ C : ℝ, 0 < C ∧
    ∀ (χ : DirichletCharacter ℂ 5), χ ≠ 1 → ∀ (t : ℝ) (σ : ℝ),
      1 < σ → σ ≤ 2 →
      (-deriv (DirichletCharacter.LFunction χ) ((σ : ℂ) + Complex.I * (t : ℂ)) /
        DirichletCharacter.LFunction χ ((σ : ℂ) + Complex.I * (t : ℂ))).re ≤
          C * Real.log (|t| + 2) ∧
      ∀ β : ℝ, 3 / 4 ≤ β → β ≤ 1 →
        DirichletCharacter.LFunction χ ((β : ℂ) + Complex.I * (t : ℂ)) = 0 →
        (-deriv (DirichletCharacter.LFunction χ) ((σ : ℂ) + Complex.I * (t : ℂ)) /
          DirichletCharacter.LFunction χ ((σ : ℂ) + Complex.I * (t : ℂ))).re ≤
            C * Real.log (|t| + 2) - 1 / (σ - β) := by
…