GammaSeq — Mathlib

English

Define the nth term of the complex sequence by ΓSeq(s, n) = n^s · n! / ∏_{j=0}^{n} (s + j). Then ΓSeq(s, n) equals this explicit expression for all s and n.

Русский

Определим n-й член последовательности комплексного параметра s как ΓSeq(s, n) = n^s · n! / ∏_{j=0}^{n} (s + j). Тогда ΓSeq(s, n) равно этому явному выражению для всех s и n.

LaTeX

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

Lean4

/-- The sequence with `n`-th term `n ^ s * n! / (s * (s + 1) * ... * (s + n))`, for complex `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)

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