OAI/NumberTheory/Ostmann/ZeroDensity/GammaLogDerivativeBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A polynomial bound for the Gamma logarithmic derivative

Only the compact real strip [1/4,3/4] is needed. The proof combines the Euler-integral upper bound, the reflection lower bound, and the disk estimate.

  1. theorem OAI.Ostmann.gamma_logDeriv_strip_bound line 17

    Source documentation

    Linear growth is enough after multiplication by the eighth-order Mellin decay.

    theorem gamma_logDeriv_strip_bound : ∃ B : ℝ, 0 < B ∧ ∀ z : ℂ,
    (1 / 4 : ℝ) ≤ z.re → z.re ≤ 3 / 4 →
      ‖logDeriv Complex.Gamma z‖ ≤ B * (1 + |z.im|) := by
…