minimaxRisk_of_isEmpty

Mathlib.Probability.Decision.Risk.Defs

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

English

If 𝓧 is empty, the minimax risk is 0.

Русский

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

LaTeX

$$$[IsEmpty 𝓧] \\Rightarrow \\text{minimaxRisk}_ℓ(P) = 0$$$

Lean4

@[simp]
theorem minimaxRisk_of_isEmpty [IsEmpty 𝓧] : minimaxRisk ℓ P = 0 := by simp [minimaxRisk, Subsingleton.elim P 0]

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

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

Разделы

Аффилиация

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