A uniform complex Stirling estimate in the right half-plane

Proved

ZudilinZeta.complex_stirling_right_half_plane

by tomasz · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisasymptoticscomplex-analysisgamma-functionzeta-values

For every complex number $w$ with $\operatorname{Re}w\ge1$ , the Gamma function satisfies

\left|\frac{\Gamma(w+1)\exp\!\left(w-(w+\tfrac12)\log w\right)}{\sqrt{2\pi}}-1\right| \le \exp\!\left(\frac{2}{\operatorname{Re}w}\right)-1.

Here $\log$ is the principal complex logarithm and the square root is the positive real one. The estimate is uniform in $\operatorname{Im}w$ . In particular, the normalized expression tends to $1$ whenever $\operatorname{Re}w$ tends to $+\infty$ .

This is a quantitative ingredient for the Gamma-factor asymptotics in Zudilin's saddle analysis. It does not assert the contour representation or the saddle-integral asymptotic.

Preamble

import Mathlib

Formal statement

theorem ZudilinZeta.complex_stirling_right_half_plane (w : ℂ) (hw : 1 ≤ w.re) :
    ‖Complex.Gamma (w + 1) *
      Complex.exp (-((w + 1 / 2) * Complex.log w - w)) /
      (Real.sqrt (2 * Real.pi) : ℂ) - 1‖ ≤ Real.exp (2 / w.re) - 1 := by sorry

Source

Derived auxiliary estimate for W. Zudilin, Arithmetic of linear forms involving odd zeta values, https://arxiv.org/abs/math/0206176, Lemma 20, printed p.33. The explicit constant is proved here, not quoted from that lemma. The proof uses Mathlib's factorial_isEquivalent_stirling and the platform's proved Zeta23 digamma-series and finite-remainder identities.

View graph