The Beta function, and further properties of the Gamma function #
In this file we define the Beta integral, relate Beta and Gamma functions, and prove some refined properties of the Gamma function using these relations.
Results on the Beta function #
complex.beta_integral
: the Beta functionΒ(u, v)
, whereu
,v
are complex with positive real part.complex.Gamma_mul_Gamma_eq_beta_integral
: the formulaGamma u * Gamma v = Gamma (u + v) * beta_integral u v
.
Results on the Gamma function #
complex.Gamma_ne_zero
: for alls : ℂ
withs ∉ {-n : n ∈ ℕ}
we haveΓ s ≠ 0
.complex.Gamma_seq_tendsto_Gamma
: for alls
, the limit asn → ∞
of the sequencen ↦ n ^ s * n! / (s * (s + 1) * ... * (s + n))
isΓ(s)
.complex.Gamma_mul_Gamma_one_sub
: Euler's reflection formulaGamma s * Gamma (1 - s) = π / sin π s
.complex.differentiable_one_div_Gamma
: the function1 / Γ(s)
is differentiable everywhere.real.Gamma_ne_zero
,real.Gamma_seq_tendsto_Gamma
,real.Gamma_mul_Gamma_one_sub
: real versions of the above results.
The Beta function #
Relation between Beta integral and Gamma function.
Recurrence formula for the Beta function.
The Euler limit formula #
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.
Euler's limit formula for the complex Gamma function.
The reflection formula #
Euler's reflection formula for the complex Gamma function.
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).
Euler's limit formula for the real Gamma function.
Euler's reflection formula for the real Gamma function.
The reciprocal Gamma function #
We show that the reciprocal Gamma function 1 / Γ(s)
is entire. These lemmas show that (in this
case at least) mathlib's conventions for division by zero do actually give a mathematically useful
answer! (These results are useful in the theory of zeta and L-functions.)
A reformulation of the Gamma recurrence relation which is true for s = 0
as well.
The reciprocal of the Gamma function is differentiable everywhere (including the points where Gamma itself is not).