mathlib3 documentation

analysis.special_functions.gamma.bohr_mollerup

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

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

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

theorem convex_on.congr {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} {s : set E} {f g : E → β} [ordered_semiring 𝕜] [has_smul 𝕜 E] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 β] (hf : convex_on 𝕜 s f) (hfg : set.eq_on f g s) :

convex_on 𝕜 s g

theorem concave_on.congr {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} {s : set E} {f g : E → β} [ordered_semiring 𝕜] [has_smul 𝕜 E] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 β] (hf : concave_on 𝕜 s f) (hfg : set.eq_on f g s) :

concave_on 𝕜 s g

theorem strict_convex_on.congr {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} {s : set E} {f g : E → β} [ordered_semiring 𝕜] [has_smul 𝕜 E] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 β] (hf : strict_convex_on 𝕜 s f) (hfg : set.eq_on f g s) :

strict_convex_on 𝕜 s g

theorem strict_concave_on.congr {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} {s : set E} {f g : E → β} [ordered_semiring 𝕜] [has_smul 𝕜 E] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 β] (hf : strict_concave_on 𝕜 s f) (hfg : set.eq_on f g s) :

strict_concave_on 𝕜 s g

theorem convex_on.add_const {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} {s : set E} {f : E → β} [ordered_semiring 𝕜] [has_smul 𝕜 E] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 β] (hf : convex_on 𝕜 s f) (b : β) :

convex_on 𝕜 s (f + λ (_x : E), b)

theorem concave_on.add_const {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} {s : set E} {f : E → β} [ordered_semiring 𝕜] [has_smul 𝕜 E] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 β] (hf : concave_on 𝕜 s f) (b : β) :

concave_on 𝕜 s (f + λ (_x : E), b)

theorem strict_convex_on.add_const {𝕜 : Type u_1} {E : Type u_2} {s : set E} [ordered_semiring 𝕜] [has_smul 𝕜 E] [add_comm_monoid E] {γ : Type u_3} {f : E → γ} [ordered_cancel_add_comm_monoid γ] [module 𝕜 γ] (hf : strict_convex_on 𝕜 s f) (b : γ) :

strict_convex_on 𝕜 s (f + λ (_x : E), b)

theorem strict_concave_on.add_const {𝕜 : Type u_1} {E : Type u_2} {s : set E} [ordered_semiring 𝕜] [has_smul 𝕜 E] [add_comm_monoid E] {γ : Type u_3} {f : E → γ} [ordered_cancel_add_comm_monoid γ] [module 𝕜 γ] (hf : strict_concave_on 𝕜 s f) (b : γ) :

strict_concave_on 𝕜 s (f + λ (_x : E), b)

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.

theorem real.convex_on_log_Gamma :

convex_on ℝ (set.Ioi 0) (real.log ∘ real.Gamma)

theorem real.convex_on_Gamma :

convex_on ℝ (set.Ioi 0) real.Gamma

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

real.bohr_mollerup.log_gamma_seq x n = x * real.log ↑n + real.log ↑(n.factorial) - (finset.range (n + 1)).sum (λ (m : ℕ), real.log (x + ↑m))

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.log_gamma_seq_add_one (x : ℝ) (n : ℕ) :

real.bohr_mollerup.log_gamma_seq (x + 1) n = real.bohr_mollerup.log_gamma_seq x (n + 1) + real.log x - (x + 1) * (real.log (↑n + 1) - real.log ↑n)

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 : ℕ) :

f x ≤ f 1 + x * real.log (↑n + 1) - x * real.log ↑n + real.bohr_mollerup.log_gamma_seq x 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) :

f 1 + real.bohr_mollerup.log_gamma_seq x n ≤ f x

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

filter.tendsto (real.bohr_mollerup.log_gamma_seq x) filter.at_top (nhds (f x - f 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) :

filter.tendsto (real.bohr_mollerup.log_gamma_seq x) filter.at_top (nhds (f x - f 1))

theorem real.bohr_mollerup.tendsto_log_Gamma {x : ℝ} (hx : 0 < x) :

filter.tendsto (real.bohr_mollerup.log_gamma_seq x) filter.at_top (nhds (real.log (real.Gamma 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) :

set.eq_on f real.Gamma (set.Ioi 0)

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 :

real.Gamma 2 = 1

theorem real.Gamma_three_div_two_lt_one :

real.Gamma (3 / 2) < 1

theorem real.Gamma_strict_mono_on_Ici :

strict_mono_on real.Gamma (set.Ici 2)

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 multiple of Gamma, and we can compute the constant by specialising at s = 1.

noncomputable def real.doubling_Gamma (s : ℝ) :

Auxiliary definition for the doubling formula (we'll show this is equal to Gamma s)

Equations

s.doubling_Gamma = real.Gamma (s / 2) * real.Gamma (s / 2 + 1 / 2) * 2 ^ (s - 1) / √ real.pi

theorem real.doubling_Gamma_add_one (s : ℝ) (hs : s ≠ 0) :

(s + 1).doubling_Gamma = s * s.doubling_Gamma

theorem real.doubling_Gamma_one :

1.doubling_Gamma = 1

theorem real.log_doubling_Gamma_eq :

set.eq_on (real.log ∘ real.doubling_Gamma) (λ (s : ℝ), real.log (real.Gamma (s / 2)) + real.log (real.Gamma (s / 2 + 1 / 2)) + s * real.log 2 - real.log (2 * √ real.pi)) (set.Ioi 0)

theorem real.doubling_Gamma_log_convex_Ioi :

convex_on ℝ (set.Ioi 0) (real.log ∘ real.doubling_Gamma)

theorem real.doubling_Gamma_eq_Gamma {s : ℝ} (hs : 0 < s) :

s.doubling_Gamma = real.Gamma s

theorem real.Gamma_mul_Gamma_add_half_of_pos {s : ℝ} (hs : 0 < s) :

real.Gamma s * real.Gamma (s + 1 / 2) = real.Gamma (2 * s) * 2 ^ (1 - 2 * s) * √ real.pi

Legendre's doubling formula for the Gamma function, for positive real arguments. Note that we shall later prove this for all s as real.Gamma_mul_Gamma_add_half (superseding this result) but this result is needed as an intermediate step.