# mathlibdocumentation

analysis.special_functions.gamma

# The Gamma and Beta functions #

This file defines the Γ function (of a real or complex variable s). We define this by Euler's integral Γ(s) = ∫ x in Ioi 0, exp (-x) * x ^ (s - 1) in the range where this integral converges (i.e., for 0 < s in the real case, and 0 < re s in the complex case).

We show that this integral satisfies Γ(1) = 1 and Γ(s + 1) = s * Γ(s); hence we can define Γ(s) for all s as the unique function satisfying this recurrence and agreeing with Euler's integral in the convergence range. (If s = -n for n ∈ ℕ, then the function is undefined, and we set it to be 0 by convention.)

## Tags #

Gamma

theorem integral_exp_neg_Ioi  :
(x : ) in , rexp (-x) = 1
theorem real.Gamma_integrand_is_o (s : ) :
(λ (x : ), rexp (-x) * x ^ s) =o[filter.at_top] λ (x : ), rexp (-(1 / 2) * x)

Asymptotic bound for the Γ function integrand.

The Euler integral for the Γ function converges for positive real s.

The integral defining the Γ function converges for complex s with 0 < re s.

This is proved by reduction to the real case.

noncomputable def complex.Gamma_integral (s : ) :

Euler's integral for the Γ function (of a complex variable s), defined as ∫ x in Ioi 0, exp (-x) * x ^ (s - 1).

See complex.Gamma_integral_convergent for a proof of the convergence of the integral for 0 < re s.

Equations

Now we establish the recurrence relation Γ(s + 1) = s * Γ(s) using integration by parts.

noncomputable def complex.partial_Gamma (s : ) (X : ) :

The indefinite version of the Γ function, Γ(s, X) = ∫ x ∈ 0..X, exp(-x) x ^ (s - 1).

Equations
theorem complex.partial_Gamma_add_one {s : } (hs : 0 < s.re) {X : } (hX : 0 X) :
(s + 1).partial_Gamma X = s * - (rexp (-X)) * X ^ s

The recurrence relation for the indefinite version of the Γ function.

theorem complex.Gamma_integral_add_one {s : } (hs : 0 < s.re) :

The recurrence relation for the Γ integral.

Now we define Γ(s) on the whole complex plane, by recursion.

noncomputable def complex.Gamma_aux  :

The nth function in this family is Γ(s) if -n < s.re, and junk otherwise.

Equations
theorem complex.Gamma_aux_recurrence1 (s : ) (n : ) (h1 : -s.re < n) :
= (s + 1) / s
theorem complex.Gamma_aux_recurrence2 (s : ) (n : ) (h1 : -s.re < n) :
noncomputable def complex.Gamma (s : ) :

The Γ function (of a complex variable s).

Equations
• = s
theorem complex.Gamma_eq_Gamma_aux (s : ) (n : ) (h1 : -s.re < n) :
theorem complex.Gamma_add_one (s : ) (h2 : s 0) :

The recurrence relation for the Γ function.

theorem complex.Gamma_eq_integral {s : } (hs : 0 < s.re) :
theorem complex.Gamma_zero  :

At 0 the Gamma function is undefined; by convention we assign it the value 0.

theorem complex.Gamma_neg_nat_eq_zero (n : ) :
= 0

At -n for n ∈ ℕ, the Gamma function is undefined; by convention we assign it the value 0.

Now check that the Γ function is differentiable, wherever this makes sense.

noncomputable def dGamma_integrand (s : ) (x : ) :

Integrand for the derivative of the Γ function

Equations
noncomputable def dGamma_integrand_real (s x : ) :

Integrand for the absolute value of the derivative of the Γ function

Equations
theorem dGamma_integrand_is_o_at_top (s : ) :
(λ (x : ), rexp (-x) * * x ^ (s - 1)) =o[filter.at_top] λ (x : ), rexp (-(1 / 2) * x)

Absolute convergence of the integral which will give the derivative of the Γ function on 1 < re s.

theorem loc_unif_bound_dGamma_integrand {t : } {s1 s2 x : } (ht1 : s1 t.re) (ht2 : t.re s2) (hx : 0 < x) :

