OAI/NumberTheory/Ostmann/ZeroDensity/SharpDigammaStrip.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The leading logarithm of digamma on the required positive strip

The bounded remainder, rather than a multiple of the logarithm, preserves the correct length in the approximate functional equation for the fourth moment.

  1. theorem OAI.Ostmann.sharp_digamma_strip line 16