GammaIntegral — Mathlib

English

Euler's integral for Γ(s) is defined as ΓIntegral(s) = ∫_0^∞ e^{-x} x^{s-1} dx.

Русский

Эйлеров интеграл для Γ(s) задаётся как ΓIntegral(s) = ∫_0^∞ e^{-x} x^{s-1} dx.

LaTeX

$$$$ \GammaIntegral(s) = \int_{0}^{\infty} e^{-x} x^{s-1} \, dx. $$$$

Lean4

/-- Euler's integral for the `Γ` function (of a complex variable `s`), defined as
`∫ x in Ioi 0, exp (-x) * x ^ (s - 1)`.

See `Complex.GammaIntegral_convergent` for a proof of the convergence of the integral for
`0 < re s`. -/
def GammaIntegral (s : ℂ) : ℂ :=
  ∫ x in Ioi (0 : ℝ), ↑(-x).exp * ↑x ^ (s - 1)

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