bayesRisk_of_isEmpty' — Mathlib

English

If the second space is empty, Bayes risk is zero.

Русский

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

LaTeX

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

Lean4

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

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