English
For all n ≠ 0, log n! ≥ n log n − n + (log n)/2 + (log(2π))/2.
Русский
Для всех n ≠ 0 логарифм n! не меньше n log n − n + (log n)/2 + (log(2π))/2.
LaTeX
$$$$ n\log n - n + \frac{\log n}{2} + \frac{\log (2\pi)}{2} \le \log n!. $$$$
Lean4
/-- 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.
-/
theorem le_log_factorial_stirling {n : ℕ} (hn : n ≠ 0) : n * log n - n + log n / 2 + log (2 * π) / 2 ≤ log n ! := by
calc
_ = (log (2 * π) + log n) / 2 + n * (log n - 1) := by ring
_ = log (√(2 * π * n) * (n / rexp 1) ^ n) := by
rw [log_mul (x := √_), log_sqrt, log_mul (x := 2 * π), log_pow, log_div, log_exp] <;> positivity
_ ≤ _ := log_le_log (by positivity) (le_factorial_stirling n)
