lintegral_gaussianPDF_eq_one

Mathlib.Probability.Distributions.Gaussian.Real

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.lintegral_gaussianPDF_eq_one

English

For μ ∈ ℝ and hv: v ≠ 0, gaussianReal μ v = volume.withDensity (gaussianPDF μ v).

Русский

Для μ ∈ ℝ и v ≠ 0, gaussianReal μ v = volume.withDensity (gaussianPDF μ v).

LaTeX

$$$gaussianReal\\mu \\ v = volume.withDensity (gaussianPDF\\mu \\ v)$$$

Lean4

@[simp]
theorem lintegral_gaussianPDF_eq_one (μ : ℝ) {v : ℝ≥0} (h : v ≠ 0) : ∫⁻ x, gaussianPDF μ v x = 1 :=
  lintegral_gaussianPDFReal_eq_one μ h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru