English
Let p > 0, q > -1, b > 0. Then ∫_0^∞ x^q e^(−b x^p) dx = b^{−(q+1)/p} (1/p) Γ((q+1)/p).
Русский
Пусть p > 0, q > -1, b > 0. Тогда ∫_0^∞ x^q e^(−b x^p) dx = b^{−(q+1)/p} (1/p) Γ((q+1)/p).
LaTeX
$$$ \displaystyle \int_{0}^{\infty} x^{q} e^{-b x^{p}} \, dx = b^{-(q+1)/p} \frac{1}{p} \Gamma\left(\frac{q+1}{p}\right), \quad p>0, q>-1, b>0 $$$
Lean4
theorem integral_rpow_mul_exp_neg_mul_rpow {p q b : ℝ} (hp : 0 < p) (hq : -1 < q) (hb : 0 < b) :
∫ x in Ioi (0 : ℝ), x ^ q * exp (-b * x ^ p) = b ^ (-(q + 1) / p) * (1 / p) * Gamma ((q + 1) / p) := by
calc
_ = ∫ x in Ioi (0 : ℝ), b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p)) :=
by
refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)
rw [mul_rpow _ (le_of_lt hx), mul_rpow _ (le_of_lt hx), ← rpow_mul, ← rpow_mul, inv_mul_cancel₀, rpow_one,
mul_assoc, ← mul_assoc, ← rpow_add, neg_mul p⁻¹, neg_add_cancel, rpow_zero, one_mul, neg_mul]
all_goals positivity
_ = (b ^ p⁻¹)⁻¹ * ∫ x in Ioi (0 : ℝ), b ^ (-p⁻¹ * q) * (x ^ q * rexp (-x ^ p)) :=
by
rw [integral_comp_mul_left_Ioi (fun x => b ^ (-p⁻¹ * q) * (x ^ q * exp (-x ^ p))) 0, mul_zero, smul_eq_mul]
all_goals positivity
_ = b ^ (-(q + 1) / p) * (1 / p) * Gamma ((q + 1) / p) :=
by
rw [integral_const_mul, integral_rpow_mul_exp_neg_rpow _ hq, mul_assoc, ← mul_assoc, ← rpow_neg_one, ← rpow_mul, ←
rpow_add]
· congr; ring
all_goals positivity
