Convexity properties of the Gamma function #
In this file, we prove that
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
Real.BohrMollerup.tendsto_logGammaSeq, stating that for positive
x the sequence
x * log n + log n! - ∑ (m : ℕ) in Finset.range (n + 1), log (x + m)
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.BohrMollerup 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
Complex.Gamma_seq_tendsto_Gamma in the file
As an application of the Bohr-Mollerup theorem we prove the Legendre doubling formula for the
Gamma function for real positive
s (which will be upgraded to a proof for all complex
s in a
TODO: This argument can be extended to prove the general
k-multiplication formula (at least up
to a constant, and it should be possible to deduce the value of this constant using Stirling's
Log-convexity of the Gamma function on the positive reals (stated in multiplicative form), proved using the Hölder inequality applied to Euler's integral.
The Bohr-Mollerup theorem: the Gamma function is the unique log-convex, positive-valued
function on the positive reals which satisfies
f 1 = 1 and
f (x + 1) = x * f x for all
The Gamma doubling formula #
As a fun application of the Bohr-Mollerup theorem, we prove the Gamma-function doubling formula
(for positive real
s). The idea is that
2 ^ s * Gamma (s / 2) * Gamma (s / 2 + 1 / 2) is
log-convex and satisfies the Gamma functional equation, so it must actually be a constant
Gamma, and we can compute the constant by specialising at
s = 1.
Legendre's doubling formula for the Gamma function, for positive real arguments. Note that
we shall later prove this for all
Real.Gamma_mul_Gamma_add_half (superseding this result)
but this result is needed as an intermediate step.