OAI/NumberTheory/Ostmann/ZeroDensity/LowHeightArchimedean.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform Gamma and zeta-pole errors in the low-height rectangle

  1. theorem OAI.Ostmann.gammaReal_logDeriv_rectangle_bound line 12
  2. theorem OAI.Ostmann.characterGamma_low_height_bound line 26
  3. theorem OAI.Ostmann.vonMangoldt_low_height_pole_error line 46

    Source documentation

    The pole remainder is uniformly bounded even when the evaluation point approaches one through the complex low-height rectangle.

    theorem vonMangoldt_low_height_pole_error : ∃ C : ℝ, 0 < C ∧
    ∀ s : ℂ, 1 < s.re → s.re ≤ 2 → |s.im| ≤ 2 →
      ‖LSeries (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s - (s - 1)⁻¹‖ ≤ C := by
…