mathlib3 documentation

analysis.special_functions.gamma.basic

The Gamma function #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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. (If s = -n for n ∈ ℕ, then the function is undefined, and we set it to be 0 by convention.)

Gamma function: main statements (complex case) #

complex.Gamma: the Γ function (of a complex variable).
complex.Gamma_eq_integral: for 0 < re s, Γ(s) agrees with Euler's integral.
complex.Gamma_add_one: for all s : ℂ with s ≠ 0, we have Γ (s + 1) = s Γ(s).
complex.Gamma_nat_eq_factorial: for all n : ℕ we have Γ (n + 1) = n!.
complex.differentiable_at_Gamma: Γ is complex-differentiable at all s : ℂ with s ∉ {-n : n ∈ ℕ}.

Gamma function: main statements (real case) #

real.Gamma: the Γ function (of a real variable).
Real counterparts of all the properties of the complex Gamma function listed above: real.Gamma_eq_integral, real.Gamma_add_one, real.Gamma_nat_eq_factorial, real.differentiable_at_Gamma.

Tags #

Gamma

theorem real.Gamma_integrand_is_o (s : ℝ) :

(λ (x : ℝ), rexp (-x) * x ^ s) =o[filter.at_top ] λ (x : ℝ), rexp (-(1 / 2) * x)

Asymptotic bound for the Γ function integrand.

theorem real.Gamma_integral_convergent {s : ℝ} (h : 0 < s) :

measure_theory.integrable_on (λ (x : ℝ), rexp (-x) * x ^ (s - 1)) (set.Ioi 0) measure_theory.measure_space.volume

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

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

measure_theory.integrable_on (λ (x : ℝ), ↑(rexp (-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.

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

s.Gamma_integral = ∫ (x : ℝ) in set.Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1)

theorem complex.Gamma_integral_conj (s : ℂ) :

(⇑(star_ring_end ℂ) s).Gamma_integral = ⇑(star_ring_end ℂ) s.Gamma_integral

theorem complex.Gamma_integral_of_real (s : ℝ) :

↑s.Gamma_integral = ↑∫ (x : ℝ) in set.Ioi 0, rexp (-x) * x ^ (s - 1)

theorem complex.Gamma_integral_one :

1.Gamma_integral = 1

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

s.partial_Gamma X = ∫ (x : ℝ) in 0..X, ↑(rexp (-x)) * ↑x ^ (s - 1)

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

filter.tendsto (λ (X : ℝ), s.partial_Gamma X) filter.at_top (nhds s.Gamma_integral)

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 - ↑(rexp (-X)) * ↑X ^ s

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

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.

noncomputable def complex.Gamma_aux :

ℕ → ℂ → ℂ

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

Equations

complex.Gamma_aux (n + 1) = λ (s : ℂ), complex.Gamma_aux n (s + 1) / s
complex.Gamma_aux 0 = complex.Gamma_integral

theorem complex.Gamma_aux_recurrence1 (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) :

complex.Gamma_aux n s = complex.Gamma_aux n (s + 1) / s

theorem complex.Gamma_aux_recurrence2 (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) :

complex.Gamma_aux n s = complex.Gamma_aux (n + 1) s

noncomputable def complex.Gamma (s : ℂ) :

The Γ function (of a complex variable s).

Equations

complex.Gamma s = complex.Gamma_aux ⌊1 - s.re⌋₊ s

theorem complex.Gamma_eq_Gamma_aux (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) :

complex.Gamma s = complex.Gamma_aux n s

theorem complex.Gamma_add_one (s : ℂ) (h2 : s ≠ 0) :

complex.Gamma (s + 1) = s * complex.Gamma s

The recurrence relation for the Γ function.

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

complex.Gamma s = s.Gamma_integral

theorem complex.Gamma_one :

complex.Gamma 1 = 1

theorem complex.Gamma_nat_eq_factorial (n : ℕ) :

complex.Gamma (↑n + 1) = ↑(n.factorial)

theorem complex.Gamma_zero :

complex.Gamma 0 = 0

At 0 the Gamma function is undefined; by convention we assign it the value 0.

theorem complex.Gamma_neg_nat_eq_zero (n : ℕ) :

complex.Gamma (-↑n) = 0

At -n for n ∈ ℕ, the Gamma function is undefined; by convention we assign it the value 0.

theorem complex.Gamma_conj (s : ℂ) :

complex.Gamma (⇑(star_ring_end ℂ) s) = ⇑(star_ring_end ℂ) (complex.Gamma s)

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

theorem complex.Gamma_integral_eq_mellin :

complex.Gamma_integral = mellin (λ (x : ℝ), ↑(rexp (-x)))

Rewrite the Gamma integral as an example of a Mellin transform.

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

has_deriv_at complex.Gamma_integral (∫ (t : ℝ) in set.Ioi 0, ↑t ^ (s - 1) * (↑(real.log t) * ↑(rexp (-t)))) s

The derivative of the Γ integral, at any s ∈ ℂ with 1 < re s, is given by the Melllin transform of log t * exp (-t).

theorem complex.differentiable_at_Gamma_aux (s : ℂ) (n : ℕ) (h1 : 1 - s.re < ↑n) (h2 : ∀ (m : ℕ), s ≠ -↑m) :

differentiable_at ℂ (complex.Gamma_aux n) s

theorem complex.differentiable_at_Gamma (s : ℂ) (hs : ∀ (m : ℕ), s ≠ -↑m) :

differentiable_at ℂ complex.Gamma s

theorem complex.tendsto_self_mul_Gamma_nhds_zero :

filter.tendsto (λ (z : ℂ), z * complex.Gamma z) (nhds_within 0 {0}ᶜ) (nhds 1)

At s = 0, the Gamma function has a simple pole with residue 1.

noncomputable def real.Gamma (s : ℝ) :

The Γ function (of a real variable s).

Equations

real.Gamma s = (complex.Gamma ↑s).re

theorem real.Gamma_eq_integral {s : ℝ} (hs : 0 < s) :

real.Gamma s = ∫ (x : ℝ) in set.Ioi 0, rexp (-x) * x ^ (s - 1)

theorem real.Gamma_add_one {s : ℝ} (hs : s ≠ 0) :

real.Gamma (s + 1) = s * real.Gamma s

theorem real.Gamma_one :

real.Gamma 1 = 1

theorem complex.Gamma_of_real (s : ℝ) :

complex.Gamma ↑s = ↑(real.Gamma s)

theorem real.Gamma_nat_eq_factorial (n : ℕ) :

real.Gamma (↑n + 1) = ↑(n.factorial)

theorem real.Gamma_zero :

real.Gamma 0 = 0

At 0 the Gamma function is undefined; by convention we assign it the value 0.

theorem real.Gamma_neg_nat_eq_zero (n : ℕ) :

real.Gamma (-↑n) = 0

At -n for n ∈ ℕ, the Gamma function is undefined; by convention we assign it the value 0.

theorem real.Gamma_pos_of_pos {s : ℝ} (hs : 0 < s) :

0 < real.Gamma s

theorem real.Gamma_ne_zero {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -↑m) :

real.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 real.Gamma_eq_zero_iff (s : ℝ) :

real.Gamma s = 0 ↔ ∃ (m : ℕ), s = -↑m

theorem real.differentiable_at_Gamma {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -↑m) :

differentiable_at ℝ real.Gamma s