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.BohrMollerup.tendsto_logGammaSeq, 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.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 x; see Real.Gamma_seq_tendsto_Gamma and Complex.Gamma_seq_tendsto_Gamma in the file Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean.)

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 ConvexOn.congr {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} {s : Set E} {f : E → β} {g : E → β} [OrderedSemiring 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 β] (hf : ConvexOn 𝕜 s f) (hfg : Set.EqOn f g s) : ConvexOn 𝕜 s g

theorem ConcaveOn.congr {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} {s : Set E} {f : E → β} {g : E → β} [OrderedSemiring 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 β] (hf : ConcaveOn 𝕜 s f) (hfg : Set.EqOn f g s) : ConcaveOn 𝕜 s g

theorem StrictConvexOn.congr {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} {s : Set E} {f : E → β} {g : E → β} [OrderedSemiring 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 β] (hf : StrictConvexOn 𝕜 s f) (hfg : Set.EqOn f g s) : StrictConvexOn 𝕜 s g

theorem StrictConcaveOn.congr {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} {s : Set E} {f : E → β} {g : E → β} [OrderedSemiring 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 β] (hf : StrictConcaveOn 𝕜 s f) (hfg : Set.EqOn f g s) : StrictConcaveOn 𝕜 s g

theorem ConvexOn.add_const {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} {s : Set E} {f : E → β} [OrderedSemiring 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 β] (hf : ConvexOn 𝕜 s f) (b : β) : ConvexOn 𝕜 s (f + fun (x : E) => b)

theorem ConcaveOn.add_const {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} {s : Set E} {f : E → β} [OrderedSemiring 𝕜] [SMul 𝕜 E] [AddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 β] (hf : ConcaveOn 𝕜 s f) (b : β) : ConcaveOn 𝕜 s (f + fun (x : E) => b)

theorem StrictConvexOn.add_const {𝕜 : Type u_1} {E : Type u_2} {s : Set E} [OrderedSemiring 𝕜] [SMul 𝕜 E] [AddCommMonoid E] {γ : Type u_4} {f : E → γ} [OrderedCancelAddCommMonoid γ] [Module 𝕜 γ] (hf : StrictConvexOn 𝕜 s f) (b : γ) : StrictConvexOn 𝕜 s (f + fun (x : E) => b)

