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. (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.differentiableAt_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.differentiableAt_Gamma.

Tags

Gamma

theorem Real.Gamma_integrand_isLittleO (s : ℝ) : (fun (x : ℝ) => Real.exp (-x) * x ^ s) =o[Filter.atTop] fun (x : ℝ) => Real.exp (-(1 / 2) * x)

Asymptotic bound for the Γ function integrand.

theorem Real.GammaIntegral_convergent {s : ℝ} (h : 0 < s) : MeasureTheory.IntegrableOn (fun (x : ℝ) => Real.exp (-x) * x ^ (s - 1)) (Set.Ioi 0) MeasureTheory.volume

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

theorem Complex.GammaIntegral_convergent {s : ℂ} (hs : 0 < s.re) : MeasureTheory.IntegrableOn (fun (x : ℝ) => ↑(Real.exp (-x)) * ↑x ^ (s - 1)) (Set.Ioi 0) MeasureTheory.volume

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

This is proved by reduction to the real case.

def Complex.GammaIntegral (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.GammaIntegral_convergent for a proof of the convergence of the integral for 0 < re s.

Equations

• Complex.GammaIntegral s = ∫ (x : ℝ) in Set.Ioi 0, ↑(Real.exp (-x)) * ↑x ^ (s - 1)

theorem Complex.GammaIntegral_conj (s : ℂ) : Complex.GammaIntegral ((starRingEnd ℂ) s) = (starRingEnd ℂ) (Complex.GammaIntegral s)

theorem Complex.GammaIntegral_ofReal (s : ℝ) : Complex.GammaIntegral ↑s = ↑(∫ (x : ℝ) in Set.Ioi 0, Real.exp (-x) * x ^ (s - 1))

@[simp]

theorem Complex.GammaIntegral_one : Complex.GammaIntegral 1 = 1

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

def Complex.partialGamma (s : ℂ) (X : ℝ) : ℂ

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

Equations

• Complex.partialGamma s X = ∫ (x : ℝ) in 0 ..X, ↑(Real.exp (-x)) * ↑x ^ (s - 1)

theorem Complex.tendsto_partialGamma {s : ℂ} (hs : 0 < s.re) : Filter.Tendsto (fun (X : ℝ) => Complex.partialGamma s X) Filter.atTop (nhds (Complex.GammaIntegral s))

theorem Complex.partialGamma_add_one {s : ℂ} (hs : 0 < s.re) {X : ℝ} (hX : 0 ≤ X) : Complex.partialGamma (s + 1) X = s * Complex.partialGamma s X - ↑(Real.exp (-X)) * ↑X ^ s

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

theorem Complex.GammaIntegral_add_one {s : ℂ} (hs : 0 < s.re) : Complex.GammaIntegral (s + 1) = s * Complex.GammaIntegral s

The recurrence relation for the Γ integral.

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

noncomputable def Complex.GammaAux : ℕ → ℂ → ℂ

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

Equations

• Complex.GammaAux 0 = Complex.GammaIntegral
• Complex.GammaAux (Nat.succ n) = fun (s : ℂ) => Complex.GammaAux n (s + 1) / s

theorem Complex.GammaAux_recurrence1 (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) : Complex.GammaAux n s = Complex.GammaAux n (s + 1) / s

theorem Complex.GammaAux_recurrence2 (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) : Complex.GammaAux n s = Complex.GammaAux (n + 1) s

theorem Complex.Gamma_def (s : ℂ) : Complex.Gamma s = Complex.GammaAux ⌊1 - s.re⌋₊ s

@[irreducible]

def Complex.Gamma (s : ℂ) : ℂ

The Γ function (of a complex variable s).

Equations

• Complex.Gamma = Complex.wrapped✝.1

theorem Complex.Gamma_eq_GammaAux (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) : Complex.Gamma s = Complex.GammaAux 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 = Complex.GammaIntegral s

@[simp]

theorem Complex.Gamma_one : Complex.Gamma 1 = 1

theorem Complex.Gamma_nat_eq_factorial (n : ℕ) : Complex.Gamma (↑n + 1) = ↑(Nat.factorial n)

@[simp]

theorem Complex.Gamma_ofNat_eq_factorial (n : ℕ) [Nat.AtLeastTwo (n + 1)] : Complex.Gamma (OfNat.ofNat (n + 1)) = ↑(Nat.factorial n)

@[simp]

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 ((starRingEnd ℂ) s) = (starRingEnd ℂ) (Complex.Gamma s)

theorem Complex.integral_cpow_mul_exp_neg_mul_Ioi {a : ℂ} {r : ℝ} (ha : 0 < a.re) (hr : 0 < r) : ∫ (t : ℝ) in Set.Ioi 0, ↑t ^ (a - 1) * Complex.exp (-(↑r * ↑t)) = (1 / ↑r) ^ a * Complex.Gamma a

Expresses the integral over Ioi 0 of t ^ (a - 1) * exp (-(r * t)) in terms of the Gamma function, for complex a.

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

theorem Complex.GammaIntegral_eq_mellin : Complex.GammaIntegral = mellin fun (x : ℝ) => ↑(Real.exp (-x))

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

theorem Complex.hasDerivAt_GammaIntegral {s : ℂ} (hs : 0 < s.re) : HasDerivAt Complex.GammaIntegral (∫ (t : ℝ) in Set.Ioi 0, ↑t ^ (s - 1) * (↑(Real.log t) * ↑(Real.exp (-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.differentiableAt_GammaAux (s : ℂ) (n : ℕ) (h1 : 1 - s.re < ↑n) (h2 : ∀ (m : ℕ), s ≠ -↑m) : DifferentiableAt ℂ (Complex.GammaAux n) s

theorem Complex.differentiableAt_Gamma (s : ℂ) (hs : ∀ (m : ℕ), s ≠ -↑m) : DifferentiableAt ℂ Complex.Gamma s

theorem Complex.tendsto_self_mul_Gamma_nhds_zero : Filter.Tendsto (fun (z : ℂ) => z * Complex.Gamma z) (nhdsWithin 0 {0}ᶜ) (nhds 1)

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

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, Real.exp (-x) * x ^ (s - 1)

theorem Real.Gamma_add_one {s : ℝ} (hs : s ≠ 0) : Real.Gamma (s + 1) = s * Real.Gamma s

@[simp]

theorem Real.Gamma_one : Real.Gamma 1 = 1

theorem Complex.Gamma_ofReal (s : ℝ) : Complex.Gamma ↑s = ↑(Real.Gamma s)

theorem Real.Gamma_nat_eq_factorial (n : ℕ) : Real.Gamma (↑n + 1) = ↑(Nat.factorial n)

@[simp]

theorem Real.Gamma_ofNat_eq_factorial (n : ℕ) [Nat.AtLeastTwo (n + 1)] : Real.Gamma (OfNat.ofNat (n + 1)) = ↑(Nat.factorial n)

@[simp]

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_nonneg_of_nonneg {s : ℝ} (hs : 0 ≤ s) : 0 ≤ Real.Gamma s

theorem Real.integral_rpow_mul_exp_neg_mul_Ioi {a : ℝ} {r : ℝ} (ha : 0 < a) (hr : 0 < r) : ∫ (t : ℝ) in Set.Ioi 0, t ^ (a - 1) * Real.exp (-(r * t)) = (1 / r) ^ a * Real.Gamma a

Expresses the integral over Ioi 0 of t ^ (a - 1) * exp (-(r * t)), for positive real r, in terms of the Gamma function.

def Mathlib.Meta.Positivity.evalGamma : Mathlib.Meta.Positivity.PositivityExt

The positivity extension which identifies expressions of the form Gamma a.

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.differentiableAt_Gamma {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -↑m) : DifferentiableAt ℝ Real.Gamma s