∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓧' : Type u_3} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓧' : MeasurableSpace 𝓧'} {m𝓨 : MeasurableSpace 𝓨} (ℓ : Θ → 𝓨 → ENNReal) (P : ProbabilityTheory.Kernel Θ 𝓧)
  [ProbabilityTheory.IsSFiniteKernel P] (π : MeasureTheory.Measure Θ) (η : ProbabilityTheory.Kernel (Θ × 𝓧) 𝓧')
  [ProbabilityTheory.IsMarkovKernel η],
  ProbabilityTheory.bayesRisk ℓ (P.compProd η) π ≤ ProbabilityTheory.bayesRisk ℓ P π