stirlingSeq — Mathlib

English

Define stirlingSeq(n) to be n! / (√(2n) (n/e)^n). This defines a sequence whose asymptotic behavior is governed by Stirling’s formula.

Русский

Определим stirlingSeq(n) как n! / (√(2n) (n/e)^n). Эта последовательность описывает асимпотику Стирлинга.

LaTeX

$$$\\operatorname{stirlingSeq}(n) = \\dfrac{n!}{\\sqrt{2n}\\left(\\dfrac{n}{e}\\right)^n}$$$

Lean4

/-- Define `stirlingSeq n` as $\frac{n!}{\sqrt{2n}(\frac{n}{e})^n}$.
Stirling's formula states that this sequence has limit $\sqrt(π)$.
-/
noncomputable def stirlingSeq (n : ℕ) : ℝ :=
  n ! / (√(2 * n : ℝ) * (n / exp 1) ^ n)

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