integral_gaussianPDFReal_eq_one — Mathlib

English

For μ ∈ ℝ and v ≠ 0, the ordinary integral ∫ gaussianPDFReal μ v x dx equals 1.

Русский

Для μ ∈ ℝ и v ≠ 0, ∫ gaussianPDFReal μ v x dx = 1.

LaTeX

$$$\int x gaussianPDFReal\\mu \\ v \\ x = 1$$$

Lean4

/-- The Gaussian distribution pdf integrates to 1 when the variance is not zero. -/
theorem integral_gaussianPDFReal_eq_one (μ : ℝ) {v : ℝ≥0} (hv : v ≠ 0) : ∫ x, gaussianPDFReal μ v x = 1 :=
  by
  have h := lintegral_gaussianPDFReal_eq_one μ hv
  rw [← ofReal_integral_eq_lintegral_ofReal (integrable_gaussianPDFReal _ _) (ae_of_all _ (gaussianPDFReal_nonneg _ _)),
    ← ENNReal.ofReal_one] at h
  rwa [← ENNReal.ofReal_eq_ofReal_iff (integral_nonneg (gaussianPDFReal_nonneg _ _)) zero_le_one]

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