GammaSeq — Mathlib

English

Definition: Real.GammaSeq(s,n) = (n^s) n! / ∏_{j=0}^{n} (s + j).

Русский

Определение: Real.GammaSeq(s,n) = (n^s) n! / ∏_{j=0}^{n} (s + j).

LaTeX

$$$$ \GammaSeq(s,n) = \frac{n^{s} \; n!}{\prod_{j=0}^{n} (s + j)}. $$$$

Lean4

/-- The sequence with `n`-th term `n ^ s * n! / (s * (s + 1) * ... * (s + n))`, for real `s`. We
will show that this tends to `Γ(s)` as `n → ∞`. -/
noncomputable def GammaSeq (s : ℝ) (n : ℕ) :=
  (n : ℝ) ^ s * n ! / ∏ j ∈ Finset.range (n + 1), (s + j)

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