English
Let p > 0 and q > -1. Then the improper integral ∫_0^∞ x^q e^(−x^p) dx converges and equals (1/p) Γ((q+1)/p).
Русский
Пусть p > 0 и q > −1. Тогда интеграл ∫_0^∞ x^q e^(−x^p) dx сходится и равен (1/p) Γ((q+1)/p).
LaTeX
$$$ \displaystyle \int_{0}^{\infty} x^{q} e^{-x^{p}} \, dx = \frac{1}{p} \; \Gamma\left(\frac{q+1}{p}\right), \quad p>0,\ q>-1 $$$
Lean4
theorem integral_rpow_mul_exp_neg_rpow {p q : ℝ} (hp : 0 < p) (hq : -1 < q) :
∫ x in Ioi (0 : ℝ), x ^ q * exp (-x ^ p) = (1 / p) * Gamma ((q + 1) / p) := by
calc
_ = ∫ (x : ℝ) in Ioi 0, (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * exp (-x)) :=
by
rw [← integral_comp_rpow_Ioi _ (one_div_ne_zero (ne_of_gt hp)), abs_eq_self.mpr (le_of_lt (one_div_pos.mpr hp))]
refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)
rw [← rpow_mul (le_of_lt hx) _ p, one_div_mul_cancel (ne_of_gt hp), rpow_one]
_ = ∫ (x : ℝ) in Ioi 0, 1 / p * exp (-x) * x ^ (1 / p - 1 + q / p) :=
by
simp_rw [smul_eq_mul, mul_assoc]
refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)
rw [← rpow_mul (le_of_lt hx), div_mul_eq_mul_div, one_mul, rpow_add hx]
ring_nf
_ = (1 / p) * Gamma ((q + 1) / p) :=
by
rw [Gamma_eq_integral (div_pos (neg_lt_iff_pos_add.mp hq) hp)]
simp_rw [show 1 / p - 1 + q / p = (q + 1) / p - 1 by field_simp; ring, ← integral_const_mul, ← mul_assoc]
