integral_exp_neg_mul_rpow — Mathlib

English

Let p ≥ 1 and b > 0. Then ∫ z∈ℂ e^{−b‖z‖^p} d z = π b^{−2/p} Γ(2/p + 1).

Русский

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

LaTeX

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

Lean4

theorem integral_exp_neg_mul_rpow {p b : ℝ} (hp : 1 ≤ p) (hb : 0 < b) :
    ∫ x : ℂ, rexp (-b * ‖x‖ ^ p) = π * b ^ (-2 / p) * Real.Gamma (2 / p + 1) :=
  by
  convert (integral_rpow_mul_exp_neg_mul_rpow hp (by linarith : (-2 : ℝ) < 0)) hb using 1
  · simp_rw [rpow_zero, one_mul]
  · rw [zero_add, Real.Gamma_add_one (div_ne_zero two_ne_zero (by linarith))]
    ring

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