OAI/NumberTheory/Ostmann/ZeroDensity/GammaStripBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bounds for Gamma on the positive vertical strips used by the contour

  1. theorem OAI.Ostmann.gamma_norm_le_real line 12

    Source documentation

    The Euler integral bounds Gamma at a complex point by its real value.

    theorem gamma_norm_le_real (z : ℂ) (hz : 0 < z.re) :
    ‖Complex.Gamma z‖ ≤ Real.Gamma z.re := by
…
  2. theorem OAI.Ostmann.gamma_positive_strip_bound line 21