minimaxRisk_zero

Mathlib.Probability.Decision.Risk.Defs

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

English

The minimax risk of any loss function against the zero kernel is 0.

Русский

Минимакс-рисок нулевого ядра равен 0.

LaTeX

$$$\\text{minimaxRisk}_ℓ(0) = 0$$$

Lean4

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

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

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

Разделы

Аффилиация

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