integral_exp_neg_rpow — Mathlib

English

Let p > 0 and q > -1. Then ∫_0^∞ x^q e^(−b x^p) dx = b^{−(q+1)/p} (1/p) Γ((q+1)/p).

Русский

Пусть p > 0 и q > −1. Тогда ∫_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) $$$

Lean4

theorem integral_exp_neg_rpow {p : ℝ} (hp : 0 < p) : ∫ x in Ioi (0 : ℝ), exp (-x ^ p) = Gamma (1 / p + 1) :=
  by
  convert (integral_rpow_mul_exp_neg_rpow hp neg_one_lt_zero) using 1
  · simp_rw [rpow_zero, one_mul]
  · rw [zero_add, Gamma_add_one (one_div_ne_zero (ne_of_gt hp))]

Похожие утверждения