The Beta function, and further 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 define the Beta integral, relate Beta and Gamma functions, and prove some refined properties of the Gamma function using these relations.

Results on the Beta function #

complex.beta_integral: the Beta function Β(u, v), where u, v are complex with positive real part.
complex.Gamma_mul_Gamma_eq_beta_integral: the formula Gamma u * Gamma v = Gamma (u + v) * beta_integral u v.

Results on the Gamma function #

complex.Gamma_ne_zero: for all s : ℂ with s ∉ {-n : n ∈ ℕ} we have Γ s ≠ 0.
complex.Gamma_seq_tendsto_Gamma: for all s, the limit as n → ∞ of the sequence n ↦ n ^ s * n! / (s * (s + 1) * ... * (s + n)) is Γ(s).
complex.Gamma_mul_Gamma_one_sub: Euler's reflection formula Gamma s * Gamma (1 - s) = π / sin π s.
complex.differentiable_one_div_Gamma: the function 1 / Γ(s) is differentiable everywhere.
complex.Gamma_mul_Gamma_add_half: Legendre's duplication formula Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * 2 ^ (1 - 2 * s) * sqrt π.
real.Gamma_ne_zero, real.Gamma_seq_tendsto_Gamma, real.Gamma_mul_Gamma_one_sub, real.Gamma_mul_Gamma_add_half: real versions of the above.

The Beta function #

source

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

u.beta_integral v = ∫ (x : ℝ) in 0..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)

source

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.

source

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

interval_integrable (λ (x : ℝ), ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) measure_theory.measure_space.volume 0 1

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

source

theorem complex.beta_integral_symm (u v : ℂ) :

v.beta_integral u = u.beta_integral v

source

theorem complex.beta_integral_eval_one_right {u : ℂ} (hu : 0 < u.re) :

u.beta_integral 1 = 1 / u

source

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) * s.beta_integral t

source

theorem complex.Gamma_mul_Gamma_eq_beta_integral {s t : ℂ} (hs : 0 < s.re) (ht : 0 < t.re) :

complex.Gamma s * complex.Gamma t = complex.Gamma (s + t) * s.beta_integral t

Relation between Beta integral and Gamma function.

source

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.

source

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 #

source

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

s.Gamma_seq n = ↑n ^ s * ↑(n.factorial) / (finset.range (n + 1)).prod (λ (j : ℕ), s + ↑j)

source

theorem complex.Gamma_seq_eq_beta_integral_of_re_pos {s : ℂ} (hs : 0 < s.re) (n : ℕ) :

s.Gamma_seq n = ↑n ^ s * s.beta_integral (↑n + 1)

source

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

source

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)

source

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.

source

theorem complex.Gamma_seq_tendsto_Gamma (s : ℂ) :

filter.tendsto s.Gamma_seq filter.at_top (nhds (complex.Gamma s))

Euler's limit formula for the complex Gamma function.

The reflection formula #

source

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

source

theorem complex.Gamma_mul_Gamma_one_sub (z : ℂ) :

complex.Gamma z * complex.Gamma (1 - z) = ↑real.pi / complex.sin (↑real.pi * z)

Euler's reflection formula for the complex Gamma function.

source

theorem complex.Gamma_ne_zero {s : ℂ} (hs : ∀ (m : ℕ), s ≠ -↑m) :

complex.Gamma s ≠ 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).

source

theorem complex.Gamma_eq_zero_iff (s : ℂ) :

complex.Gamma s = 0 ↔ ∃ (m : ℕ), s = -↑m

source

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

complex.Gamma s ≠ 0

A weaker, but easier-to-apply, version of complex.Gamma_ne_zero.

source

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

s.Gamma_seq n = ↑n ^ s * ↑(n.factorial) / (finset.range (n + 1)).prod (λ (j : ℕ), s + ↑j)

source

theorem real.Gamma_seq_tendsto_Gamma (s : ℝ) :

filter.tendsto s.Gamma_seq filter.at_top (nhds (real.Gamma s))

Euler's limit formula for the real Gamma function.

source

theorem real.Gamma_mul_Gamma_one_sub (s : ℝ) :

real.Gamma s * real.Gamma (1 - s) = real.pi / real.sin (real.pi * s)

Euler's reflection formula for the real Gamma function.

The reciprocal Gamma function #

We show that the reciprocal Gamma function 1 / Γ(s) is entire. These lemmas show that (in this case at least) mathlib's conventions for division by zero do actually give a mathematically useful answer! (These results are useful in the theory of zeta and L-functions.)

source

theorem complex.one_div_Gamma_eq_self_mul_one_div_Gamma_add_one (s : ℂ) :

(complex.Gamma s)⁻¹ = s * (complex.Gamma (s + 1))⁻¹

A reformulation of the Gamma recurrence relation which is true for s = 0 as well.

source

theorem complex.differentiable_one_div_Gamma :

differentiable ℂ (λ (s : ℂ), (complex.Gamma s)⁻¹)

The reciprocal of the Gamma function is differentiable everywhere (including the points where Gamma itself is not).

The doubling formula for Gamma #

We prove the doubling formula for arbitrary real or complex arguments, by analytic continuation from the positive real case. (Knowing that Γ⁻¹ is analytic everywhere makes this much simpler, since we do not have to do any special-case handling for the poles of Γ.)

source

theorem complex.Gamma_mul_Gamma_add_half (s : ℂ) :

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

source

theorem real.Gamma_mul_Gamma_add_half (s : ℝ) :

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