gaussianPDFReal_zero_var

Mathlib.Probability.Distributions.Gaussian.Real

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

English

If the variance parameter v equals 0, then gaussianPDFReal(μ,0,x) = 0 for all x.

Русский

Если дисперсия v равна 0, то gaussianPDFReal(μ,0,x) = 0 для всех x.

LaTeX

$$$gaussianPDFReal(μ,0,x) = 0$ for all x$$

Lean4

@[simp]
theorem gaussianPDFReal_zero_var (m : ℝ) : gaussianPDFReal m 0 = 0 :=
  by
  ext1 x
  simp [gaussianPDFReal]

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

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

Разделы

Аффилиация

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