mathlib documentation

analysis.special_functions.gamma

The Gamma function #

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. In the complex case we also prove that the resulting function is holomorphic on ℂ away from the points {-n : n ∈ ℤ}.

Tags #

Gamma

source
theorem integral_exp_neg_Ioi  :
∫ (x : ℝ) in set.Ioi 0, real.exp (-x) = 1
source
theorem real.Gamma_integrand_is_o (s : ℝ) :
(λ (x : ℝ), real.exp (-x) * x ^ s) =o[filter.at_top] λ (x : ℝ), real.exp (-(1 / 2) * x)

Asymptotic bound for the Γ function integrand.

source
noncomputable def real.Gamma_integral (s : ℝ) :
ℝ

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

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

Equations
source
theorem real.Gamma_integral_convergent {s : ℝ} (h : 0 < s) :
measure_theory.integrable_on (λ (x : ℝ), real.exp (-x) * x ^ (s - 1)) (set.Ioi 0) measure_theory.measure_space.volume

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

source
theorem real.Gamma_integral_one  :
1.Gamma_integral = 1
source
theorem complex.Gamma_integral_convergent {s : ℂ} (hs : 0 < s.re) :
measure_theory.integrable_on (λ (x : ℝ), ↑(real.exp (-x)) * ↑x ^ (s - 1)) (set.Ioi 0) measure_theory.measure_space.volume

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

This is proved by reduction to the real case.

source
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
source
theorem complex.Gamma_integral_of_real (s : ℝ) :
↑s.Gamma_integral = ↑(s.Gamma_integral)
source
theorem complex.Gamma_integral_one  :
1.Gamma_integral = 1

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

source
noncomputable def complex.partial_Gamma (s : ℂ) (X : ℝ) :
ℂ

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

Equations
source
theorem complex.tendsto_partial_Gamma {s : ℂ} (hs : 0 < s.re) :
filter.tendsto (λ (X : ℝ), s.partial_Gamma X) filter.at_top (nhds s.Gamma_integral)
source
theorem complex.partial_Gamma_add_one {s : ℂ} (hs : 0 < s.re) {X : ℝ} (hX : 0 ≤ X) :
(s + 1).partial_Gamma X = s * s.partial_Gamma X - ↑(real.exp (-X)) * ↑X ^ s

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

source
theorem complex.Gamma_integral_add_one {s : ℂ} (hs : 0 < s.re) :
(s + 1).Gamma_integral = s * s.Gamma_integral

The recurrence relation for the Γ integral.

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

source
noncomputable def complex.Gamma_aux  :
ℕ → ℂ → ℂ

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

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

The Γ function (of a complex variable s).

Equations
source
theorem complex.Gamma_eq_Gamma_aux (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) :
s.Gamma = complex.Gamma_aux n s
source
theorem complex.Gamma_add_one (s : ℂ) (h2 : s ≠ 0) :
(s + 1).Gamma = s * s.Gamma

The recurrence relation for the Γ function.

source
theorem complex.Gamma_eq_integral (s : ℂ) (hs : 0 < s.re) :
s.Gamma = s.Gamma_integral
source
theorem complex.Gamma_nat_eq_factorial (n : ℕ) :
(↑n + 1).Gamma = ↑(n.factorial)

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

source
noncomputable def dGamma_integrand (s : ℂ) (x : ℝ) :
ℂ

Integrand for the derivative of the Γ function

Equations
source
noncomputable def dGamma_integrand_real (s x : ℝ) :
ℝ

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

Equations
source
theorem dGamma_integrand_is_o_at_top (s : ℝ) :
(λ (x : ℝ), real.exp (-x) * real.log x * x ^ (s - 1)) =o[filter.at_top] λ (x : ℝ), real.exp (-(1 / 2) * x)
source
theorem dGamma_integral_abs_convergent (s : ℝ) (hs : 1 < s) :
measure_theory.integrable_on (λ (x : ℝ), ∥real.exp (-x) * real.log x * x ^ (s - 1)∥) (set.Ioi 0) measure_theory.measure_space.volume

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

source
theorem loc_unif_bound_dGamma_integrand {t : ℂ} {s1 s2 x : ℝ} (ht1 : s1 ≤ t.re) (ht2 : t.re ≤ s2) (hx : 0 < x) :
∥dGamma_integrand t x∥ ≤ dGamma_integrand_real s1 x + dGamma_integrand_real s2 x

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

source
theorem complex.has_deriv_at_Gamma_integral {s : ℂ} (hs : 1 < s.re) :
measure_theory.integrable_on (λ (x : ℝ), ↑(real.exp (-x)) * ↑(real.log x) * ↑x ^ (s - 1)) (set.Ioi 0) measure_theory.measure_space.volume ∧ has_deriv_at complex.Gamma_integral (∫ (x : ℝ) in set.Ioi 0, ↑(real.exp (-x)) * ↑(real.log x) * ↑x ^ (s - 1)) s

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

source
theorem complex.differentiable_at_Gamma_aux (s : ℂ) (n : ℕ) (h1 : 1 - s.re < ↑n) (h2 : ∀ (m : ℕ), s + ↑m ≠ 0) :
differentiable_at ℂ (complex.Gamma_aux n) s
source
theorem complex.differentiable_at_Gamma (s : ℂ) (hs : ∀ (m : ℕ), s + ↑m ≠ 0) :
differentiable_at ℂ complex.Gamma s