OAI/NumberTheory/Ostmann/ZeroDensity/LogDerivativeContourDisk.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The zero-free logarithmic-derivative bound up to the contour's left edge

  1. theorem OAI.Ostmann.logDeriv_norm_le_contour_disk line 12