English
If s is real, then ΓIntegral(s) equals the complex embedding of the real Euler integral ∫_0^∞ e^{-x} x^{s-1} dx.
Русский
Если s вещественно, то ΓIntegral(s) равен комплексному отображению вещественного интеграла Эйлера ∫_0^∞ e^{-x} x^{s-1} dx.
LaTeX
$$$$ \GammaIntegral(\mathrm{ofReal}(s)) = \mathrm{ofReal}\left( \int_{0}^{\infty} e^{-x} x^{s-1} \, dx \right). $$$$
Lean4
theorem GammaIntegral_ofReal (s : ℝ) : GammaIntegral ↑s = ↑(∫ x : ℝ in Ioi 0, Real.exp (-x) * x ^ (s - 1)) :=
by
have : ∀ r : ℝ, Complex.ofReal r = @RCLike.ofReal ℂ _ r := fun r => rfl
rw [GammaIntegral]
conv_rhs => rw [this, ← _root_.integral_ofReal]
refine setIntegral_congr_fun measurableSet_Ioi ?_
intro x hx; dsimp only
conv_rhs => rw [← this]
rw [ofReal_mul, ofReal_cpow (mem_Ioi.mp hx).le]
simp
