Convexity properties of the Gamma function #

In this file, we prove that Gamma and log ∘ Gamma are convex functions on the positive real line. We then prove the Bohr-Mollerup theorem, which characterises Gamma as the unique positive-real-valued, log-convex function on the positive reals satisfying f (x + 1) = x f x and f 1 = 1.

The proof of the Bohr-Mollerup theorem is bound up with the proof of (a weak form of) the Euler limit formula, real.bohr_mollerup.tendsto_log_gamma_seq, stating that for positive real x the sequence x * log n + log n! - ∑ (m : ℕ) in finset.range (n + 1), log (x + m) tends to log Γ(x) as n → ∞. We prove that any function satisfying the hypotheses of the Bohr-Mollerup theorem must agree with the limit in the Euler limit formula, so there is at most one such function; then we show that Γ satisfies these conditions.

Since most of the auxiliary lemmas for the Bohr-Mollerup theorem are of no relevance outside the context of this proof, we place them in a separate namespace real.bohr_mollerup to avoid clutter. (This includes the logarithmic form of the Euler limit formula, since later we will prove a more general form of the Euler limit formula valid for any real or complex x; see real.Gamma_seq_tendsto_Gamma and complex.Gamma_seq_tendsto_Gamma in the file analysis.special_functions.gamma.beta.)