OAI/NumberTheory/Ostmann/ZeroDensity/VonMangoldtLogarithmicBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The zeta-pole upper bound with logarithmic dependence on height

  1. theorem OAI.Ostmann.regularizedZeta_logDeriv_lower line 12
  2. theorem OAI.Ostmann.exists_regularizedZeta_log_bound line 29
  3. theorem OAI.Ostmann.exists_vonMangoldt_logarithmic_upper line 68

    Source documentation

    Uniform zeta-pole estimate, without any zero-free-region assumption.

    theorem exists_vonMangoldt_logarithmic_upper : ∃ C : ℝ, 0 < C ∧
    ∀ s : ℂ, 1 < s.re → s.re ≤ 2 →
      (LSeries (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s).re ≤
        realZeroKernel (s.re - 1) s.im + C * Real.log (|s.im| + 2) := by
…

    Mentions: OAI.Ostmann.realZeroKernel