tendsto_partialGamma — Mathlib

English

As X → ∞, partialGamma(s,X) tends to GammaIntegral(s) for Re(s) > 0.

Русский

При X → ∞ частичная гамма-функция стремится к Γ(s) при Re(s) > 0.

LaTeX

$$$$ \lim_{X \to \infty} \text{partialGamma}(s,X) = \GammaIntegral(s) $$$$

Lean4

theorem tendsto_partialGamma {s : ℂ} (hs : 0 < s.re) :
    Tendsto (fun X : ℝ => partialGamma s X) atTop (𝓝 <| GammaIntegral s) :=
  intervalIntegral_tendsto_integral_Ioi 0 (GammaIntegral_convergent hs) tendsto_id

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