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 [avgRisk]

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

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

Разделы

Аффилиация

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