The Beta function, and further properties of the Gamma function #

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.
real.Gamma_ne_zero, real.Gamma_seq_tendsto_Gamma, real.Gamma_mul_Gamma_one_sub: real versions of the above results.

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

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