OAI/NumberTheory/Ostmann/ZeroDensity/CharacterZeroFreeLogDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform logarithmic derivatives in the zero-free rectangle

One exceptional character is omitted. All other primitive characters have an explicit log-squared bound on the right-hand contour rectangle.

  1. theorem OAI.Ostmann.character_zero_free_logDeriv_data line 16
  2. theorem OAI.Ostmann.character_zero_free_logDeriv_bound line 93