mathlib documentation

analysis.special_functions.gamma

The Gamma and Beta functions #

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 ∈ ℕ}.
complex.Gamma_ne_zero: for all s : ℂ with s ∉ {-n : n ∈ ℕ} we have Γ s ≠ 0.
complex.Gamma_seq_tendsto_Gamma: for all s, the limit as n → ∞ of the sequence n ↦ n ^ s * n! / (s * (s + 1) * ... * (s + n)) is Γ(s).
complex.Gamma_mul_Gamma_one_sub: Euler's reflection formula Gamma s * Gamma (1 - s) = π / sin π s.

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, real.Gamma_ne_zero, real.Gamma_seq_tendsto_Gamma, real.Gamma_mul_Gamma_one_sub.
real.convex_on_log_Gamma : log ∘ Γ is convex on Ioi 0.
real.eq_Gamma_of_log_convex : the Bohr-Mollerup theorem, which states that the Γ function is the unique log-convex, positive-valued function on Ioi 0 satisfying the functional equation and having Γ 1 = 1.

Beta function #

complex.beta_integral: the Beta function Β(u, v), where u, v are complex with positive real part.
complex.Gamma_mul_Gamma_eq_beta_integral: the formula Gamma u * Gamma v = Gamma (u + v) * beta_integral u v.

Tags #

Gamma

theorem integral_exp_neg_Ioi :

∫ (x : ℝ) in set.Ioi 0, rexp (-x) = 1

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.

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

Integrand for the derivative of the Γ function

Equations

dGamma_integrand s x = ↑(rexp (-x)) * ↑(real.log x) * ↑x ^ (s - 1)

noncomputable def dGamma_integrand_real (s x : ℝ) :

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

Equations

dGamma_integrand_real s x = |rexp (-x) * real.log x * x ^ (s - 1)|

theorem dGamma_integrand_is_o_at_top (s : ℝ) :

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

theorem dGamma_integral_abs_convergent (s : ℝ) (hs : 1 < s) :

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

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.

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

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

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

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

theorem real.Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma {s t a b : ℝ} (hs : 0 < s) (ht : 0 < t) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :

real.Gamma (a * s + b * t) ≤ real.Gamma s ^ a * real.Gamma t ^ b

Log-convexity of the Gamma function on the positive reals (stated in multiplicative form), proved using the Hölder inequality applied to Euler's integral.

theorem real.convex_on_log_Gamma :

convex_on ℝ (set.Ioi 0) (real.log ∘ real.Gamma)

theorem real.convex_on_Gamma :

convex_on ℝ (set.Ioi 0) real.Gamma

The Bohr-Mollerup theorem #

In this section we prove two interrelated statements about the Γ function on the positive reals:

the Euler limit formula real.bohr_mollerup.tendsto_log_gamma_seq, stating that for positive real x the sequence x * log n + log n! - ∑ (m : ℕ) in finset.range (n + 1), log (x + m) tends to log Γ(x) as n → ∞.
the Bohr-Mollerup theorem (real.eq_Gamma_of_log_convex) which states that Γ is the unique log-convex, positive-real-valued function on the positive reals satisfying f (x + 1) = x f x and f 1 = 1.

To do this, we prove that any function satisfying the hypotheses of the Bohr--Mollerup theorem must agree with the limit in the Euler limit formula, so there is at most one such function. Then we show that Γ satisfies these conditions.

Since most of the auxiliary lemmas for the Bohr-Mollerup theorem are of no relevance outside the context of this proof, we place them in a separate namespace real.bohr_mollerup to avoid clutter. (This includes the logarithmic form of the Euler limit formula, since later we will prove a more general form of the Euler limit formula valid for any real or complex x; see real.Gamma_seq_tendsto_Gamma and complex.Gamma_seq_tendsto_Gamma.)

noncomputable def real.bohr_mollerup.log_gamma_seq (x : ℝ) (n : ℕ) :

The function n ↦ x log n + log n! - (log x + ... + log (x + n)), which we will show tends to log (Gamma x) as n → ∞.

Equations

real.bohr_mollerup.log_gamma_seq x n = x * real.log ↑n + real.log ↑(n.factorial) - (finset.range (n + 1)).sum (λ (m : ℕ), real.log (x + ↑m))

theorem real.bohr_mollerup.f_nat_eq {f : ℝ → ℝ} {n : ℕ} (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + real.log y) (hn : n ≠ 0) :

f ↑n = f 1 + real.log ↑((n - 1).factorial)

theorem real.bohr_mollerup.f_add_nat_eq {f : ℝ → ℝ} {x : ℝ} (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + real.log y) (hx : 0 < x) (n : ℕ) :

