Theorems · Theorem · statistics

ProbabilityTheory.IsArgminEstimator.avgRisk_eq_lintegral_iInf

∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ}
  [inst : StandardBorelSpace Θ] [inst_1 : Nonempty Θ] {f : 𝓧 → 𝓨} [inst_2 : ProbabilityTheory.IsFiniteKernel P]
  [inst_3 : MeasureTheory.IsFiniteMeasure π] (hf : ProbabilityTheory.IsArgminEstimator ℓ P π f),
  Measurable (Function.uncurry ℓ) →
    ProbabilityTheory.avgRisk ℓ P hf.kernel π =
      ∫⁻ (x : 𝓧), ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂(ProbabilityTheory.posterior P π) x ∂π.bind ⇑P

The risk of an argmin estimator is the risk lower bound ∫⁻ x, ⨅ z, ∫⁻ θ, ℓ θ z ∂(P†π) x ∂(P ∘ₘ π).

Defined in

Mathlib.Probability.Decision.BayesEstimator

Cited by

2 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceNonemptyProbabilityTheory.IsFiniteKernelMeasureTheory.IsFiniteMeasure