integrable_cexp_neg_mul_sq — Mathlib

English

Let b > 0. The real-valued Gaussian function exp(-b x^2) is integrable on R.

Русский

Пусть b > 0. Функция exp(-b x^2) интегрируема по мере Лебега на всей прямой.

LaTeX

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

Lean4

theorem integrable_cexp_neg_mul_sq {b : ℂ} (hb : 0 < b.re) : Integrable fun x : ℝ => cexp (-b * (x : ℂ) ^ 2) :=
  by
  refine ⟨(Complex.continuous_exp.comp (continuous_const.mul (continuous_ofReal.pow 2))).aestronglyMeasurable, ?_⟩
  rw [← hasFiniteIntegral_norm_iff]
  simp_rw [norm_cexp_neg_mul_sq]
  exact (integrable_exp_neg_mul_sq hb).2

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