Theorems · Definition · statistics

ProbabilityTheory.avgRisk

{Θ : Type u_1} →
  {𝓧 : Type u_2} →
    {𝓨 : Type u_3} →
      {mΘ : MeasurableSpace Θ} →
        {m𝓧 : MeasurableSpace 𝓧} →
          {m𝓨 : MeasurableSpace 𝓨} →
            (Θ → 𝓨 → ENNReal) →
              ProbabilityTheory.Kernel Θ 𝓧 → ProbabilityTheory.Kernel 𝓧 𝓨 → MeasureTheory.Measure Θ → ENNReal

The average risk of an estimator κ on an estimation task with loss ℓ and data generating kernel P with respect to a prior π.

Defined in

Mathlib.Probability.Decision.Risk.Defs

Cited by

25 results in Mathlib

Foundations

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