integral_rpow_mul_exp_neg_mul_rpow

English

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

Русский

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

LaTeX

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

Lean4

theorem integral_rpow_mul_exp_neg_mul_rpow {p q b : ℝ} (hp : 1 ≤ p) (hq : -2 < q) (hb : 0 < b) :
    ∫ x : ℂ, ‖x‖ ^ q * rexp (-b * ‖x‖ ^ p) = (2 * π / p) * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p) := by
  calc
    _ = ∫ x in Ioi (0 : ℝ) ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-b * |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 (-b * |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 (-b * |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 (-b * 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 * π / p) * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p) :=
      by
      rw [_root_.integral_rpow_mul_exp_neg_mul_rpow (by linarith) (by linarith) hb, add_assoc, one_add_one_eq_two]
      ring

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