log_stirlingSeq_formula — Mathlib

English

For any natural n, the logarithm of the Stirling sequence satisfies equation: log(stirlingSeq(n)) = log(n!) − (1/2) log(2n) − n log(n/e).

Русский

Для любого натурального n выполняется: log(stirlingSeq(n)) = log(n!) − (1/2) log(2n) − n log(n/e).

LaTeX

$$$\\log\\big(\\operatorname{stirlingSeq}(n)\\big) = \\log(n!) - \\tfrac{1}{2}\\log(2n) - n\\log\\left(\\dfrac{n}{e}\\right)$$$

Lean4

theorem log_stirlingSeq_formula (n : ℕ) :
    log (stirlingSeq n) = Real.log n ! - 1 / 2 * Real.log (2 * n) - n * log (n / exp 1) :=
  by
  cases n
  · simp
  · rw [stirlingSeq, log_div, log_mul, sqrt_eq_rpow, log_rpow, Real.log_pow, tsub_tsub] <;> positivity

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