bayesRisk_of_isEmpty

Mathlib.Probability.Decision.Risk.Defs

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

English

If 𝓧 is empty, Bayes risk is zero.

Русский

Если 𝓧 пусто, байесовский риск равен 0.

LaTeX

$$$[IsEmpty 𝓧] \\Rightarrow bayesRisk_ℓ(P, π) = 0$$$

Lean4

@[simp]
theorem bayesRisk_of_isEmpty [IsEmpty 𝓧] : bayesRisk ℓ P π = 0 := by simp [bayesRisk]

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

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

Разделы

Аффилиация

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