7.8. Stirling's formula🔗

Mathlib has Stirling's formula for factorials (Stirling.tendsto_stirlingSeq_sqrt_pi) but not for \Gamma at half-integers; the asymptotics of v_d^{1/d}\sqrt d in Lemma 3.1.8 are therefore derived through an even/odd split in d. The report's gamma asymptotics (Stirling's expansion of \psi, uniform trigamma and polygamma bounds, the Malmstén–Binet representation of \log\Gamma, and \log|\Gamma(a+ib)| for |b| \to \infty) are correspondingly replaced by the elementary bounds \log(x-1) \le \psi(x) \le \log x (Lemma 3.1.6), explicit moment bounds for the gamma damping density (Lemma 5.3.12), the exponentiated Binet representation (Lemma 5.3.5) and polynomial decay of \Gamma along vertical lines.