∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} (ℓ : Θ → 𝓨 → ENNReal) (μ : MeasureTheory.Measure 𝓧) (κ : ProbabilityTheory.Kernel 𝓧 𝓨)
  (π : MeasureTheory.Measure Θ),
  ProbabilityTheory.avgRisk ℓ (ProbabilityTheory.Kernel.const Θ μ) κ π = ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂μ.bind ⇑κ ∂π