Stirling's formula #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file proves Stirling's formula for the factorial. It states that $n!$ grows asymptotically like $\sqrt{2\pi n}(\frac{n}{e})^n$.
Proof outline #
The proof follows: https://proofwiki.org/wiki/Stirling%27s_Formula.
We proceed in two parts.
Part 1: We consider the sequence $a_n$ of fractions $\frac{n!}{\sqrt{2n}(\frac{n}{e})^n}$ and prove that this sequence converges to a real, positive number $a$. For this the two main ingredients are
- taking the logarithm of the sequence and
- using the series expansion of $\log(1 + x)$.
Part 2: We use the fact that the series defined in part 1 converges againt a real number $a$
and prove that $a = \sqrt{\pi}$. Here the main ingredient is the convergence of Wallis' product
formula for π.
We have the expression
log (stirling_seq (n + 1)) = log(n + 1)! - 1 / 2 * log(2 * n) - n * log ((n + 1) / e).
The sequence log (stirling_seq (m + 1)) - log (stirling_seq (m + 2)) has the series expansion
∑ 1 / (2 * (k + 1) + 1) * (1 / 2 * (m + 1) + 1)^(2 * (k + 1))
The sequence log ∘ stirling_seq ∘ succ is monotone decreasing
We have a bound for successive elements in the sequence log (stirling_seq k).
For any n, we have log_stirling_seq 1 - log_stirling_seq n ≤ 1/4 * ∑' 1/k^2
The sequence stirling_seq is positive for n > 0
The sequence stirling_seq ∘ succ is monotone decreasing
The limit a of the sequence stirling_seq satisfies 0 < a
The sequence n / (2 * n + 1) tends to 1/2
For any n ≠ 0, we have the identity
(stirling_seq n)^4 / (stirling_seq (2*n))^2 * (n / (2 * n + 1)) = W n, where W n is the
n-th partial product of Wallis' formula for π / 2.
Suppose the sequence stirling_seq (defined above) has the limit a ≠ 0.
Then the Wallis sequence W n has limit a^2 / 2.
Stirling's Formula