Theorems · Theorem · statistics

ProbabilityTheory.avgRisk_fintype

∀ {Θ : Type u_1} {𝓧 : Type u_3} {𝓨 : Type u_5} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {κ : ProbabilityTheory.Kernel 𝓧 𝓨}
  {π : MeasureTheory.Measure Θ} [inst : Fintype Θ] [MeasurableSingletonClass Θ],
  ProbabilityTheory.avgRisk ℓ P κ π = ∑ θ, (∫⁻ (y : 𝓨), ℓ θ y ∂(κ.comp P) θ) * π {θ}

Defined in

Mathlib.Probability.Decision.Risk.Countable

Cited by

1 results in Mathlib

Foundations

Depth 215 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeMeasurableSingletonClass