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

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_sub_log_stirlingSeq_succ (n : ℕ) : Real.log (stirlingSeq (n + 1)) - Real.log (stirlingSeq (n + 2)) ≤ 1 / (4 * ↑(n + 1) ^ 2)

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

theorem Stirling.log_stirlingSeq_bounded_aux : ∃ (c : ℝ), ∀ (n : ℕ), Real.log (stirlingSeq 1) - Real.log (stirlingSeq (n + 1)) ≤ c

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

theorem Stirling.log_stirlingSeq_bounded_by_constant : ∃ (c : ℝ), ∀ (n : ℕ), c ≤ 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. Sharper bounds due to Robbins are available, but are not yet formalised.

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. Sharper bounds due to Robbins are available, but are not yet formalised. These would add lower order terms (beginning with (12 * n)⁻¹) to the left-hand side.