Euler integral for the gamma function

Remarks

Absolute convergence follows from $\abs{t^{s-1} e^{-t}} = t^{\sigma - 1} e^{-t}$ with $\sigma = \operatorname{Re} s > 0$, which is the real integrand. For holomorphy, the truncated integrals $\int_{1/n}^{n}$ are entire in $s$ and converge to $G$ uniformly on each strip $a \le \operatorname{Re} s \le b$ with $0 < a < b$, so the limit is holomorphic. Uniqueness comes from the identity theorem, since $(0, \infty)$ has accumulation points in the connected set $H$. The integral diverges at $t = 0$ when $\operatorname{Re} s \le 0$; the extension of $\Gamma$ beyond $H$ uses the functional equation $\Gamma(s + 1) = s\,\Gamma(s)$ instead. In Mathlib the statement is Complex.Gamma_eq_integral.

Going deeper

For a student

The integral is the gamma function's Mellin transform description: $\Gamma(s)$ is the Mellin transform of $e^{-t}$. Many identities, such as the formula linking the beta function with $\Gamma$, start from this integral and a change of variables. The integral alone only defines $\Gamma$ on the right half-plane; the meromorphic extension to $\C$ comes from the functional equation.