A uniform bound for the s-derivative of the Γ integrand for s in vertical strips.

The derivative of the Γ integral, at any s ∈ ℂ with 1 < re s, is given by the integral of exp (-x) * log x * x ^ (s - 1) over [0, ∞).

theorem complex.differentiable_at_Gamma_aux (s : ) (n : ) (h1 : 1 - s.re < n) (h2 : (m : ), s -m) :
theorem complex.differentiable_at_Gamma (s : ) (hs : (m : ), s -m) :
noncomputable def real.Gamma (s : ) :

The Γ function (of a real variable s).

Equations
theorem real.Gamma_eq_integral {s : } (hs : 0 < s) :
= (x : ) in , rexp (-x) * x ^ (s - 1)
theorem real.Gamma_add_one {s : } (hs : s 0) :
real.Gamma (s + 1) = s *
theorem real.Gamma_one  :
= 1
theorem complex.Gamma_of_real (s : ) :
theorem real.Gamma_zero  :
= 0

At 0 the Gamma function is undefined; by convention we assign it the value 0.

At -n for n ∈ ℕ, the Gamma function is undefined; by convention we assign it the value 0.

theorem real.Gamma_pos_of_pos {s : } (hs : 0 < s) :
0 <
theorem real.Gamma_ne_zero {s : } (hs : (m : ), s -m) :
0

The Gamma function does not vanish on (except at non-positive integers, where the function is mathematically undefined and we set it to 0 by convention).

theorem real.Gamma_eq_zero_iff (s : ) :
= 0 (m : ), s = -m
theorem real.differentiable_at_Gamma {s : } (hs : (m : ), s -m) :
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) ^ a * ^ 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.

## The Bohr-Mollerup theorem #

In this section we prove two interrelated statements about the Γ function on the positive reals:

• 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 → ∞.
• the Bohr-Mollerup theorem (real.eq_Gamma_of_log_convex) which states that Γ is the unique log-convex, positive-real-valued function on the positive reals satisfying f (x + 1) = x f x and f 1 = 1.

