minimaxRisk_of_isEmpty' — Mathlib

English

Let the input space 𝓧 be nonempty and the output space 𝓨 be empty. Then for every loss function ℓ and for every transition kernel P, the minimax risk is infinite: minimaxRisk ℓ P = ∞.

Русский

Пусть входное пространство 𝓧 не пусто, а выходное пространство 𝓨 пусто. Тогда для любой функции потерь ℓ и любого переходного ядра P минимакс-риск равен бесконечности: minimaxRisk ℓ P = ∞.

LaTeX

$$$\\minimaxRisk \\ell P = \\infty$$$

Lean4

@[simp]
theorem minimaxRisk_of_isEmpty' [Nonempty 𝓧] [IsEmpty 𝓨] : minimaxRisk ℓ P = ∞ :=
  by
  have : IsEmpty (Subtype (@IsMarkovKernel 𝓧 𝓨 m𝓧 m𝓨)) :=
    by
    simp only [isEmpty_subtype]
    exact fun κ ↦ Subsingleton.elim κ 0 ▸ Kernel.not_isMarkovKernel_zero
  simp [minimaxRisk, iInf_subtype']

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