gaussianPDFReal_pos — Mathlib

English

The Gaussian density is positive for v ≠ 0 at all x; specifically, g(μ,v,x) > 0 when v > 0.

Русский

Гауссова плотность положительна при v ≠ 0; для v > 0 g(μ,v,x) > 0.

LaTeX

$$$v ≠ 0 \\Rightarrow 0 < gaussianPDFReal(μ,v,x)$$$

Lean4

/-- The Gaussian pdf is positive when the variance is not zero. -/
theorem gaussianPDFReal_pos (μ : ℝ) (v : ℝ≥0) (x : ℝ) (hv : v ≠ 0) : 0 < gaussianPDFReal μ v x :=
  by
  rw [gaussianPDFReal]
  positivity

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