Theorems · Theorem · statistics

ProbabilityTheory.avgRisk_le_mul

∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} (P : ProbabilityTheory.Kernel Θ 𝓧) [ProbabilityTheory.IsMarkovKernel P]
  (κ : ProbabilityTheory.Kernel 𝓧 𝓨) [ProbabilityTheory.IsMarkovKernel κ] (π : MeasureTheory.Measure Θ)
  [MeasureTheory.IsProbabilityMeasure π] {C : NNReal},
  (∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C) → ProbabilityTheory.avgRisk ℓ P κ π ≤ ↑C

Defined in

Mathlib.Probability.Decision.Risk.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

ProbabilityTheory.IsMarkovKernelProbabilityTheory.IsMarkovKernelMeasureTheory.IsProbabilityMeasure