gaussianPDFReal_nonneg

Mathlib.Probability.Distributions.Gaussian.Real

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

← MathLib Explorer

English

Let μ ∈ ℝ, v ∈ ℝ≥0, x ∈ ℝ. Then gaussianPDFReal μ v x ≥ 0.

Русский

Пусть μ ∈ ℝ, v ∈ ℝ≥0 и x ∈ ℝ. Тогда gaussianPDFReal μ v x ≥ 0.

LaTeX

$$$0 \le gaussianPDFReal(\\mu, \\ v, \\ x)$$$

Lean4

/-- The Gaussian pdf is nonnegative. -/
theorem gaussianPDFReal_nonneg (μ : ℝ) (v : ℝ≥0) (x : ℝ) : 0 ≤ gaussianPDFReal μ v x :=
  by
  rw [gaussianPDFReal]
  positivity

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

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

Разделы

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

Аффилиация

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