Theorems · Inductive type · statistics

ProbabilityTheory.IsArgminEstimator

{Θ : 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

We say that a measurable function f : 𝓧 → 𝓨 is an argmin estimator with respect to the prior π if for (P ∘ₘ π)-almost every x it is of the form x ↦ argmin_y P†π(x)[θ ↦ ℓ θ y].

Defined in

Mathlib.Probability.Decision.BayesEstimator

Cited by

6 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceNonemptyMeasurableSpaceProbabilityTheory.IsFiniteKernelMeasureTheory.IsFiniteMeasure