mathlib documentation

analysis.special_functions.gamma.bohr_mollerup

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.)

theorem real.Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma {s t a b : } (hs : 0 < s) (ht : 0 < t) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
real.Gamma (a * s + b * t) real.Gamma s ^ a * real.Gamma t ^ b

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.

noncomputable def real.bohr_mollerup.log_gamma_seq (x : ) (n : ) :

The function n ↦ x log n + log n! - (log x + ... + log (x + n)), which we will show tends to log (Gamma x) as n → ∞.

Equations
theorem real.bohr_mollerup.f_nat_eq {f : } {n : } (hf_feq : {y : }, 0 < y f (y + 1) = f y + real.log y) (hn : n 0) :
f n = f 1 + real.log ((n - 1).factorial)
theorem real.bohr_mollerup.f_add_nat_eq {f : } {x : } (hf_feq : {y : }, 0 < y f (y + 1) = f y + real.log y) (hx : 0 < x) (n : ) :
f (x + n) = f x + (finset.range n).sum (λ (m : ), real.log (x + m))
theorem real.bohr_mollerup.f_add_nat_le {f : } {x : } {n : } (hf_conv : convex_on (set.Ioi 0) f) (hf_feq : {y : }, 0 < y f (y + 1) = f y + real.log y) (hn : n 0) (hx : 0 < x) (hx' : x 1) :
f (n + x) f n + x * real.log n

Linear upper bound for f (x + n) on unit interval

theorem real.bohr_mollerup.f_add_nat_ge {f : } {x : } {n : } (hf_conv : convex_on (set.Ioi 0) f) (hf_feq : {y : }, 0 < y f (y + 1) = f y + real.log y) (hn : 2 n) (hx : 0 < x) :
f n + x * real.log (n - 1) f (n + x)

Linear lower bound for f (x + n) on unit interval

theorem real.bohr_mollerup.le_log_gamma_seq {f : } {x : } (hf_conv : convex_on (set.Ioi 0) f) (hf_feq : {y : }, 0 < y f (y + 1) = f y + real.log y) (hx : 0 < x) (hx' : x 1) (n : ) :
theorem real.bohr_mollerup.ge_log_gamma_seq {f : } {x : } {n : } (hf_conv : convex_on (set.Ioi 0) f) (hf_feq : {y : }, 0 < y f (y + 1) = f y + real.log y) (hx : 0 < x) (hn : n 0) :
theorem real.bohr_mollerup.tendsto_log_gamma_seq_of_le_one {f : } {x : } (hf_conv : convex_on (set.Ioi 0) f) (hf_feq : {y : }, 0 < y f (y + 1) = f y + real.log y) (hx : 0 < x) (hx' : x 1) :
theorem real.bohr_mollerup.tendsto_log_gamma_seq {f : } {x : } (hf_conv : convex_on (set.Ioi 0) f) (hf_feq : {y : }, 0 < y f (y + 1) = f y + real.log y) (hx : 0 < x) :
theorem real.eq_Gamma_of_log_convex {f : } (hf_conv : convex_on (set.Ioi 0) (real.log f)) (hf_feq : {y : }, 0 < y f (y + 1) = y * f y) (hf_pos : {y : }, 0 < y 0 < f y) (hf_one : f 1 = 1) :

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 x.

theorem real.Gamma_two  :