Convexity properties of the Gamma function #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.bohr_mollerup.tendsto_log_gamma_seq, 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.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
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.
n ↦ x log n + log n! - (log x + ... + log (x + n)), which we will show tends to
log (Gamma x) as
n → ∞.
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.