mathlib documentation

analysis.special_functions.stirling

Stirling's formula #

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 fraction sequence $a_n$ of fractions $\frac{n!}{\sqrt{2n}(\frac{n}{e})^n}$ and prove that this sequence converges against a real, positive number $a$. For this the two main ingredients are

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 the Wallis product.

Part 1 #

https://proofwiki.org/wiki/Stirling%27s_Formula#Part_1

noncomputable def stirling.stirling_seq (n : ) :

Define stirling_seq n as $\frac{n!}{\sqrt{2n}(\frac{n}{e})^n}$. Stirling's formula states that this sequence has limit $\sqrt(π)$.

Equations

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).

We have the bound log (stirling_seq n) - log (stirling_seq (n+1)) ≤ 1/(4 n^2)

For any n, we have log_stirling_seq 1 - log_stirling_seq n ≤ 1/4 * ∑' 1/k^2

The sequence log_stirling_seq is bounded below for n ≥ 1.

The sequence stirling_seq is positive for n > 0

The sequence stirling_seq has a positive lower bound.

The sequence stirling_seq ∘ succ is monotone decreasing

The limit a of the sequence stirling_seq satisfies 0 < a

Part 2 #

https://proofwiki.org/wiki/Stirling%27s_Formula#Part_2

noncomputable def stirling.w (n : ) :

For n : ℕ, define w n as 2^(4*n) * n!^4 / ((2*n)!^2 * (2*n + 1))

Equations

The sequence w n converges to π/2

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.

Suppose the sequence stirling_seq (defined above) has the limit a ≠ 0. Then the sequence w has limit a^2/2