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

theorem integral_exp_neg_Ioi  :
∫ (x : ) in set.Ioi 0, real.exp (-x) = 1
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.

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

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

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

This is proved by reduction to the real case.

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

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

noncomputable def complex.partial_Gamma (s : ) (X : ) :

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

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

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

The recurrence relation for the Γ integral.

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

noncomputable def complex.Gamma_aux  :

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

Equations
theorem complex.Gamma_aux_recurrence1 (s : ) (n : ) (h1 : -s.re < n) :
theorem complex.Gamma_aux_recurrence2 (s : ) (n : ) (h1 : -s.re < n) :
noncomputable def complex.Gamma (s : ) :

The Γ function (of a complex variable s).

Equations
theorem complex.Gamma_eq_Gamma_aux (s : ) (n : ) (h1 : -s.re < n) :
theorem complex.Gamma_add_one (s : ) (h2 : s 0) :
(s + 1).Gamma = s * s.Gamma

The recurrence relation for the Γ function.

theorem complex.Gamma_eq_integral (s : ) (hs : 0 < s.re) :

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

noncomputable def dGamma_integrand (s : ) (x : ) :

Integrand for the derivative of the Γ function

Equations
noncomputable def dGamma_integrand_real (s x : ) :

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

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

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

theorem loc_unif_bound_dGamma_integrand {t : } {s1 s2 x : } (ht1 : s1 t.re) (ht2 : t.re s2) (hx : 0 < x) :

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

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

theorem complex.differentiable_at_Gamma_aux (s : ) (n : ) (h1 : 1 - s.re < n) (h2 : ∀ (m : ), s + m 0) :