English
For a with Re(a) > 0 and r > 0, ∫_0^∞ t^{a-1} e^{-(r t)} dt = (1/r)^a Γ(a).
Русский
При Re(a) > 0 и r > 0, ∫_0^∞ t^{a-1} e^{-(r t)} dt = (1/r)^a Γ(a).
LaTeX
$$$$ \int_{0}^{\infty} t^{a-1} e^{-r t} \, dt = (1/r)^{a} \ Gamma(a). $$$$
Lean4
/-- Expresses the integral over `Ioi 0` of `t ^ (a - 1) * exp (-(r * t))` in terms of the Gamma
function, for complex `a`. -/
theorem integral_cpow_mul_exp_neg_mul_Ioi {a : ℂ} {r : ℝ} (ha : 0 < a.re) (hr : 0 < r) :
∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * exp (-(r * t)) = (1 / r) ^ a * Gamma a :=
by
have aux : (1 / r : ℂ) ^ a = 1 / r * (1 / r) ^ (a - 1) :=
by
nth_rewrite 2 [← cpow_one (1 / r : ℂ)]
rw [← cpow_add _ _ (one_div_ne_zero <| ofReal_ne_zero.mpr hr.ne'), add_sub_cancel]
calc
_ = ∫ (t : ℝ) in Ioi 0, (1 / r) ^ (a - 1) * (r * t) ^ (a - 1) * exp (-(r * t)) :=
by
refine MeasureTheory.setIntegral_congr_fun measurableSet_Ioi (fun x hx ↦ ?_)
rw [mem_Ioi] at hx
rw [mul_cpow_ofReal_nonneg hr.le hx.le, ← mul_assoc, one_div, ← ofReal_inv, ←
mul_cpow_ofReal_nonneg (inv_pos.mpr hr).le hr.le, ← ofReal_mul r⁻¹, inv_mul_cancel₀ hr.ne', ofReal_one,
one_cpow, one_mul]
_ = 1 / r * ∫ (t : ℝ) in Ioi 0, (1 / r) ^ (a - 1) * t ^ (a - 1) * exp (-t) :=
by
simp_rw [← ofReal_mul]
rw [integral_comp_mul_left_Ioi (fun x ↦ _ * x ^ (a - 1) * exp (-x)) _ hr, mul_zero, real_smul, ← one_div,
ofReal_div, ofReal_one]
_ = 1 / r * (1 / r : ℂ) ^ (a - 1) * (∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * exp (-t)) := by
simp_rw [← MeasureTheory.integral_const_mul, mul_assoc]
_ = (1 / r) ^ a * Gamma a := by
rw [aux, Gamma_eq_integral ha]
congr 2 with x
rw [ofReal_exp, ofReal_neg, mul_comm]
