English
Γ(s) = 0 iff s is a non-positive integer, i.e., s = -m for some m ∈ ℕ.
Русский
Γ(s) = 0 тогда и только тогда, когда s является не положительным целым числом, то есть s = -m для некоторого m ∈ ℕ.
LaTeX
$$$\Gamma(s) = 0 \iff \exists m\in\mathbb{N},\; s = -m$$$
Lean4
/-- Expresses the integral over `Ioi 0` of `t ^ (a - 1) * exp (-(r * t))`, for positive real `r`,
in terms of the Gamma function. -/
theorem integral_rpow_mul_exp_neg_mul_Ioi {a r : ℝ} (ha : 0 < a) (hr : 0 < r) :
∫ t : ℝ in Ioi 0, t ^ (a - 1) * exp (-(r * t)) = (1 / r) ^ a * Gamma a :=
by
rw [← ofReal_inj, ofReal_mul, ← Gamma_ofReal, ofReal_cpow (by positivity), ofReal_div]
convert integral_cpow_mul_exp_neg_mul_Ioi (by rwa [ofReal_re] : 0 < (a : ℂ).re) hr
refine integral_ofReal.symm.trans <| setIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ ?_)
norm_cast
simp_rw [← ofReal_cpow ht.le, RCLike.ofReal_mul, coe_algebraMap]
