English
For every real s > 0, the Gamma function equals the improper integral Γ(s) = ∫_0^∞ e^{-x} x^{s-1} dx.
Русский
Для каждого действительного s > 0 гамма-функция равна несобственному интегралу Γ(s) = ∫_0^∞ e^{-x} x^{s-1} dx.
LaTeX
$$$\Gamma(s) = \displaystyle \int_{0}^{\infty} e^{-x} x^{s-1}\,dx \quad\text{for } s>0$$$
Lean4
theorem Gamma_eq_integral {s : ℝ} (hs : 0 < s) : Gamma s = ∫ x in Ioi 0, exp (-x) * x ^ (s - 1) :=
by
rw [Gamma, Complex.Gamma_eq_integral (by rwa [Complex.ofReal_re] : 0 < Complex.re s)]
dsimp only [Complex.GammaIntegral]
simp_rw [← Complex.ofReal_one, ← Complex.ofReal_sub]
suffices
∫ x : ℝ in Ioi 0, ↑(exp (-x)) * (x : ℂ) ^ ((s - 1 : ℝ) : ℂ) = ∫ x : ℝ in Ioi 0, ((exp (-x) * x ^ (s - 1) : ℝ) : ℂ)
by
have cc : ∀ r : ℝ, Complex.ofReal r = @RCLike.ofReal ℂ _ r := fun r => rfl
conv_lhs => rw [this]; enter [1, 2, x]; rw [cc]
rw [_root_.integral_ofReal, ← cc, Complex.ofReal_re]
refine setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_
push_cast
rw [Complex.ofReal_cpow (le_of_lt hx)]
push_cast; rfl
