gaussianPDF — Mathlib

English

The pdf of a Gaussian distribution on ℝ with mean μ and variance v is defined by gaussianPDF μ v x = ENNReal.ofReal (gaussianPDFReal μ v x).

Русский

Плотность распределения Гаусса на ℝ с математическим ожиданием μ и дисперсией v определяется как gaussianPDF μ v x = ENNReal.ofReal (gaussianPDFReal μ v x).

LaTeX

$$$gaussianPDF(\\mu \\ v \\ x) = ENNReal.ofReal (gaussianPDFReal\\mu \\ v \\ x)$$$

Lean4

/-- The pdf of a Gaussian distribution on ℝ with mean `μ` and variance `v`. -/
noncomputable def gaussianPDF (μ : ℝ) (v : ℝ≥0) (x : ℝ) : ℝ≥0∞ :=
  ENNReal.ofReal (gaussianPDFReal μ v x)

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