partialGamma — Mathlib

English

The partial Gamma function Γ(s, X) is defined by the integral from 0 to X: Γ(s, X) = ∫_0^X e^{-x} x^{s-1} dx.

Русский

Частичная гамма-функция Γ(s, X) задаётся интегралом ∫_0^X e^{-x} x^{s-1} dx.

LaTeX

$$$$ \text{partialGamma}(s,X) = \int_{0}^{X} e^{-x} x^{s-1} \, dx. $$$$

Lean4

/-- The indefinite version of the `Γ` function, `Γ(s, X) = ∫ x ∈ 0..X, exp(-x) x ^ (s - 1)`. -/
def partialGamma (s : ℂ) (X : ℝ) : ℂ :=
  ∫ x in 0..X, (-x).exp * x ^ (s - 1)

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