English
Let p ≥ 1 and q > −2. Then ∫ z∈ℂ ‖z‖^q e^{−‖z‖^p} = (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}}} \; d z = \frac{2\pi}{p} \; \Gamma\left(\frac{q+2}{p}\right) $$$
Lean4
theorem integral_rpow_mul_exp_neg_rpow {p q : ℝ} (hp : 1 ≤ p) (hq : -2 < q) :
∫ x : ℂ, ‖x‖ ^ q * rexp (-‖x‖ ^ p) = (2 * π / p) * Real.Gamma ((q + 2) / p) := by
calc
_ = ∫ x in Ioi (0 : ℝ) ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)) :=
by
rw [← Complex.integral_comp_polarCoord_symm, polarCoord_target]
simp_rw [Complex.norm_polarCoord_symm, smul_eq_mul]
_ = (∫ x in Ioi (0 : ℝ), x * |x| ^ q * rexp (-|x| ^ p)) * ∫ _ in Ioo (-π) π, 1 :=
by
rw [← setIntegral_prod_mul, volume_eq_prod]
simp_rw [mul_one]
congr! 2; ring
_ = 2 * π * ∫ x in Ioi (0 : ℝ), x * |x| ^ q * rexp (-|x| ^ p) := by
simp_rw [integral_const, measureReal_restrict_apply MeasurableSet.univ, Set.univ_inter,
volume_real_Ioo_of_le (a := -π) (b := π) (by linarith [pi_nonneg]), sub_neg_eq_add, ← two_mul, smul_eq_mul,
mul_one, mul_comm]
_ = 2 * π * ∫ x in Ioi (0 : ℝ), x ^ (q + 1) * rexp (-x ^ p) :=
by
congr 1
refine setIntegral_congr_fun measurableSet_Ioi (fun x hx => ?_)
rw [mem_Ioi] at hx
rw [abs_eq_self.mpr hx.le, rpow_add hx, rpow_one]
ring
_ = (2 * Real.pi / p) * Real.Gamma ((q + 2) / p) :=
by
rw [_root_.integral_rpow_mul_exp_neg_rpow (by linarith) (by linarith), add_assoc, one_add_one_eq_two]
ring
