mathlib3 documentation

analysis.special_functions.gamma.beta

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 #

Results on the Gamma function #

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_eval_one_right {u : } (hu : 0 < u.re) :
u.beta_integral 1 = 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) * s.beta_integral t
theorem complex.Gamma_mul_Gamma_eq_beta_integral {s t : } (hs : 0 < s.re) (ht : 0 < t.re) :

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_ne_zero_of_re_pos {s : } (hs : 0 < s.re) :

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

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.

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

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

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

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