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: Clique_and_Monotone_Circuits, Comparison_Sort_Lower_Bound, Irrationals_From_THEBOOK, Lambert_W, Prime_Number_Theorem