integral_exp_neg_rpow — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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