Documentation

Mathlib.Analysis.SpecialFunctions.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$.

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

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

source
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(π)$.

Equations
Instances For
    source
    @[simp]
    theorem Stirling.stirlingSeq_zero :
    stirlingSeq 0 = 0
    source
    @[simp]
    theorem Stirling.stirlingSeq_one :
    stirlingSeq 1 = Real.exp 1 / √2
    source
    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)
    source
    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)).

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

    The sequence log ∘ stirlingSeq ∘ succ is monotone decreasing

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

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

    source
    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

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

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

    The sequence stirlingSeq is positive for n > 0

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

    The sequence stirlingSeq has a positive lower bound.

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

    The sequence stirlingSeq ∘ succ is monotone decreasing

    source
    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

    source
    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

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

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

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

    Stirling's Formula

    source
    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 #

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

    source
    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 approxmation. 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.

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