Theorems · Inductive type · statistics

ProbabilityTheory.HasArgminEstimator

{Θ : Type u_1} →
  {𝓧 : Type u_2} →
    {mΘ : MeasurableSpace Θ} →
      {m𝓧 : MeasurableSpace 𝓧} →
        [StandardBorelSpace Θ] →
          [Nonempty Θ] →
            {𝓨 : Type u_4} →
              [MeasurableSpace 𝓨] →
                (Θ → 𝓨 → ENNReal) →
                  (P : ProbabilityTheory.Kernel Θ 𝓧) →
                    [ProbabilityTheory.IsFiniteKernel P] →
                      (π : MeasureTheory.Measure Θ) → [MeasureTheory.IsFiniteMeasure π] → Prop

The estimation problem admits an argmin estimator with respect to the prior π. That is, we can choose the argmin of the posterior expected loss in a measurable way.

Defined in

Mathlib.Probability.Decision.BayesEstimator

Cited by

3 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceNonemptyMeasurableSpaceProbabilityTheory.IsFiniteKernelMeasureTheory.IsFiniteMeasure