f (x + ↑n) = f x + (finset.range n).sum (λ (m : ℕ), real.log (x + ↑m))

theorem real.bohr_mollerup.f_add_nat_le {f : ℝ → ℝ} {x : ℝ} {n : ℕ} (hf_conv : convex_on ℝ (set.Ioi 0) f) (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + real.log y) (hn : n ≠ 0) (hx : 0 < x) (hx' : x ≤ 1) :

f (↑n + x) ≤ f ↑n + x * real.log ↑n

Linear upper bound for f (x + n) on unit interval

theorem real.bohr_mollerup.f_add_nat_ge {f : ℝ → ℝ} {x : ℝ} {n : ℕ} (hf_conv : convex_on ℝ (set.Ioi 0) f) (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + real.log y) (hn : 2 ≤ n) (hx : 0 < x) :

f ↑n + x * real.log (↑n - 1) ≤ f (↑n + x)

Linear lower bound for f (x + n) on unit interval

theorem real.bohr_mollerup.log_gamma_seq_add_one (x : ℝ) (n : ℕ) :

real.bohr_mollerup.log_gamma_seq (x + 1) n = real.bohr_mollerup.log_gamma_seq x (n + 1) + real.log x - (x + 1) * (real.log (↑n + 1) - real.log ↑n)

theorem real.bohr_mollerup.le_log_gamma_seq {f : ℝ → ℝ} {x : ℝ} (hf_conv : convex_on ℝ (set.Ioi 0) f) (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + real.log y) (hx : 0 < x) (hx' : x ≤ 1) (n : ℕ) :

f x ≤ f 1 + x * real.log (↑n + 1) - x * real.log ↑n + real.bohr_mollerup.log_gamma_seq x n

theorem real.bohr_mollerup.ge_log_gamma_seq {f : ℝ → ℝ} {x : ℝ} {n : ℕ} (hf_conv : convex_on ℝ (set.Ioi 0) f) (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + real.log y) (hx : 0 < x) (hn : n ≠ 0) :

f 1 + real.bohr_mollerup.log_gamma_seq x n ≤ f x

theorem real.bohr_mollerup.tendsto_log_gamma_seq_of_le_one {f : ℝ → ℝ} {x : ℝ} (hf_conv : convex_on ℝ (set.Ioi 0) f) (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + real.log y) (hx : 0 < x) (hx' : x ≤ 1) :

filter.tendsto (real.bohr_mollerup.log_gamma_seq x) filter.at_top (nhds (f x - f 1))

theorem real.bohr_mollerup.tendsto_log_gamma_seq {f : ℝ → ℝ} {x : ℝ} (hf_conv : convex_on ℝ (set.Ioi 0) f) (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + real.log y) (hx : 0 < x) :

filter.tendsto (real.bohr_mollerup.log_gamma_seq x) filter.at_top (nhds (f x - f 1))

theorem real.bohr_mollerup.tendsto_log_Gamma {x : ℝ} (hx : 0 < x) :

filter.tendsto (real.bohr_mollerup.log_gamma_seq x) filter.at_top (nhds (real.log (real.Gamma x)))

theorem real.eq_Gamma_of_log_convex {f : ℝ → ℝ} (hf_conv : convex_on ℝ (set.Ioi 0) (real.log ∘ f)) (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y) (hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y) (hf_one : f 1 = 1) :

set.eq_on f real.Gamma (set.Ioi 0)

The Bohr-Mollerup theorem: the Gamma function is the unique log-convex, positive-valued function on the positive reals which satisfies f 1 = 1 and f (x + 1) = x * f x for all x.

theorem real.Gamma_two :

real.Gamma 2 = 1

theorem real.Gamma_three_div_two_lt_one :

real.Gamma (3 / 2) < 1

theorem real.Gamma_strict_mono_on_Ici :

strict_mono_on real.Gamma (set.Ici 2)

The Beta function #

noncomputable def complex.beta_integral (u v : ℂ) :

The Beta function Β (u, v), defined as ∫ x:ℝ in 0..1, x ^ (u - 1) * (1 - x) ^ (v - 1).

Equations

u.beta_integral v = ∫ (x : ℝ) in 0..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)

theorem complex.beta_integral_convergent_left {u : ℂ} (hu : 0 < u.re) (v : ℂ) :

interval_integrable (λ (x : ℝ), ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) measure_theory.measure_space.volume 0 (1 / 2)

Auxiliary lemma for beta_integral_convergent, showing convergence at the left endpoint.

theorem complex.beta_integral_convergent {u v : ℂ} (hu : 0 < u.re) (hv : 0 < v.re) :

interval_integrable (λ (x : ℝ), ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) measure_theory.measure_space.volume 0 1

The Beta integral is convergent for all u, v of positive real part.

theorem complex.beta_integral_symm (u v : ℂ) :

v.beta_integral u = u.beta_integral v

theorem complex.beta_integral_eval_one_right {u : ℂ} (hu : 0 < u.re) :

u.beta_integral 1 = 1 / u

theorem complex.beta_integral_scaled (s t : ℂ) {a : ℝ} (ha : 0 < a) :

∫ (x : ℝ) in 0..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) = ↑a ^ (s + t - 1) * s.beta_integral t

theorem complex.Gamma_mul_Gamma_eq_beta_integral {s t : ℂ} (hs : 0 < s.re) (ht : 0 < t.re) :

complex.Gamma s * complex.Gamma t = complex.Gamma (s + t) * s.beta_integral t

Relation between Beta integral and Gamma function.

theorem complex.beta_integral_recurrence {u v : ℂ} (hu : 0 < u.re) (hv : 0 < v.re) :

u * u.beta_integral (v + 1) = v * (u + 1).beta_integral v

Recurrence formula for the Beta function.

theorem complex.beta_integral_eval_nat_add_one_right {u : ℂ} (hu : 0 < u.re) (n : ℕ) :

u.beta_integral (↑n + 1) = ↑(n.factorial) / (finset.range (n + 1)).prod (λ (j : ℕ), u + ↑j)

Explicit formula for the Beta function when second argument is a positive integer.

The Euler limit formula #

noncomputable def complex.Gamma_seq (s : ℂ) (n : ℕ) :

The sequence with n-th term n ^ s * n! / (s * (s + 1) * ... * (s + n)), for complex s. We will show that this tends to Γ(s) as n → ∞.

Equations

s.Gamma_seq n = ↑n ^ s * ↑(n.factorial) / (finset.range (n + 1)).prod (λ (j : ℕ), s + ↑j)

theorem complex.Gamma_seq_eq_beta_integral_of_re_pos {s : ℂ} (hs : 0 < s.re) (n : ℕ) :

s.Gamma_seq n = ↑n ^ s * s.beta_integral (↑n + 1)

theorem complex.Gamma_seq_add_one_left (s : ℂ) {n : ℕ} (hn : n ≠ 0) :

(s + 1).Gamma_seq n / s = ↑n / (↑n + 1 + s) * s.Gamma_seq n

theorem complex.Gamma_seq_eq_approx_Gamma_integral {s : ℂ} (hs : 0 < s.re) {n : ℕ} (hn : n ≠ 0) :

s.Gamma_seq n = ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)

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