To do this, 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.)

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 + ) (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 + ) (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 : (set.Ioi 0) f) (hf_feq : {y : }, 0 < y f (y + 1) = f y + ) (hn : n 0) (hx : 0 < x) (hx' : x 1) :
f (n + x) f n + x *

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

theorem real.bohr_mollerup.f_add_nat_ge {f : } {x : } {n : } (hf_conv : (set.Ioi 0) f) (hf_feq : {y : }, 0 < y f (y + 1) = f 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 : ) :
= + - (x + 1) * (real.log (n + 1) -
theorem real.bohr_mollerup.le_log_gamma_seq {f : } {x : } (hf_conv : (set.Ioi 0) f) (hf_feq : {y : }, 0 < y f (y + 1) = f y + ) (hx : 0 < x) (hx' : x 1) (n : ) :
f x f 1 + x * real.log (n + 1) - x * +
theorem real.bohr_mollerup.ge_log_gamma_seq {f : } {x : } {n : } (hf_conv : (set.Ioi 0) f) (hf_feq : {y : }, 0 < y f (y + 1) = f y + ) (hx : 0 < x) (hn : n 0) :
f x
theorem real.bohr_mollerup.tendsto_log_gamma_seq_of_le_one {f : } {x : } (hf_conv : (set.Ioi 0) f) (hf_feq : {y : }, 0 < y f (y + 1) = f y + ) (hx : 0 < x) (hx' : x 1) :
(nhds (f x - f 1))
theorem real.bohr_mollerup.tendsto_log_gamma_seq {f : } {x : } (hf_conv : (set.Ioi 0) f) (hf_feq : {y : }, 0 < y f (y + 1) = f y + ) (hx : 0 < x) :
(nhds (f x - f 1))
theorem real.bohr_mollerup.tendsto_log_Gamma {x : } (hx : 0 < x) :
theorem real.eq_Gamma_of_log_convex {f : } (hf_conv : (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.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  :
= 1

## The Beta function #

noncomputable def complex.beta_integral (u v : ) :

The Beta function Β (u, v), defined as ∫ x:ℝ in 0..1, x ^ (u - 1) * (1 - x) ^ (v - 1).

Equations
theorem complex.beta_integral_convergent_left {u : } (hu : 0 < u.re) (v : ) :
interval_integrable (λ (x : ), x ^ (u - 1) * (1 - x) ^ (v - 1)) measure_theory.measure_space.volume 0 (1 / 2)

Auxiliary lemma for beta_integral_convergent, showing convergence at the left endpoint.

theorem complex.beta_integral_convergent {u v : } (hu : 0 < u.re) (hv : 0 < v.re) :

The Beta integral is convergent for all u, v of positive real part.

theorem complex.beta_integral_symm (u v : ) :
=
theorem complex.beta_integral_eval_one_right {u : } (hu : 0 < u.re) :
= 1 / u
theorem complex.beta_integral_scaled (s t : ) {a : } (ha : 0 < a) :
(x : ) in 0..a, x ^ (s - 1) * (a - x) ^ (t - 1) = a ^ (s + t - 1) *
theorem complex.Gamma_mul_Gamma_eq_beta_integral {s t : } (hs : 0 < s.re) (ht : 0 < t.re) :
= complex.Gamma (s + t) *

Relation between Beta integral and Gamma function.

theorem complex.beta_integral_recurrence {u v : } (hu : 0 < u.re) (hv : 0 < v.re) :
u * u.beta_integral (v + 1) = v * (u + 1).beta_integral v

Recurrence formula for the Beta function.

theorem complex.beta_integral_eval_nat_add_one_right {u : } (hu : 0 < u.re) (n : ) :
u.beta_integral (n + 1) = (n.factorial) / (finset.range (n + 1)).prod (λ (j : ), u + j)

Explicit formula for the Beta function when second argument is a positive integer.

## The Euler limit formula #

noncomputable def complex.Gamma_seq (s : ) (n : ) :

The sequence with n-th term n ^ s * n! / (s * (s + 1) * ... * (s + n)), for complex s. We will show that this tends to Γ(s) as n → ∞.

Equations
theorem complex.Gamma_seq_eq_beta_integral_of_re_pos {s : } (hs : 0 < s.re) (n : ) :
theorem complex.Gamma_seq_add_one_left (s : ) {n : } (hn : n 0) :
(s + 1).Gamma_seq n / s = n / (n + 1 + s) * s.Gamma_seq n
theorem complex.Gamma_seq_eq_approx_Gamma_integral {s : } (hs : 0 < s.re) {n : } (hn : n 0) :
s.Gamma_seq n = (x : ) in 0..n, ((1 - x / n) ^ n) * x ^ (s - 1)
theorem complex.approx_Gamma_integral_tendsto_Gamma_integral {s : } (hs : 0 < s.re) :
filter.tendsto (λ (n : ), (x : ) in 0..n, ((1 - x / n) ^ n) * x ^ (s - 1)) filter.at_top (nhds (complex.Gamma s))

The main techical lemma for Gamma_seq_tendsto_Gamma, expressing the integral defining the Gamma function for 0 < re s as the limit of a sequence of integrals over finite intervals.

Euler's limit formula for the complex Gamma function.

## The reflection formula #

theorem complex.Gamma_seq_mul (z : ) {n : } (hn : n 0) :
z.Gamma_seq n * (1 - z).Gamma_seq n = n / (n + 1 - z) * (1 / (z * (finset.range n).prod (λ (j : ), 1 - z ^ 2 / (j + 1) ^ 2)))

Euler's reflection formula for the complex Gamma function.

theorem complex.Gamma_ne_zero {s : } (hs : (m : ), s -m) :

The Gamma function does not vanish on (except at non-positive integers, where the function is mathematically undefined and we set it to 0 by convention).

theorem complex.Gamma_eq_zero_iff (s : ) :
(m : ), s = -m
noncomputable def real.Gamma_seq (s : ) (n : ) :

The sequence with n-th term n ^ s * n! / (s * (s + 1) * ... * (s + n)), for real s. We will show that this tends to Γ(s) as n → ∞.

Equations

Euler's limit formula for the real Gamma function.

Euler's reflection formula for the real Gamma function.