English
For all n, sqrt(2π n) (n/e)^n ≤ n!.
Русский
Для всех n выполняется sqrt(2π n) (n/e)^n ≤ n!.
LaTeX
$$$$ \sqrt{2\pi n}\left(\frac{n}{e}\right)^n \le n!. $$$$
Lean4
/-- 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.
-/
theorem le_factorial_stirling (n : ℕ) : √(2 * π * n) * (n / exp 1) ^ n ≤ n ! :=
by
obtain rfl | hn := eq_or_ne n 0
· simp
have : √(2 * π * n) * (n / exp 1) ^ n = √π * (√(2 * n) * (n / exp 1) ^ n) := by simp [sqrt_mul']; ring
rw [this, ← le_div_iff₀ (by positivity)]
exact sqrt_pi_le_stirlingSeq hn
