Bayes estimator

Let Θ be a parameter space, 𝓧 a data space, 𝓨 a prediction space, P : Kernel Θ 𝓧 a data generating kernel, π a prior on the parameter space, and ℓ : Θ → 𝓨 → ℝ≥0∞ a loss function.

An estimator (a Kernel 𝓧 𝓨) is said to be a Bayes estimator if it attains the Bayes risk for the estimation problem. It can be written as a measurable function x ↦ argmin_y P†π(x)[θ ↦ ℓ θ y] for (P ∘ₘ π)-almost every x, where P†π is the posterior kernel, whenever we can select the argmin in a measurable way.

Main definitions

• IsBayesEstimator: an estimator is a Bayes estimator if it attains the Bayes risk for the prior.
• IsArgminEstimator: a measurable function f : 𝓧 → 𝓨 is an argmin estimator if for (P ∘ₘ π)-almost every x the value f x belongs to argmin_y P†π(x)[θ ↦ ℓ θ y].
• HasArgminEstimator: the estimation problem admits an argmin estimator. That is, we can choose the argmin of the posterior expected loss in a measurable way.

Main statements

• lintegral_iInf_posterior_le_bayesRisk: the Bayes risk with respect to a prior is bounded from below by the integral over the data (with distribution P ∘ₘ π) of the infimum over the possible predictions y of the posterior loss ∫⁻ θ, ℓ θ y ∂((P†π) x): ∫⁻ x, ⨅ y : 𝓨, ∫⁻ θ, ℓ θ y ∂((P†π) x) ∂(P ∘ₘ π) ≤ bayesRisk ℓ P π
• IsArgminEstimator.isBayesEstimator: an argmin Bayes estimator is a Bayes estimator. That is, it minimizes the Bayesian risk.
• bayesRisk_eq_of_hasArgminEstimator: if the estimation problem admits an argmin estimator, then the Bayesian risk attains the risk lower bound ∫⁻ x, ⨅ y, ∫⁻ θ, ℓ θ y ∂(P†π) x ∂(P ∘ₘ π).

TODO

Once Mathlib has measurable selection theorems, we will be able to prove HasArgminEstimator under general conditions on the measurable spaces 𝓧 and/or 𝓨.

theorem ProbabilityTheory.avgRisk_eq_lintegral_posterior_prod {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} [StandardBorelSpace Θ] [Nonempty Θ] (hl : Measurable (Function.uncurry ℓ)) (P : Kernel Θ 𝓧) [IsFiniteKernel P] (κ : Kernel 𝓧 𝓨) [IsSFiniteKernel κ] (π : MeasureTheory.Measure Θ) [MeasureTheory.IsFiniteMeasure π] : avgRisk ℓ P κ π = ∫⁻ (θy : Θ × 𝓨), ℓ θy.1 θy.2 ∂(π.bind ⇑P).bind ⇑((posterior P π).prod κ)

The average risk of an estimator κ with respect to a prior π can be expressed as an integral in the following way: R_π(κ) = ((P†π × κ) ∘ P ∘ π)[(θ, y) ↦ ℓ θ y].

theorem ProbabilityTheory.avgRisk_eq_lintegral_lintegral_lintegral {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} [StandardBorelSpace Θ] [Nonempty Θ] (hl : Measurable (Function.uncurry ℓ)) (P : Kernel Θ 𝓧) [IsFiniteKernel P] (κ : Kernel 𝓧 𝓨) [IsSFiniteKernel κ] (π : MeasureTheory.Measure Θ) [MeasureTheory.IsFiniteMeasure π] : avgRisk ℓ P κ π = ∫⁻ (x : 𝓧), ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂(posterior P π) x ∂κ x ∂π.bind ⇑P

theorem ProbabilityTheory.lintegral_iInf_posterior_le_avgRisk {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} [StandardBorelSpace Θ] [Nonempty Θ] (hl : Measurable (Function.uncurry ℓ)) (P : Kernel Θ 𝓧) [IsFiniteKernel P] (κ : Kernel 𝓧 𝓨) [IsMarkovKernel κ] (π : MeasureTheory.Measure Θ) [MeasureTheory.IsFiniteMeasure π] : ∫⁻ (x : 𝓧), ⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂(posterior P π) x ∂π.bind ⇑P ≤ avgRisk ℓ P κ π

theorem ProbabilityTheory.lintegral_iInf_posterior_le_bayesRisk {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} [StandardBorelSpace Θ] [Nonempty Θ] (hl : Measurable (Function.uncurry ℓ)) (P : Kernel Θ 𝓧) [IsFiniteKernel P] (π : MeasureTheory.Measure Θ) [MeasureTheory.IsFiniteMeasure π] : ∫⁻ (x : 𝓧), ⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂(posterior P π) x ∂π.bind ⇑P ≤ bayesRisk ℓ P π

def ProbabilityTheory.IsBayesEstimator {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} (ℓ : Θ → 𝓨 → ENNReal) (P : Kernel Θ 𝓧) (κ : Kernel 𝓧 𝓨) (π : MeasureTheory.Measure Θ) : Prop

