bayesRisk_of_isEmpty''

Mathlib.Probability.Decision.Risk.Defs

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

English

If Θ is empty and 𝓨 is nonempty, Bayes risk is 0.

Русский

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

LaTeX

$$$[IsEmpty Θ] \\land [Nonempty 𝓨] \\Rightarrow bayesRisk_ℓ(P, π) = 0$$$

Lean4

@[simp]
theorem bayesRisk_of_isEmpty'' [IsEmpty Θ] [Nonempty 𝓨] : bayesRisk ℓ P π = 0 := by simp [bayesRisk, iInf_subtype']

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

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

Разделы

Аффилиация

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