# mathlibdocumentation

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 , 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 * - (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) :
= (s + 1) / s
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) :
s.Gamma =
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) * * 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.

theorem complex.has_deriv_at_Gamma_integral {s : } (hs : 1 < s.re) :

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) :
theorem complex.differentiable_at_Gamma (s : ) (hs : ∀ (m : ), s + m 0) :