Documentation

Mathlib.Analysis.SpecialFunctions.Stirling

Stirling's formula #

This file proves Stirling's formula for the factorial. It states that n! grows asymptotically like 2πn(ne)n.

Proof outline #

The proof follows: https://proofwiki.org/wiki/Stirling%27s_Formula.

We proceed in two parts.

Part 1: We consider the sequence an of fractions n!2n(ne)n and prove that this sequence converges to 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 against a real number a and prove that a=π. 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 n!2n(ne)n. Stirling's formula states that this sequence has limit (π).

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

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

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

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

The sequence log_stirlingSeq is bounded below for 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.

The sequence stirlingSeq ∘ succ is monotone decreasing

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.

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

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