OAI/NumberTheory/Ostmann/ZeroDensity/DirichletLogDerivativeBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A uniform Euler-series bound for real arguments

This part uses proved Mathlib theorems only: the continued zeta pole, the Euler logarithmic derivative, and the norm bound for Dirichlet characters.

  1. theorem OAI.Ostmann.residue_one_eq_vonMangoldt line 17
  2. theorem OAI.Ostmann.exists_vonMangoldt_series_bound line 22
  3. theorem OAI.Ostmann.dirichlet_logDerivative_le_vonMangoldt line 56
  4. theorem OAI.Ostmann.exists_dirichlet_logDerivative_bound line 88