gaussianReal — Mathlib

English

A Gaussian distribution on ℝ with mean μ and variance v is defined as the Dirac measure at μ when v = 0, otherwise volume with density gaussianPDF μ v.

Русский

Распределение Гаусса на ℝ с параметрами μ и v определяется как дираковская мера в точке μ при v = 0, иначе — мера объема с плотностью gaussianPDF μ v.

LaTeX

$$gaussianReal\\mu \\ v = \begin{cases}Measure.dirac\\mu, & v = 0 \\ volume.withDensity (gaussianPDF\\mu \\ v), & v ≠ 0\end{cases}$$

Lean4

/-- A Gaussian distribution on `ℝ` with mean `μ` and variance `v`. -/
noncomputable def gaussianReal (μ : ℝ) (v : ℝ≥0) : Measure ℝ :=
  if v = 0 then Measure.dirac μ else volume.withDensity (gaussianPDF μ v)

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