bayesRisk_zero_left

Mathlib.Probability.Decision.Risk.Defs

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

← MathLib Explorer

English

If 𝓧 is empty, Bayes risk is zero.

Русский

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

LaTeX

$$$\\text{If } 𝓧 = \\varnothing,\\; bayesRisk_ℓ(P, π) = 0$$$

Lean4

@[simp]
theorem bayesRisk_zero_left [Nonempty 𝓨] (ℓ : Θ → 𝓨 → ℝ≥0∞) (π : Measure Θ) : bayesRisk ℓ (0 : Kernel Θ 𝓧) π = 0 := by
  simp [bayesRisk, iInf_subtype']

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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