avgRisk_of_isEmpty

Mathlib.Probability.Decision.Risk.Defs

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

English

If 𝓧 is empty, the average risk is 0.

Русский

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

LaTeX

$$$[IsEmpty 𝓧] \\Rightarrow \\text{avgRisk}_ℓ(P, κ, π) = 0$$$

Lean4

@[simp]
theorem avgRisk_of_isEmpty [IsEmpty 𝓧] : avgRisk ℓ P κ π = 0 := by simp [Subsingleton.elim P 0]

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

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

Разделы

Аффилиация

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