integrable_exp_neg_mul_sq_iff — Mathlib

English

The integral over the whole line of exp(-b x^2) is finite if and only if b > 0.

Русский

Интеграл по всей оси exp(-b x^2) конечен тогда и только тогда, когда b > 0.

LaTeX

$$$$\\int_{-\\\\infty}^{\\\\infty} e^{-b x^2} dx < \\infty \\Longleftrightarrow b > 0.$$$$

Lean4

theorem integrable_exp_neg_mul_sq_iff {b : ℝ} : (Integrable fun x : ℝ => exp (-b * x ^ 2)) ↔ 0 < b :=
  ⟨fun h => integrableOn_Ioi_exp_neg_mul_sq_iff.mp h.integrableOn, integrable_exp_neg_mul_sq⟩

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