avgRisk_of_isEmpty'

Mathlib.Probability.Decision.Risk.Defs

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

English

If the target space of the second parameter 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 κ 0]

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

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

Разделы

Аффилиация

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