Theorems · Theorem · statistics

ProbabilityTheory.bayesRisk_le_bayesRisk_map

∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓧' : Type u_3} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓧' : MeasurableSpace 𝓧'} {m𝓨 : MeasurableSpace 𝓨} (ℓ : Θ → 𝓨 → ENNReal) (P : ProbabilityTheory.Kernel Θ 𝓧)
  (π : MeasureTheory.Measure Θ) {f : 𝓧 → 𝓧'},
  Measurable f → ProbabilityTheory.bayesRisk ℓ P π ≤ ProbabilityTheory.bayesRisk ℓ (P.map f) π

Data processing inequality for the Bayes risk with respect to a prior: taking the map of the data generating kernel by a function increases the risk.

Defined in

Mathlib.Probability.Decision.Risk.Basic

Cited by

0 results in Mathlib

Foundations

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