gaussianReal_of_var_ne_zero

Mathlib.Probability.Distributions.Gaussian.Real

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

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

theorem gaussianReal_of_var_ne_zero (μ : ℝ) {v : ℝ≥0} (hv : v ≠ 0) :
    gaussianReal μ v = volume.withDensity (gaussianPDF μ v) :=
  if_neg hv

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

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

Разделы

Аффилиация

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