Theorems · Theorem · statistics

ProbabilityTheory.avgRisk_eq_lintegral_posterior_prod

∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} [inst : StandardBorelSpace Θ] [inst_1 : Nonempty Θ],
  Measurable (Function.uncurry ℓ) →
    ∀ (P : ProbabilityTheory.Kernel Θ 𝓧) [inst_2 : ProbabilityTheory.IsFiniteKernel P]
      (κ : ProbabilityTheory.Kernel 𝓧 𝓨) [ProbabilityTheory.IsSFiniteKernel κ] (π : MeasureTheory.Measure Θ)
      [inst_4 : MeasureTheory.IsFiniteMeasure π],
      ProbabilityTheory.avgRisk ℓ P κ π =
        ∫⁻ (θy : Θ × 𝓨), ℓ θy.1 θy.2 ∂(π.bind ⇑P).bind ⇑((ProbabilityTheory.posterior P π).prod κ)

The average risk of an estimator κ with respect to a prior π can be expressed as an integral in the following way: R_π(κ) = ((P†π × κ) ∘ P ∘ π)[(θ, y) ↦ ℓ θ y].

Defined in

Mathlib.Probability.Decision.BayesEstimator

Cited by

1 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceNonemptyProbabilityTheory.IsFiniteKernelProbabilityTheory.IsSFiniteKernelMeasureTheory.IsFiniteMeasure