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.

• 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 Θ) : ENNReal

The average risk of an estimator κ on an estimation task with loss ℓ and data generating kernel P with respect to a prior π.

Equations

• ProbabilityTheory.avgRisk ℓ P κ π = ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(κ.comp P) θ ∂π

noncomputable def ProbabilityTheory.bayesRisk {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} [MeasurableSpace 𝓨] (ℓ : Θ → 𝓨 → ENNReal) (P : Kernel Θ 𝓧) (π : MeasureTheory.Measure Θ) : ENNReal

The Bayes risk with respect to a prior π, defined as the infimum of the average risks of all estimators.

Equations

• ProbabilityTheory.bayesRisk ℓ P π = ⨅ (κ : ProbabilityTheory.Kernel 𝓧 𝓨), ⨅ (_ : ProbabilityTheory.IsMarkovKernel κ), ProbabilityTheory.avgRisk ℓ P κ π

noncomputable def ProbabilityTheory.minimaxRisk {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} [MeasurableSpace 𝓨] (ℓ : Θ → 𝓨 → ENNReal) (P : Kernel Θ 𝓧) : ENNReal

The minimax risk, defined as the infimum over estimators of the maximal risk of the estimator.

Equations

• ProbabilityTheory.minimaxRisk ℓ P = ⨅ (κ : ProbabilityTheory.Kernel 𝓧 𝓨), ⨅ (_ : ProbabilityTheory.IsMarkovKernel κ), ⨆ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(κ.comp P) θ

@[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 Θ) : avgRisk ℓ 0 κ π = 0

@[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 Θ) : avgRisk ℓ P 0 π = 0

@[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 𝓧 𝓨) : avgRisk ℓ P κ 0 = 0

@[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 Θ) : bayesRisk ℓ 0 π = 0

@[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 Θ 𝓧) : bayesRisk ℓ P 0 = 0

@[simp]

theorem ProbabilityTheory.minimaxRisk_zero {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} [Nonempty 𝓨] (ℓ : Θ → 𝓨 → ENNReal) : minimaxRisk ℓ 0 = 0

@[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 𝓧] : avgRisk ℓ P κ π = 0

@[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 𝓨] : avgRisk ℓ P κ π = 0

@[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 Θ] : avgRisk ℓ P κ π = 0

@[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 𝓧] : bayesRisk ℓ P π = 0

@[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 𝓨] : bayesRisk ℓ P π = ⊤

@[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 𝓨] : bayesRisk ℓ P π = 0

@[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 𝓧] : minimaxRisk ℓ P = 0

@[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 𝓨] : minimaxRisk ℓ P = ⊤

@[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 Θ] : minimaxRisk ℓ P = 0