gaussianPDFReal_def — Mathlib

English

The Gaussian density is defined by the standard formula (2πv)^{-1/2} exp(-(x-μ)^2/(2v)).

Русский

Плотность гауссова распределения задается формулой (2πv)^{-1/2} exp(-(x-μ)^2/(2v)).

LaTeX

$$$gaussianPDFReal(μ,v,x) = (\\sqrt{2\\pi v})^{-1} \\cdot \\exp(- (x-μ)^2 /(2v))$$$

Lean4

theorem gaussianPDFReal_def (μ : ℝ) (v : ℝ≥0) :
    gaussianPDFReal μ v = fun x ↦ (√(2 * π * v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * v)) :=
  rfl

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