Theorems · Definition · statistics

ProbabilityTheory.IsArgminEstimator.kernel

{Θ : 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 π] →
                            ProbabilityTheory.IsArgminEstimator ℓ P π f → ProbabilityTheory.Kernel 𝓧 𝓨

Given an argmin estimator f, we can define a deterministic kernel.

Defined in

Mathlib.Probability.Decision.BayesEstimator

Cited by

2 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceNonemptyProbabilityTheory.IsFiniteKernelMeasureTheory.IsFiniteMeasure