English
For b ∈ R with b > 0, exp(-b x^2) is integrable on (0, ∞). Conversely, if exp(-b x^2) is integrable on (0, ∞), then b > 0.
Русский
Для b > 0 exp(-b x^2) интегрируема на (0, ∞); наоборот, если интегрируема на (0, ∞), то b > 0.
LaTeX
$$$$\\int_0^{\\infty} e^{-b x^2} dx < \\infty \\quad \\Longleftrightarrow \\quad b > 0.$$$$
Lean4
theorem integrableOn_Ioi_exp_neg_mul_sq_iff {b : ℝ} : IntegrableOn (fun x : ℝ => exp (-b * x ^ 2)) (Ioi 0) ↔ 0 < b :=
by
refine ⟨fun h => ?_, fun h => (integrable_exp_neg_mul_sq h).integrableOn⟩
by_contra! hb
have : ∫⁻ _ : ℝ in Ioi 0, 1 ≤ ∫⁻ x : ℝ in Ioi 0, ‖exp (-b * x ^ 2)‖₊ :=
by
apply lintegral_mono (fun x ↦ _)
simp only [neg_mul, ENNReal.one_le_coe_iff, ← toNNReal_one, toNNReal_le_iff_le_coe,
Real.norm_of_nonneg (exp_pos _).le, coe_nnnorm, one_le_exp_iff, Right.nonneg_neg_iff]
exact fun x ↦ mul_nonpos_of_nonpos_of_nonneg hb (sq_nonneg x)
simpa using this.trans_lt h.2
