Stirling's formula

 

Title: Stirling's formula
Author: Manuel Eberl
Submission date: 2016-09-01
Abstract:

This work contains a proof of Stirling's formula both for the factorial $n! \sim \sqrt{2\pi n} (n/e)^n$ on natural numbers and the real Gamma function $\Gamma(x)\sim \sqrt{2\pi/x} (x/e)^x$. The proof is based on work by Graham Jameson.

This is then extended to the full asymptotic expansion $$\log\Gamma(z) = \big(z - \tfrac{1}{2}\big)\log z - z + \tfrac{1}{2}\log(2\pi) + \sum_{k=1}^{n-1} \frac{B_{k+1}}{k(k+1)} z^{-k}\\ {} - \frac{1}{n} \int_0^\infty B_n([t])(t + z)^{-n}\,\text{d}t$$ uniformly for all complex $z\neq 0$ in the cone $\text{arg}(z)\leq \alpha$ for any $\alpha\in(0,\pi)$, with which the above asymptotic relation for Γ is also extended to complex arguments.

BibTeX:
@article{Stirling_Formula-AFP,
  author  = {Manuel Eberl},
  title   = {Stirling's formula},
  journal = {Archive of Formal Proofs},
  month   = sep,
  year    = 2016,
  note    = {\url{https://isa-afp.org/entries/Stirling_Formula.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Bernoulli, Landau_Symbols
Used by: Comparison_Sort_Lower_Bound, Lambert_W, Prime_Number_Theorem