English
The Euler integral defining the Gamma function converges for positive real s.
Русский
Эйлеров интеграл, задающий гамма-функцию, сходится при положительном действительном s.
LaTeX
$$$$ \text{If } s > 0, \quad \int_{0}^{\infty} e^{-x} x^{s-1} \, dx \text{ converges}. $$$$
Lean4
/-- The Euler integral for the `Γ` function converges for positive real `s`. -/
theorem GammaIntegral_convergent {s : ℝ} (h : 0 < s) : IntegrableOn (fun x : ℝ => exp (-x) * x ^ (s - 1)) (Ioi 0) :=
by
rw [← Ioc_union_Ioi_eq_Ioi (@zero_le_one ℝ _ _ _ _), integrableOn_union]
constructor
· rw [← integrableOn_Icc_iff_integrableOn_Ioc]
refine IntegrableOn.continuousOn_mul continuousOn_id.neg.rexp ?_ isCompact_Icc
refine (intervalIntegrable_iff_integrableOn_Icc_of_le zero_le_one).mp ?_
exact intervalIntegrable_rpow' (by linarith)
· refine integrable_of_isBigO_exp_neg one_half_pos ?_ (Gamma_integrand_isLittleO _).isBigO
refine continuousOn_id.neg.rexp.mul (continuousOn_id.rpow_const ?_)
intro x hx
exact Or.inl ((zero_lt_one : (0 : ℝ) < 1).trans_le hx).ne'
