ModFiveRightBound.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Absolute convergence bounds on the right Perron line. The twisted series is dominated term by term by the untwisted Mangoldt series, whose pole has the explicit reciprocal-distance bound.

lemma OAI.TwoPointCorrelations.modFive_mangoldt_norm line 15
Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveRightBound.lean:15 (same declaration text).
lemma OAI.TwoPointCorrelations.modFive_logderiv_right_domination line 22
Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveRightBound.lean:22 (same declaration text).

theorem OAI.TwoPointCorrelations.modFive_logderiv_right_bound line 55

Source documentation

A uniform right-line bound, valid for every character, with only the explicit simple-pole dependence on the distance from one.

Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveRightBound.lean:55 (same declaration text).

theorem modFive_logderiv_right_bound : ∃ C : ℝ, 0 < C ∧
    ∀ (χ : DirichletCharacter ℂ 5) (δ t : ℝ), 0 < δ →
      ‖-deriv (DirichletCharacter.LFunction χ) (((1 + δ : ℝ) : ℂ) + (t : ℂ) * Complex.I) /
        DirichletCharacter.LFunction χ (((1 + δ : ℝ) : ℂ) + (t : ℂ) * Complex.I)‖ ≤
          1 / δ + C := by
…