gaussianPDF_pos

Mathlib.Probability.Distributions.Gaussian.Real

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

← MathLib Explorer

English

For μ ∈ ℝ, v ∈ ℝ≥0 with v ≠ 0, and x ∈ ℝ, 0 < gaussianPDF μ v x.

Русский

Для μ ∈ ℝ, v ≠ 0, x ∈ ℝ, верно 0 < gaussianPDF μ v x.

LaTeX

$$$0 < gaussianPDF\\mu \\ v \\ x$$$

Lean4

theorem gaussianPDF_pos (μ : ℝ) {v : ℝ≥0} (hv : v ≠ 0) (x : ℝ) : 0 < gaussianPDF μ v x :=
  by
  rw [gaussianPDF, ENNReal.ofReal_pos]
  exact gaussianPDFReal_pos _ _ _ hv

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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