factorial_isEquivalent_stirling — Mathlib

English

Stirling's formula (factorial is asymptotically equivalent to sqrt(2πn) (n/e)^n).

Русский

Формула Стирлинга: n! асимптотически эквивалентна sqrt(2πn) (n/e)^n.

LaTeX

$$$$ n! \sim \sqrt{2\pi n}\left(\frac{n}{e}\right)^n. $$$$

Lean4

/-- **Stirling's Formula**, formulated in terms of `Asymptotics.IsEquivalent`. -/
theorem factorial_isEquivalent_stirling :
    (fun n ↦ n ! : ℕ → ℝ) ~[atTop] fun n ↦ Real.sqrt (2 * n * π) * (n / exp 1) ^ n :=
  by
  refine Asymptotics.isEquivalent_of_tendsto_one ?_ ?_
  · filter_upwards [eventually_ne_atTop 0] with n hn h
    exact absurd h (by positivity)
  · have : sqrt π ≠ 0 := by positivity
    nth_rewrite 2 [← div_self this]
    convert tendsto_stirlingSeq_sqrt_pi.div tendsto_const_nhds this using 1
    ext n
    simp [field, stirlingSeq, mul_right_comm]

Похожие утверждения