logGammaSeq — Mathlib

English

For real s, GammaSeq(s,n) tends to Gamma(s) as n → ∞.

Русский

Для действительного s, GammaSeq(s,n) сходится к Gamma(s) при n → ∞.

LaTeX

$$$$ \lim_{n\to\infty} \GammaSeq(s,n) = \Gamma(s). $$$$

Lean4

/-- The function `n ↦ x log n + log n! - (log x + ... + log (x + n))`, which we will show tends to
`log (Gamma x)` as `n → ∞`. -/
def logGammaSeq (x : ℝ) (n : ℕ) : ℝ :=
  x * log n + log n ! - ∑ m ∈ Finset.range (n + 1), log (x + m)

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