English
For complex s with Re(s) > 0, the Euler integral defining Γ(s) converges (the integral defining Γ(s) is integrable on (0, ∞)).
Русский
Для комплексного числа s с Re(s) > 0 интеграл Эйлера, задающий Γ(s), сходится (интеграл на (0, ∞) интегрируем по модулю).
LaTeX
$$$$ \int_{0}^{\infty} |x^{s-1} e^{-x}| \, dx < \infty \quad \text{for} \quad \operatorname{Re}(s) > 0. $$$$
Lean4
/-- The integral defining the `Γ` function converges for complex `s` with `0 < re s`.
This is proved by reduction to the real case. -/
theorem GammaIntegral_convergent {s : ℂ} (hs : 0 < s.re) :
IntegrableOn (fun x => (-x).exp * x ^ (s - 1) : ℝ → ℂ) (Ioi 0) :=
by
constructor
· refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioi
apply (continuous_ofReal.comp continuous_neg.rexp).continuousOn.mul
apply continuousOn_of_forall_continuousAt
intro x hx
have : ContinuousAt (fun x : ℂ => x ^ (s - 1)) ↑x := continuousAt_cpow_const <| ofReal_mem_slitPlane.2 hx
exact ContinuousAt.comp this continuous_ofReal.continuousAt
· rw [← hasFiniteIntegral_norm_iff]
refine HasFiniteIntegral.congr (Real.GammaIntegral_convergent hs).2 ?_
apply (ae_restrict_iff' measurableSet_Ioi).mpr
filter_upwards with x hx
rw [norm_mul, Complex.norm_of_nonneg <| le_of_lt <| exp_pos <| -x, norm_cpow_eq_rpow_re_of_pos hx _]
simp
