Theorems · Theorem · statistics

ProbabilityTheory.IsArgminEstimator.property

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

Defined in

Mathlib.Probability.Decision.BayesEstimator

Cited by

1 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceNonemptyMeasurableSpaceProbabilityTheory.IsFiniteKernelMeasureTheory.IsFiniteMeasure