integral_exp_neg_mul_rpow — Mathlib

English

Let p ≥ 1 and q > −2. Then the integral over the complex plane of ‖z‖^q e^{−‖z‖^p} equals (2π/p) Γ((q+2)/p).

Русский

Пусть p ≥ 1 и q > −2. Тогда интеграл по комплексной плоскости от |z|^q e^{−|z|^p} dz равен (2π/p) Γ((q+2)/p).

LaTeX

$$$ \displaystyle \int_{\mathbb{C}} \|z\|^{q} e^{-{\|z\|^{p}}} \, dz = \frac{2\pi}{p} \; \Gamma\left(\frac{q+2}{p}\right), \quad p\ge 1, \ q>-2 $$$

Lean4

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

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