theorem StrictConcaveOn.add_const {𝕜 : Type u_1} {E : Type u_2} {s : Set E} [OrderedSemiring 𝕜] [SMul 𝕜 E] [AddCommMonoid E] {γ : Type u_4} {f : E → γ} [OrderedCancelAddCommMonoid γ] [Module 𝕜 γ] (hf : StrictConcaveOn 𝕜 s f) (b : γ) : StrictConcaveOn 𝕜 s (f + fun (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) : (a * s + b * t).Gamma ≤ s.Gamma ^ a * t.Gamma ^ 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.convexOn_log_Gamma : ConvexOn ℝ (Set.Ioi 0) (Real.log ∘ Real.Gamma)

theorem Real.convexOn_Gamma : ConvexOn ℝ (Set.Ioi 0) Real.Gamma

def Real.BohrMollerup.logGammaSeq (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.BohrMollerup.logGammaSeq x n = x * (↑n).log + (↑n.factorial).log - (Finset.range (n + 1)).sum fun (m : ℕ) => (x + ↑m).log

theorem Real.BohrMollerup.f_nat_eq {f : ℝ → ℝ} {n : ℕ} (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + y.log) (hn : n ≠ 0) : f ↑n = f 1 + (↑(n - 1).factorial).log

theorem Real.BohrMollerup.f_add_nat_eq {f : ℝ → ℝ} {x : ℝ} (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + y.log) (hx : 0 < x) (n : ℕ) : f (x + ↑n) = f x + (Finset.range n).sum fun (m : ℕ) => (x + ↑m).log

theorem Real.BohrMollerup.f_add_nat_le {f : ℝ → ℝ} {x : ℝ} {n : ℕ} (hf_conv : ConvexOn ℝ (Set.Ioi 0) f) (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + y.log) (hn : n ≠ 0) (hx : 0 < x) (hx' : x ≤ 1) : f (↑n + x) ≤ f ↑n + x * (↑n).log

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

theorem Real.BohrMollerup.f_add_nat_ge {f : ℝ → ℝ} {x : ℝ} {n : ℕ} (hf_conv : ConvexOn ℝ (Set.Ioi 0) f) (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + y.log) (hn : 2 ≤ n) (hx : 0 < x) : f ↑n + x * (↑n - 1).log ≤ f (↑n + x)

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

theorem Real.BohrMollerup.logGammaSeq_add_one (x : ℝ) (n : ℕ) : Real.BohrMollerup.logGammaSeq (x + 1) n = Real.BohrMollerup.logGammaSeq x (n + 1) + x.log - (x + 1) * ((↑n + 1).log - (↑n).log)

theorem Real.BohrMollerup.le_logGammaSeq {f : ℝ → ℝ} {x : ℝ} (hf_conv : ConvexOn ℝ (Set.Ioi 0) f) (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + y.log) (hx : 0 < x) (hx' : x ≤ 1) (n : ℕ) : f x ≤ f 1 + x * (↑n + 1).log - x * (↑n).log + Real.BohrMollerup.logGammaSeq x n

theorem Real.BohrMollerup.ge_logGammaSeq {f : ℝ → ℝ} {x : ℝ} {n : ℕ} (hf_conv : ConvexOn ℝ (Set.Ioi 0) f) (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + y.log) (hx : 0 < x) (hn : n ≠ 0) : f 1 + Real.BohrMollerup.logGammaSeq x n ≤ f x

theorem Real.BohrMollerup.tendsto_logGammaSeq_of_le_one {f : ℝ → ℝ} {x : ℝ} (hf_conv : ConvexOn ℝ (Set.Ioi 0) f) (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + y.log) (hx : 0 < x) (hx' : x ≤ 1) : Filter.Tendsto (Real.BohrMollerup.logGammaSeq x) Filter.atTop (nhds (f x - f 1))

theorem Real.BohrMollerup.tendsto_logGammaSeq {f : ℝ → ℝ} {x : ℝ} (hf_conv : ConvexOn ℝ (Set.Ioi 0) f) (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + y.log) (hx : 0 < x) : Filter.Tendsto (Real.BohrMollerup.logGammaSeq x) Filter.atTop (nhds (f x - f 1))

theorem Real.BohrMollerup.tendsto_log_gamma {x : ℝ} (hx : 0 < x) : Filter.Tendsto (Real.BohrMollerup.logGammaSeq x) Filter.atTop (nhds x.Gamma.log)

theorem Real.eq_Gamma_of_log_convex {f : ℝ → ℝ} (hf_conv : ConvexOn ℝ (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.EqOn 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 : (3 / 2).Gamma < 1

theorem Real.Gamma_strictMonoOn_Ici : StrictMonoOn 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.

def Real.doublingGamma (s : ℝ) : ℝ

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

Equations

• s.doublingGamma = (s / 2).Gamma * (s / 2 + 1 / 2).Gamma * 2 ^ (s - 1) / Real.pi.sqrt

theorem Real.doublingGamma_add_one (s : ℝ) (hs : s ≠ 0) : (s + 1).doublingGamma = s * s.doublingGamma

theorem Real.doublingGamma_one : Real.doublingGamma 1 = 1

theorem Real.log_doublingGamma_eq : Set.EqOn (Real.log ∘ Real.doublingGamma) (fun (s : ℝ) => (s / 2).Gamma.log + (s / 2 + 1 / 2).Gamma.log + s * Real.log 2 - (2 * Real.pi.sqrt).log) (Set.Ioi 0)

theorem Real.doublingGamma_log_convex_Ioi : ConvexOn ℝ (Set.Ioi 0) (Real.log ∘ Real.doublingGamma)

theorem Real.doublingGamma_eq_Gamma {s : ℝ} (hs : 0 < s) : s.doublingGamma = s.Gamma

theorem Real.Gamma_mul_Gamma_add_half_of_pos {s : ℝ} (hs : 0 < s) : s.Gamma * (s + 1 / 2).Gamma = (2 * s).Gamma * 2 ^ (1 - 2 * s) * Real.pi.sqrt

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.