English
For μ ∈ ℝ and v ∈ ℝ≥0 with v ≠ 0, the lintegral of ENNReal.ofReal(gaussianPDFReal μ v x) over x equals 1.
Русский
Пусть μ ∈ ℝ и v ∈ ℝ≥0 с v ≠ 0. lntegral ENNReal.ofReal(gaussianPDFReal μ v x) по x равно 1.
LaTeX
$$$\int^{-}_{x} ENNReal.ofReal(gaussianPDFReal\\mu \\ v \\ x) = 1$$$
Lean4
/-- The Gaussian distribution pdf integrates to 1 when the variance is not zero. -/
theorem lintegral_gaussianPDFReal_eq_one (μ : ℝ) {v : ℝ≥0} (h : v ≠ 0) :
∫⁻ x, ENNReal.ofReal (gaussianPDFReal μ v x) = 1 :=
by
rw [← ENNReal.toReal_eq_one_iff]
have hfm : AEStronglyMeasurable (gaussianPDFReal μ v) volume := by fun_prop
have hf : 0 ≤ₐₛ gaussianPDFReal μ v := ae_of_all _ (gaussianPDFReal_nonneg μ v)
rw [← integral_eq_lintegral_of_nonneg_ae hf hfm]
simp only [gaussianPDFReal, integral_const_mul]
rw [integral_sub_right_eq_self (μ := volume) (fun a ↦ rexp (-a ^ 2 / ((2 : ℝ) * v))) μ]
simp only [div_eq_inv_mul, mul_inv_rev, mul_neg]
simp_rw [← neg_mul]
rw [neg_mul, integral_gaussian, ← Real.sqrt_inv, ← Real.sqrt_mul]
· simp [field]
· positivity
