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

Also some global bounds on the factorial function and the Stirling sequence are proved.

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 against a real number $a$ and prove that $a = \sqrt{\pi}$. Here the main ingredient is the convergence of Wallis' product formula for π.

Part 1

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

noncomputable def Stirling.stirlingSeq (n : ℕ) : ℝ

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

@[simp]

theorem Stirling.stirlingSeq_zero : stirlingSeq 0 = 0

@[simp]

theorem Stirling.stirlingSeq_one : stirlingSeq 1 = Real.exp 1 / √2

theorem Stirling.log_stirlingSeq_formula (n : ℕ) : Real.log (stirlingSeq n) = Real.log ↑n.factorial - 1 / 2 * Real.log (2 * ↑n) - ↑n * Real.log (↑n / Real.exp 1)

theorem Stirling.log_stirlingSeq_diff_hasSum (m : ℕ) : HasSum (fun (k : ℕ) => 1 / (2 * ↑(k + 1) + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ (k + 1)) (Real.log (stirlingSeq (m + 1)) - Real.log (stirlingSeq (m + 2)))

The sequence log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)) has the series expansion ∑ 1 / (2 * (k + 1) + 1) * (1 / 2 * (m + 1) + 1)^(2 * (k + 1)).

theorem Stirling.log_stirlingSeq'_antitone : Antitone (Real.log ∘ stirlingSeq ∘ Nat.succ)

The sequence log ∘ stirlingSeq ∘ succ is monotone decreasing

@[deprecated "Use `log_stirlingSeq_diff_le` instead." (since := "2026-03-16")]

theorem Stirling.log_stirlingSeq_diff_le_geo_sum (n : ℕ) : Real.log (stirlingSeq (n + 1)) - Real.log (stirlingSeq (n + 2)) ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)

We have a bound for successive elements in the sequence log (stirlingSeq k).

theorem Stirling.log_stirlingSeq_diff_le (n : ℕ) : Real.log (stirlingSeq n) - Real.log (stirlingSeq (n + 1)) ≤ 1 / (12 * ↑n * (↑n + 1))

Robbins' sharp stepwise bound for the Stirling sequence: log (stirlingSeq n) - log (stirlingSeq (n+1)) ≤ 1 / (12 n (n + 1)).

@[deprecated "Use `log_stirlingSeq_diff_le` instead." (since := "2026-03-16")]

theorem Stirling.log_stirlingSeq_sub_log_stirlingSeq_succ (n : ℕ) : Real.log (stirlingSeq n) - Real.log (stirlingSeq (n + 1)) ≤ 1 / (4 * ↑n ^ 2)

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

theorem Stirling.log_stirlingSeq_bounded_aux (n : ℕ) : Real.log (stirlingSeq 1) - Real.log (stirlingSeq (n + 1)) ≤ 12⁻¹

For any n, we have log_stirlingSeq 1 - log_stirlingSeq n ≤ 12⁻¹.

theorem Stirling.log_stirlingSeq_bounded_by_constant (n : ℕ) : 1 - 12⁻¹ - Real.log 2 / 2 ≤ Real.log (stirlingSeq (n + 1))

The sequence log_stirlingSeq is bounded below for n ≥ 1.

theorem Stirling.stirlingSeq'_pos (n : ℕ) : 0 < stirlingSeq (n + 1)

The sequence stirlingSeq is positive for n > 0.

theorem Stirling.stirlingSeq'_bounded_by_pos_constant : ∃ (a : ℝ), 0 < a ∧ ∀ (n : ℕ), a ≤ stirlingSeq (n + 1)

The sequence stirlingSeq has a positive lower bound.

theorem Stirling.stirlingSeq'_antitone : Antitone (stirlingSeq ∘ Nat.succ)

The sequence stirlingSeq ∘ succ is monotone decreasing

theorem Stirling.stirlingSeq_has_pos_limit_a : ∃ (a : ℝ), 0 < a ∧ Filter.Tendsto stirlingSeq Filter.atTop (nhds a)

The limit a of the sequence stirlingSeq satisfies 0 < a

Part 2

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

theorem Stirling.tendsto_self_div_two_mul_self_add_one : Filter.Tendsto (fun (n : ℕ) => ↑n / (2 * ↑n + 1)) Filter.atTop (nhds (1 / 2))

The sequence n / (2 * n + 1) tends to 1/2

theorem Stirling.stirlingSeq_pow_four_div_stirlingSeq_pow_two_eq (n : ℕ) (hn : n ≠ 0) : stirlingSeq n ^ 4 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1)) = Real.Wallis.W n

For any n ≠ 0, we have the identity (stirlingSeq n)^4 / (stirlingSeq (2*n))^2 * (n / (2 * n + 1)) = W n, where W n is the n-th partial product of Wallis' formula for π / 2.

theorem Stirling.second_wallis_limit (a : ℝ) (hane : a ≠ 0) (ha : Filter.Tendsto stirlingSeq Filter.atTop (nhds a)) : Filter.Tendsto Real.Wallis.W Filter.atTop (nhds (a ^ 2 / 2))

Suppose the sequence stirlingSeq (defined above) has the limit a ≠ 0. Then the Wallis sequence W n has limit a^2 / 2.

theorem Stirling.tendsto_stirlingSeq_sqrt_pi : Filter.Tendsto stirlingSeq Filter.atTop (nhds √Real.pi)

Stirling's Formula

theorem Stirling.factorial_isEquivalent_stirling : Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => ↑n.factorial) fun (n : ℕ) => √(2 * ↑n * Real.pi) * (↑n / Real.exp 1) ^ n

Stirling's Formula, formulated in terms of Asymptotics.IsEquivalent.

Global bounds

theorem Stirling.sqrt_pi_le_stirlingSeq {n : ℕ} (hn : n ≠ 0) : √Real.pi ≤ stirlingSeq n

The Stirling sequence is bounded below by √π, for all positive naturals. Note that this bound holds for all n > 0, rather than for sufficiently large n: it is effective.

theorem Stirling.le_factorial_stirling (n : ℕ) : √(2 * Real.pi * ↑n) * (↑n / Real.exp 1) ^ n ≤ ↑n.factorial

Stirling's approximation gives a lower bound for n! for all n. The left-hand side is formulated to mimic the usual informal description of the approximation. See also factorial_isEquivalent_stirling which says these are asymptotically equivalent. That statement gives an upper bound also, but requires sufficiently large n. In contrast, this one is only a lower bound, but holds for all n. See also log_stirlingSeq_diff_le for Robbins' sharp bound on successive differences in the Stirling sequence.

theorem Stirling.le_log_factorial_stirling {n : ℕ} (hn : n ≠ 0) : ↑n * Real.log ↑n - ↑n + Real.log ↑n / 2 + Real.log (2 * Real.pi) / 2 ≤ Real.log ↑n.factorial

Stirling's approximation gives a lower bound for log n! for all positive n. The left-hand side is formulated in decreasing order in n: the higher order terms are first. This is a consequence of le_factorial_stirling, but is stated separately since the logarithmic version is sometimes more practical, and having this version eases algebraic calculations for applications. See also log_stirlingSeq_diff_le for Robbins' sharp bound of 1/(12k(k+1)) on successive differences in the Stirling sequence, which provides finer control over the convergence rate.