Risk of an estimator #
An estimation problem is defined by a parameter space Ī, a data generating kernel P : Kernel Ī š§
and a loss function ā : Ī ā šØ ā āā„0ā.
A (randomized) estimator is a kernel Īŗ : Kernel š§ šØ that maps data to estimates of a quantity
of interest that depends on the parameter. Often the quantity of interest is the parameter itself
and šØ = Ī.
The quality of an estimate y when data comes from the distribution with parameter Īø is measured
by the value of the loss function ā Īø y (lower is better).
Main definitions #
The risk is the average loss of the estimator Īŗ on data generated by P with parameter Īø,
equal to ā«ā» y, ā Īø y ā((Īŗ āā P) Īø). We do not introduce a definition for that risk, but we refer
to that integral as risk in lemma names.
avgRisk ā P Īŗ Ļ: the average of the risk of the estimator with respect to the priorĻ : Measure Ī.bayesRisk ā P Ļ: the Bayes risk with respect to the priorĻ, minimum of the average risks over all estimators, that is over all Markov kernelsĪŗ : Kernel š§ šØ.minimaxRisk ā P: minimax risk, infimum over all estimators of the maximum overĪøof the risk.
noncomputable def
ProbabilityTheory.avgRisk
{Ī : Type u_1}
{š§ : Type u_2}
{šØ : Type u_3}
{mĪ : MeasurableSpace Ī}
{mš§ : MeasurableSpace š§}
{mšØ : MeasurableSpace šØ}
(ā : Ī ā šØ ā ENNReal)
(P : Kernel Ī š§)
(Īŗ : Kernel š§ šØ)
(Ļ : MeasureTheory.Measure Ī)
:
The average risk of an estimator Īŗ on an estimation task with loss ā and
data generating kernel P with respect to a prior Ļ.
Equations
Instances For
noncomputable def
ProbabilityTheory.bayesRisk
{Ī : Type u_1}
{š§ : Type u_2}
{šØ : Type u_3}
{mĪ : MeasurableSpace Ī}
{mš§ : MeasurableSpace š§}
[MeasurableSpace šØ]
(ā : Ī ā šØ ā ENNReal)
(P : Kernel Ī š§)
(Ļ : MeasureTheory.Measure Ī)
:
The Bayes risk with respect to a prior Ļ, defined as the infimum of the average risks of all
estimators.
Equations
Instances For
noncomputable def
ProbabilityTheory.minimaxRisk
{Ī : Type u_1}
{š§ : Type u_2}
{šØ : Type u_3}
{mĪ : MeasurableSpace Ī}
{mš§ : MeasurableSpace š§}
[MeasurableSpace šØ]
(ā : Ī ā šØ ā ENNReal)
(P : Kernel Ī š§)
:
The minimax risk, defined as the infimum over estimators of the maximal risk of the estimator.
Equations
Instances For
@[simp]
theorem
ProbabilityTheory.avgRisk_zero_left
{Ī : Type u_1}
{š§ : Type u_2}
{šØ : Type u_3}
{mĪ : MeasurableSpace Ī}
{mš§ : MeasurableSpace š§}
{mšØ : MeasurableSpace šØ}
(ā : Ī ā šØ ā ENNReal)
(Īŗ : Kernel š§ šØ)
(Ļ : MeasureTheory.Measure Ī)
:
@[simp]
theorem
ProbabilityTheory.avgRisk_zero_right
{Ī : Type u_1}
{š§ : Type u_2}
{šØ : Type u_3}
{mĪ : MeasurableSpace Ī}
{mš§ : MeasurableSpace š§}
{mšØ : MeasurableSpace šØ}
(ā : Ī ā šØ ā ENNReal)
(P : Kernel Ī š§)
(Ļ : MeasureTheory.Measure Ī)
:
@[simp]
theorem
ProbabilityTheory.avgRisk_zero_prior
{Ī : Type u_1}
{š§ : Type u_2}
{šØ : Type u_3}
{mĪ : MeasurableSpace Ī}
{mš§ : MeasurableSpace š§}
{mšØ : MeasurableSpace šØ}
(ā : Ī ā šØ ā ENNReal)
(P : Kernel Ī š§)
(Īŗ : Kernel š§ šØ)
:
@[simp]
theorem
ProbabilityTheory.bayesRisk_zero_left
{Ī : Type u_1}
{š§ : Type u_2}
{šØ : Type u_3}
{mĪ : MeasurableSpace Ī}
{mš§ : MeasurableSpace š§}
{mšØ : MeasurableSpace šØ}
[Nonempty šØ]
(ā : Ī ā šØ ā ENNReal)
(Ļ : MeasureTheory.Measure Ī)
:
@[simp]
theorem
ProbabilityTheory.bayesRisk_zero_right
{Ī : Type u_1}
{š§ : Type u_2}
{šØ : Type u_3}
{mĪ : MeasurableSpace Ī}
{mš§ : MeasurableSpace š§}
{mšØ : MeasurableSpace šØ}
[Nonempty šØ]
(ā : Ī ā šØ ā ENNReal)
(P : Kernel Ī š§)
:
@[simp]
theorem
ProbabilityTheory.minimaxRisk_zero
{Ī : Type u_1}
{š§ : Type u_2}
{šØ : Type u_3}
{mĪ : MeasurableSpace Ī}
{mš§ : MeasurableSpace š§}
{mšØ : MeasurableSpace šØ}
[Nonempty šØ]
(ā : Ī ā šØ ā ENNReal)
:
@[simp]
theorem
ProbabilityTheory.avgRisk_of_isEmpty
{Ī : Type u_1}
{š§ : Type u_2}
{šØ : Type u_3}
{mĪ : MeasurableSpace Ī}
{mš§ : MeasurableSpace š§}
{mšØ : MeasurableSpace šØ}
{ā : Ī ā šØ ā ENNReal}
{P : Kernel Ī š§}
{Īŗ : Kernel š§ šØ}
{Ļ : MeasureTheory.Measure Ī}
[IsEmpty š§]
:
@[simp]
theorem
ProbabilityTheory.avgRisk_of_isEmpty'
{Ī : Type u_1}
{š§ : Type u_2}
{šØ : Type u_3}
{mĪ : MeasurableSpace Ī}
{mš§ : MeasurableSpace š§}
{mšØ : MeasurableSpace šØ}
{ā : Ī ā šØ ā ENNReal}
{P : Kernel Ī š§}
{Īŗ : Kernel š§ šØ}
{Ļ : MeasureTheory.Measure Ī}
[IsEmpty šØ]
:
@[simp]
theorem
ProbabilityTheory.avgRisk_of_isEmpty''
{Ī : Type u_1}
{š§ : Type u_2}
{šØ : Type u_3}
{mĪ : MeasurableSpace Ī}
{mš§ : MeasurableSpace š§}
{mšØ : MeasurableSpace šØ}
{ā : Ī ā šØ ā ENNReal}
{P : Kernel Ī š§}
{Īŗ : Kernel š§ šØ}
{Ļ : MeasureTheory.Measure Ī}
[IsEmpty Ī]
:
@[simp]
theorem
ProbabilityTheory.bayesRisk_of_isEmpty
{Ī : Type u_1}
{š§ : Type u_2}
{šØ : Type u_3}
{mĪ : MeasurableSpace Ī}
{mš§ : MeasurableSpace š§}
{mšØ : MeasurableSpace šØ}
{ā : Ī ā šØ ā ENNReal}
{P : Kernel Ī š§}
{Ļ : MeasureTheory.Measure Ī}
[IsEmpty š§]
:
@[simp]
theorem
ProbabilityTheory.bayesRisk_of_isEmpty'
{Ī : Type u_1}
{š§ : Type u_2}
{šØ : Type u_3}
{mĪ : MeasurableSpace Ī}
{mš§ : MeasurableSpace š§}
{mšØ : MeasurableSpace šØ}
{ā : Ī ā šØ ā ENNReal}
{P : Kernel Ī š§}
{Ļ : MeasureTheory.Measure Ī}
[Nonempty š§]
[IsEmpty šØ]
:
@[simp]
theorem
ProbabilityTheory.bayesRisk_of_isEmpty''
{Ī : Type u_1}
{š§ : Type u_2}
{šØ : Type u_3}
{mĪ : MeasurableSpace Ī}
{mš§ : MeasurableSpace š§}
{mšØ : MeasurableSpace šØ}
{ā : Ī ā šØ ā ENNReal}
{P : Kernel Ī š§}
{Ļ : MeasureTheory.Measure Ī}
[IsEmpty Ī]
[Nonempty šØ]
:
@[simp]
theorem
ProbabilityTheory.minimaxRisk_of_isEmpty
{Ī : Type u_1}
{š§ : Type u_2}
{šØ : Type u_3}
{mĪ : MeasurableSpace Ī}
{mš§ : MeasurableSpace š§}
{mšØ : MeasurableSpace šØ}
{ā : Ī ā šØ ā ENNReal}
{P : Kernel Ī š§}
[IsEmpty š§]
:
@[simp]
theorem
ProbabilityTheory.minimaxRisk_of_isEmpty'
{Ī : Type u_1}
{š§ : Type u_2}
{šØ : Type u_3}
{mĪ : MeasurableSpace Ī}
{mš§ : MeasurableSpace š§}
{mšØ : MeasurableSpace šØ}
{ā : Ī ā šØ ā ENNReal}
{P : Kernel Ī š§}
[Nonempty š§]
[IsEmpty šØ]
:
@[simp]
theorem
ProbabilityTheory.minimaxRisk_of_isEmpty''
{Ī : Type u_1}
{š§ : Type u_2}
{šØ : Type u_3}
{mĪ : MeasurableSpace Ī}
{mš§ : MeasurableSpace š§}
{mšØ : MeasurableSpace šØ}
{ā : Ī ā šØ ā ENNReal}
{P : Kernel Ī š§}
[Nonempty šØ]
[IsEmpty Ī]
: