Stirling's formula

Statement

As $n \to \infty$, $$n! \sim \sqrt{2 \pi n} \left( \frac{n}{e} \right)^n.$$ That is, the ratio $\frac{n!}{\sqrt{2 \pi n} \, (n/e)^n}$ tends to $1$.

Remarks

The relation $\sim$ is asymptotic equivalence. The absolute error grows, but the relative error tends to $0$. Comparing $\ln n! = \sum_{k \le n} \ln k$ with $\int_1^n \ln x \, dx$ gives the form $n! \sim C \sqrt{n} (n/e)^n$. The Wallis product gives $C = \sqrt{2\pi}$. A sharper form is $n! = \sqrt{2 \pi n} (n/e)^n \big(1 + \frac{1}{12 n} + O(n^{-2})\big)$. Mathlib states the limit as Stirling.tendsto_stirlingSeq_sqrt_pi.

History

Abraham de Moivre first stated a less precise form of the result. In 1730, James Stirling showed that the constant is $\sqrt{2\pi}$.

Explanations

L1 human

Stirling's formula gives the size of $n!$ for large $n$. For example, it gives $10! \approx 3.599 \times 10^6$, while $10! = 3628800$.