filter.tendsto (λ (n : ℕ), ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) filter.at_top (nhds (complex.Gamma s))

The main techical lemma for Gamma_seq_tendsto_Gamma, expressing the integral defining the Gamma function for 0 < re s as the limit of a sequence of integrals over finite intervals.

theorem complex.Gamma_seq_tendsto_Gamma (s : ℂ) :

filter.tendsto s.Gamma_seq filter.at_top (nhds (complex.Gamma s))

Euler's limit formula for the complex Gamma function.

The reflection formula #

theorem complex.Gamma_seq_mul (z : ℂ) {n : ℕ} (hn : n ≠ 0) :

z.Gamma_seq n * (1 - z).Gamma_seq n = ↑n / (↑n + 1 - z) * (1 / (z * (finset.range n).prod (λ (j : ℕ), 1 - z ^ 2 / (↑j + 1) ^ 2)))

theorem complex.Gamma_mul_Gamma_one_sub (z : ℂ) :

complex.Gamma z * complex.Gamma (1 - z) = ↑real.pi / complex.sin (↑real.pi * z)

Euler's reflection formula for the complex Gamma function.

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

complex.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 complex.Gamma_eq_zero_iff (s : ℂ) :

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

noncomputable def real.Gamma_seq (s : ℝ) (n : ℕ) :

The sequence with n-th term n ^ s * n! / (s * (s + 1) * ... * (s + n)), for real s. We will show that this tends to Γ(s) as n → ∞.

Equations

s.Gamma_seq n = ↑n ^ s * ↑(n.factorial) / (finset.range (n + 1)).prod (λ (j : ℕ), s + ↑j)

theorem real.Gamma_seq_tendsto_Gamma (s : ℝ) :

filter.tendsto s.Gamma_seq filter.at_top (nhds (real.Gamma s))

Euler's limit formula for the real Gamma function.

theorem real.Gamma_mul_Gamma_one_sub (s : ℝ) :

real.Gamma s * real.Gamma (1 - s) = real.pi / real.sin (real.pi * s)

Euler's reflection formula for the real Gamma function.