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.betaIntegral: the Beta function Β(u, v), where u, v are complex with positive real part.
• Complex.Gamma_mul_Gamma_eq_betaIntegral: the formula Gamma u * Gamma v = Gamma (u + v) * betaIntegral u v.

Results on the Gamma function

• Complex.Gamma_ne_zero: for all s : ℂ with s ∉ {-n : n ∈ ℕ} we have Γ s ≠ 0.
• Complex.GammaSeq_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.GammaSeq_tendsto_Gamma, Real.Gamma_mul_Gamma_one_sub, Real.Gamma_mul_Gamma_add_half: real versions of the above.

The Beta function

noncomputable def Complex.betaIntegral (u : ℂ) (v : ℂ) : ℂ

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

Equations

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

theorem Complex.betaIntegral_convergent_left {u : ℂ} (hu : 0 < u.re) (v : ℂ) : IntervalIntegrable (fun (x : ℝ) => ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) MeasureTheory.volume 0 (1 / 2)

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

theorem Complex.betaIntegral_convergent {u : ℂ} {v : ℂ} (hu : 0 < u.re) (hv : 0 < v.re) : IntervalIntegrable (fun (x : ℝ) => ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) MeasureTheory.volume 0 1

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

theorem Complex.betaIntegral_symm (u : ℂ) (v : ℂ) : Complex.betaIntegral v u = Complex.betaIntegral u v

theorem Complex.betaIntegral_eval_one_right {u : ℂ} (hu : 0 < u.re) : Complex.betaIntegral u 1 = 1 / u

theorem Complex.betaIntegral_scaled (s : ℂ) (t : ℂ) {a : ℝ} (ha : 0 < a) : ∫ (x : ℝ) in 0 ..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) = ↑a ^ (s + t - 1) * Complex.betaIntegral s t

theorem Complex.Gamma_mul_Gamma_eq_betaIntegral {s : ℂ} {t : ℂ} (hs : 0 < s.re) (ht : 0 < t.re) : Complex.Gamma s * Complex.Gamma t = Complex.Gamma (s + t) * Complex.betaIntegral s t

Relation between Beta integral and Gamma function.

theorem Complex.betaIntegral_recurrence {u : ℂ} {v : ℂ} (hu : 0 < u.re) (hv : 0 < v.re) : u * Complex.betaIntegral u (v + 1) = v * Complex.betaIntegral (u + 1) v

Recurrence formula for the Beta function.

theorem Complex.betaIntegral_eval_nat_add_one_right {u : ℂ} (hu : 0 < u.re) (n : ℕ) : Complex.betaIntegral u (↑n + 1) = ↑(Nat.factorial n) / Finset.prod (Finset.range (n + 1)) fun (j : ℕ) => u + ↑j

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

The Euler limit formula

noncomputable def Complex.GammaSeq (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

• Complex.GammaSeq s n = ↑n ^ s * ↑(Nat.factorial n) / Finset.prod (Finset.range (n + 1)) fun (j : ℕ) => s + ↑j

theorem Complex.GammaSeq_eq_betaIntegral_of_re_pos {s : ℂ} (hs : 0 < s.re) (n : ℕ) : Complex.GammaSeq s n = ↑n ^ s * Complex.betaIntegral s (↑n + 1)

theorem Complex.GammaSeq_add_one_left (s : ℂ) {n : ℕ} (hn : n ≠ 0) : Complex.GammaSeq (s + 1) n / s = ↑n / (↑n + 1 + s) * Complex.GammaSeq s n

theorem Complex.GammaSeq_eq_approx_Gamma_integral {s : ℂ} (hs : 0 < s.re) {n : ℕ} (hn : n ≠ 0) : Complex.GammaSeq s 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 (fun (n : ℕ) => ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) Filter.atTop (nhds (Complex.Gamma s))

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

theorem Complex.GammaSeq_tendsto_Gamma (s : ℂ) : Filter.Tendsto (Complex.GammaSeq s) Filter.atTop (nhds (Complex.Gamma s))

Euler's limit formula for the complex Gamma function.

The reflection formula

theorem Complex.GammaSeq_mul (z : ℂ) {n : ℕ} (hn : n ≠ 0) : Complex.GammaSeq z n * Complex.GammaSeq (1 - z) n = ↑n / (↑n + 1 - z) * (1 / (z * Finset.prod (Finset.range n) fun (j : ℕ) => 1 - z ^ 2 / (↑j + 1) ^ 2))

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.

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

theorem Complex.Gamma_eq_zero_iff (s : ℂ) : Complex.Gamma s = 0 ↔ ∃ (m : ℕ), s = -↑m

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.

noncomputable def Real.GammaSeq (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

• Real.GammaSeq s n = ↑n ^ s * ↑(Nat.factorial n) / Finset.prod (Finset.range (n + 1)) fun (j : ℕ) => s + ↑j

theorem Real.GammaSeq_tendsto_Gamma (s : ℝ) : Filter.Tendsto (Real.GammaSeq s) Filter.atTop (nhds (Real.Gamma s))

Euler's limit formula for the real Gamma function.

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

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.

theorem Complex.differentiable_one_div_Gamma : Differentiable ℂ fun (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 Γ.)

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.sqrt Real.pi)

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.sqrt Real.pi