Functional equation of the gamma function

Remarks

For $\operatorname{Re} z > 0$, integration by parts in $\Gamma(z + 1) = \int_0^\infty t^{z} e^{-t} \, dt$ gives $z \int_0^\infty t^{z-1} e^{-t} \, dt$; the boundary terms vanish. Both sides are holomorphic on the connected set $\C \setminus \set{0, -1, -2, \ldots}$, so the identity theorem extends the equation from the half-plane to this set. Conversely the equation is the usual way to build the extension: for $\operatorname{Re} z > -n$ one sets $\Gamma(z) = \Gamma(z + n)/\big(z (z + 1) \cdots (z + n - 1)\big)$. With $\Gamma(1) = 1$ the equation gives $\Gamma(n + 1) = n!$, see the gamma function extends the factorial. For example $\Gamma(\tfrac32) = \tfrac12 \Gamma(\tfrac12) = \tfrac{\sqrt{\pi}}{2}$. In Mathlib the statement is Complex.Gamma_add_one.

Going deeper

For a student

The functional equation reduces the values of $\Gamma$ anywhere to its values on a strip of width one, such as $1 \le \operatorname{Re} z < 2$. It also shows where the poles are: dividing by $z$ at $z = 0$ creates a pole, and each further step to the left creates another. Together with log-convexity it characterizes $\Gamma$ on $(0, \infty)$, by the Bohr–Mollerup theorem, and together with boundedness on a strip it characterizes $\Gamma$ on the right half-plane, by Wielandt's theorem.