Theorems · Theorem · sequences and series

Stirling.le_log_factorial_stirling

∀ {n : ℕ}, 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. See also log_stirlingSeq_sdiff_le for Robbins' sharp bound of 1/(12k(k+1)) on successive differences in the Stirling sequence, which provides finer control over the convergence rate.

Defined in

Mathlib.Analysis.SpecialFunctions.Stirling

Cited by

0 results in Mathlib

Foundations

Depth 281 from the axioms · uses propext, Classical.choice, Quot.sound