An estimator is a Bayes estimator for a prior π if it attains the Bayes risk for π.

Equations

• ProbabilityTheory.IsBayesEstimator ℓ P κ π = (ProbabilityTheory.avgRisk ℓ P κ π = ProbabilityTheory.bayesRisk ℓ P π)

structure ProbabilityTheory.IsArgminEstimator {Θ : Type u_1} {𝓧 : Type u_2} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} [StandardBorelSpace Θ] [Nonempty Θ] {𝓨 : Type u_4} [MeasurableSpace 𝓨] (ℓ : Θ → 𝓨 → ENNReal) (P : Kernel Θ 𝓧) [IsFiniteKernel P] (π : MeasureTheory.Measure Θ) [MeasureTheory.IsFiniteMeasure π] (f : 𝓧 → 𝓨) : 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].

• measurable : Measurable f
• property : ∀ᵐ (x : 𝓧) ∂π.bind ⇑P, ∫⁻ (θ : Θ), ℓ θ (f x) ∂(posterior P π) x = ⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂(posterior P π) x

@[reducible, inline]

noncomputable abbrev ProbabilityTheory.IsArgminEstimator.kernel {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ} [StandardBorelSpace Θ] [Nonempty Θ] {f : 𝓧 → 𝓨} [IsFiniteKernel P] [MeasureTheory.IsFiniteMeasure π] (h : IsArgminEstimator ℓ P π f) : Kernel 𝓧 𝓨

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

Equations

• h.kernel = ProbabilityTheory.Kernel.deterministic f ⋯

theorem ProbabilityTheory.IsArgminEstimator.avgRisk_eq_lintegral_iInf {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ} [StandardBorelSpace Θ] [Nonempty Θ] {f : 𝓧 → 𝓨} [IsFiniteKernel P] [MeasureTheory.IsFiniteMeasure π] (hf : IsArgminEstimator ℓ P π f) (hl : Measurable (Function.uncurry ℓ)) : avgRisk ℓ P hf.kernel π = ∫⁻ (x : 𝓧), ⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂(posterior P π) x ∂π.bind ⇑P

The risk of an argmin estimator is the risk lower bound ∫⁻ x, ⨅ z, ∫⁻ θ, ℓ θ z ∂(P†π) x ∂(P ∘ₘ π).

theorem ProbabilityTheory.IsArgminEstimator.isBayesEstimator {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ} [StandardBorelSpace Θ] [Nonempty Θ] {f : 𝓧 → 𝓨} [IsFiniteKernel P] [MeasureTheory.IsFiniteMeasure π] (hf : IsArgminEstimator ℓ P π f) (hl : Measurable (Function.uncurry ℓ)) : IsBayesEstimator ℓ P hf.kernel π

An argmin estimator is a Bayes estimator: that is, it minimizes the Bayesian risk.

structure ProbabilityTheory.HasArgminEstimator {Θ : Type u_1} {𝓧 : Type u_2} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} [StandardBorelSpace Θ] [Nonempty Θ] {𝓨 : Type u_4} [MeasurableSpace 𝓨] (ℓ : Θ → 𝓨 → ENNReal) (P : Kernel Θ 𝓧) [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.

• exists_isArgminEstimator : ∃ (f : 𝓧 → 𝓨), IsArgminEstimator ℓ P π f

noncomputable def ProbabilityTheory.HasArgminEstimator.argminEstimator {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ} [StandardBorelSpace Θ] [Nonempty Θ] [IsFiniteKernel P] [MeasureTheory.IsFiniteMeasure π] (h : HasArgminEstimator ℓ P π) : 𝓧 → 𝓨

An estimator for an estimation problem that for (P ∘ₘ π)-almost every x is of the form x ↦ argmin_y P†π(x)[θ ↦ ℓ θ y].

Equations

• h.argminEstimator = ⋯.choose

theorem ProbabilityTheory.HasArgminEstimator.isArgminEstimator_argminEstimator {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ} [StandardBorelSpace Θ] [Nonempty Θ] [IsFiniteKernel P] [MeasureTheory.IsFiniteMeasure π] (h : HasArgminEstimator ℓ P π) : IsArgminEstimator ℓ P π h.argminEstimator

theorem ProbabilityTheory.HasArgminEstimator.bayesRisk_eq {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ} [StandardBorelSpace Θ] [Nonempty Θ] [IsFiniteKernel P] [MeasureTheory.IsFiniteMeasure π] (hl : Measurable (Function.uncurry ℓ)) (h : HasArgminEstimator ℓ P π) : bayesRisk ℓ P π = ∫⁻ (x : 𝓧), ⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂(posterior P π) x ∂π.bind ⇑P

If the estimation problem admits an argmin estimator, then the Bayesian risk attains the risk lower bound ∫⁻ x, ⨅ y, ∫⁻ θ, ℓ θ y ∂((P†π) x) ∂(P ∘ₘ π).