bayesRisk_zero_right

Mathlib.Probability.Decision.Risk.Defs

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

← MathLib Explorer

English

If P is a kernel, Bayes risk with zero prior is zero.

Русский

Если задан ядро, байесовский риск с нулевымPrior равен нулю.

LaTeX

$$$\\text{bayesRisk}_ℓ(P, 0) = 0$$$

Lean4

@[simp]
theorem bayesRisk_zero_right [Nonempty 𝓨] (ℓ : Θ → 𝓨 → ℝ≥0∞) (P : Kernel Θ 𝓧) : bayesRisk ℓ P (0 : Measure Θ) = 0 := by
  simp [bayesRisk, iInf_subtype']

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

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

Разделы

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

Аффилиация

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