English
For complex s and t with positive real parts, the Gamma function satisfies Gamma(s) Gamma(t) = Gamma(s+t) times the beta integral BetaIntegral(s,t).
Русский
Для комплексных s, t с положительной последовательностью действительных частей выполняется Γ(s) Γ(t) = Γ(s+t) βIntegral(s,t).
LaTeX
$$$$ \\Gamma(s) \\Gamma(t) = \\Gamma(s+t) \\betaIntegral s t $$$$
Lean4
/-- Relation between Beta integral and Gamma function. -/
theorem Gamma_mul_Gamma_eq_betaIntegral {s t : ℂ} (hs : 0 < re s) (ht : 0 < re t) :
Gamma s * Gamma t = Gamma (s + t) * betaIntegral s t := by
-- Note that we haven't proved (yet) that the Gamma function has no zeroes, so we can't formulate
-- this as a formula for the Beta function.
have conv_int :=
integral_posConvolution (GammaIntegral_convergent hs) (GammaIntegral_convergent ht) (ContinuousLinearMap.mul ℝ ℂ)
simp_rw [ContinuousLinearMap.mul_apply'] at conv_int
have hst : 0 < re (s + t) := by rw [add_re]; exact add_pos hs ht
rw [Gamma_eq_integral hs, Gamma_eq_integral ht, Gamma_eq_integral hst, GammaIntegral, GammaIntegral, GammaIntegral, ←
conv_int, ← MeasureTheory.integral_mul_const (betaIntegral _ _)]
refine setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_
rw [mul_assoc, ← betaIntegral_scaled s t hx, ← intervalIntegral.integral_const_mul]
congr 1 with y : 1
push_cast
suffices Complex.exp (-x) = Complex.exp (-y) * Complex.exp (-(x - y)) by rw [this]; ring
rw [← Complex.exp_add]; congr 1; abel
