densityProcess_nonneg

Mathlib.Probability.Kernel.Disintegration.Density

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.Kernel.densityProcess_nonneg

← MathLib Explorer

English

For all κ, ν, n, a, x, s, the densityProcess is nonnegative.

Русский

Для любых κ, ν, n, a, x, s плотность неотрицательна.

LaTeX

$$$0 \le\ \text{densityProcess}(\kappa,\nu,n,a,x,s)$$$

Lean4

theorem densityProcess_nonneg (κ : Kernel α (γ × β)) (ν : Kernel α γ) (n : ℕ) (a : α) (x : γ) (s : Set β) :
    0 ≤ densityProcess κ ν n a x s :=
  ENNReal.toReal_nonneg

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

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

Разделы

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

Аффилиация

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