OAI/NumberTheory/Ostmann/ZeroDensity/LogarithmicGammaBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic Gamma bound needed in the full-height zero-free region

The positive-strip digamma series gives a concrete logarithmic bound.

  1. theorem OAI.Ostmann.gammaReal_logarithmic_bound line 16
  2. theorem OAI.Ostmann.characterGamma_logarithmic_bound line 47