Log-convexity of the gamma function

Remarks

Write $t^{\lambda x + (1-\lambda) y - 1} e^{-t} = \big(t^{x-1}e^{-t}\big)^{\lambda}\big(t^{y-1}e^{-t}\big)^{1-\lambda}$ and apply Hölder's inequality with exponents $1/\lambda$ and $1/(1-\lambda)$ to Euler's integral; this gives the inequality. A second proof: the second derivative is $(\ln\Gamma)''(x) = \sum_{n \ge 0} \frac{1}{(x + n)^2} > 0$, so $\ln \Gamma$ is even strictly convex. Example: with $x = 1$, $y = 3$ and $\lambda = \tfrac12$ the inequality says $\Gamma(2) = 1 \le \sqrt{\Gamma(1)\Gamma(3)} = \sqrt{2}$. Log-convexity implies ordinary convexity of $\Gamma$, so $\Gamma$ has a single minimum on $(0, \infty)$, near $x \approx 1.4616$. In Mathlib the statement is Real.convexOn_log_Gamma.

Going deeper

For a student

Log-convexity is the property that singles out $\Gamma$ among all functions with $f(1) = 1$ and $f(x + 1) = x f(x)$: this is the Bohr–Mollerup theorem. It gives inequalities such as Gautschi's bounds for ratios $\Gamma(x + s)/\Gamma(x + 1)$. The positivity of $(\ln\Gamma)''$ says that the digamma function is strictly increasing on $(0, \infty)$.