English
For all μ ∈ ℝ and v ∈ ℝ≥0, gaussianPDFReal μ v is integrable over ℝ.
Русский
Пусть μ ∈ ℝ и v ∈ ℝ≥0. gaussianPDFReal μ v интегрируема по ℝ.
LaTeX
$$$\text{Integrable}(gaussianPDFReal\\mu \\ v)$$$
Lean4
@[fun_prop]
theorem integrable_gaussianPDFReal (μ : ℝ) (v : ℝ≥0) : Integrable (gaussianPDFReal μ v) :=
by
rw [gaussianPDFReal_def]
by_cases hv : v = 0
· simp [hv]
let g : ℝ → ℝ := fun x ↦ (√(2 * π * v))⁻¹ * rexp (-x ^ 2 / (2 * v))
have hg : Integrable g :=
by
suffices g = fun x ↦ (√(2 * π * v))⁻¹ * rexp (-(2 * v)⁻¹ * x ^ 2)
by
rw [this]
refine (integrable_exp_neg_mul_sq ?_).const_mul (√(2 * π * v))⁻¹
simp [lt_of_le_of_ne (zero_le _) (Ne.symm hv)]
ext x
simp only [g, NNReal.zero_le_coe, Real.sqrt_mul', mul_inv_rev, NNReal.coe_mul, NNReal.coe_inv, NNReal.coe_ofNat,
neg_mul, mul_eq_mul_left_iff, Real.exp_eq_exp, mul_eq_zero, inv_eq_zero, Real.sqrt_eq_zero, NNReal.coe_eq_zero,
hv, false_or]
rw [mul_comm]
left
field_simp
exact Integrable.comp_sub_right hg μ
