OAI/NumberTheory/Ostmann/Characters/CharacterLogarithmicSeparation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A conductor-uniform logarithmic derivative estimate

The actual Hadamard difference and the positive reference zero sum control L'/L throughout the positive half-strip, with the explicit cost of the separation from all actual zeros.

  1. theorem OAI.Ostmann.character_logDeriv_logarithmic_separation line 17