integrable_mul_cexp_neg_mul_sq — Mathlib

English

For hb with Re(b) > 0, the complex-valued function x -> exp(-b x^2) is integrable on R.

Русский

Пусть Re(b) > 0. Комплекснозначная функция x -> exp(-b x^2) интегрируема на R.

LaTeX

$$$$\\int_{-\\infty}^{\\infty} |e^{-b x^2}|\, dx < \\infty.$$$$

Lean4

theorem integrable_mul_cexp_neg_mul_sq {b : ℂ} (hb : 0 < b.re) : Integrable fun x : ℝ => ↑x * cexp (-b * (x : ℂ) ^ 2) :=
  by
  refine ⟨(continuous_ofReal.mul (Complex.continuous_exp.comp ?_)).aestronglyMeasurable, ?_⟩
  · exact continuous_const.mul (continuous_ofReal.pow 2)
  have := (integrable_mul_exp_neg_mul_sq hb).hasFiniteIntegral
  rw [← hasFiniteIntegral_norm_iff] at this ⊢
  convert this
  rw [norm_mul, norm_mul, norm_cexp_neg_mul_sq b, norm_real, norm_of_nonneg (exp_pos _).le]

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