Gamma function

Definition

For a real number $s > 0$, the gamma function is $$\Gamma(s) = \int_0^\infty t^{s-1} e^{-t} \, dt.$$

Remarks

The improper integral converges at $0$ because $s > 0$, and at $\infty$ because $e^{-t}$ decays fast. Both claims follow from the comparison test. Integration by parts gives $\Gamma(s + 1) = s \, \Gamma(s)$. Also $\Gamma(1) = 1$, so $\Gamma$ extends the factorial. The function extends to all real numbers except $0, -1, -2, \dots$, by the recursion. Mathlib defines this extension as Real.Gamma. The notation $\Gamma$ is due to Adrien-Marie Legendre.

Explanations

L1 human

The gamma function is an integral that depends on a parameter $s$. At positive integers it gives factorials, so it interpolates the factorial.