OAI/NumberTheory/Ostmann/ZeroDensity/GammaGrowthStrip.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Gamma-factor growth in the narrow strip around the contour

The upper bounds use only Euler's integral and reflection. They are needed for the horizontal-edge logarithmic-derivative estimate.

  1. theorem OAI.Ostmann.gammaReal_inverse_eq line 16
  2. theorem OAI.Ostmann.gammaReal_growth_bounds line 24