GammaSeq_tendsto_Gamma — Mathlib

English

For any 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

/-- Euler's limit formula for the real Gamma function. -/
theorem GammaSeq_tendsto_Gamma (s : ℝ) : Tendsto (GammaSeq s) atTop (𝓝 <| Gamma s) :=
  by
  suffices Tendsto ((↑) ∘ GammaSeq s : ℕ → ℂ) atTop (𝓝 <| Complex.Gamma s) by
    exact (Complex.continuous_re.tendsto (Complex.Gamma ↑s)).comp this
  convert Complex.GammaSeq_tendsto_Gamma s
  ext1 n
  dsimp only [GammaSeq, Function.comp_apply, Complex.GammaSeq]
  push_cast
  rw [Complex.ofReal_cpow n.cast_nonneg, Complex.ofReal_natCast]

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