Bayes estimators for squared and absolute loss

9 fully proved

Posterior means for squared loss

DefinitionSquared loss#✓fully proved

The squared loss of predicting \(y \in \mathbb{R}\) when the true value is \(\theta \in \mathbb{R}\) is \((\theta - y)^2\), regarded as an element of \([0, \infty]\).

noncomputable def sqLoss (θ y : ℝ) : ℝ≥0∞ :=
  ENNReal.ofReal ((θ - y) ^ 2)

Used by 2

Used byThe posterior mean is a Bayes estimator for squared loss · The mean minimizes the expected squared loss

TheoremThe mean minimizes the expected squared loss#✓fully proved

Let \(\nu\) be a probability measure on \(\mathbb{R}\) with mean \(m = \int t \, d\nu(t)\) (taken to be \(0\) when \(\nu\) has no finite first moment). Then for every \(y \in \mathbb{R}\),

\[\int (\theta - m)^2 \, d\nu(\theta) \le \int (\theta - y)^2 \, d\nu(\theta),\]

where both integrals are taken in \([0, \infty]\).

When the right side is infinite the inequality is trivial; otherwise \(\nu\) has a second moment and the variance decomposition applies.

theorem lintegral_sqLoss_integral_le (ν : Measure ℝ) [IsProbabilityMeasure ν] (y : ℝ) :
    ∫⁻ θ, sqLoss θ (∫ t, t ∂ν) ∂ν ≤ ∫⁻ θ, sqLoss θ y ∂ν

Uses 4 · Used by 1

Statement usesSquared loss

Proof usesA finite second moment makes the squared error integrable · Mean squared error · Mean squared error as variance plus squared mean deviation

Used byThe posterior mean is a Bayes estimator for squared loss

DefinitionPosterior mean#✓fully proved

Let \(P\) be a finite kernel from \(\mathbb{R}\) to a measurable space \(\mathcal{X}\), let \(\pi\) be a finite measure on \(\mathbb{R}\), and write \(P^\dagger\pi\) for the posterior kernel from \(\mathcal{X}\) to \(\mathbb{R}\). The posterior mean is the function on \(\mathcal{X}\) sending \(x\) to \(\int \theta \, d(P^\dagger\pi)(x)(\theta)\), the mean of the posterior distribution given the observation \(x\) (taken to be \(0\) when that distribution has no finite first moment).

noncomputable def posteriorMean (P : Kernel ℝ 𝓧) [IsFiniteKernel P] (π : Measure ℝ)
    [IsFiniteMeasure π] (x : 𝓧) : ℝ :=
  ∫ θ, θ ∂(P†π) x

Used by 2

Used byThe posterior mean is a Bayes estimator for squared loss · Measurable versions of the posterior mean

StructureMeasurable versions of the posterior mean#✓fully proved

Let \(P\) be a finite kernel from \(\mathbb{R}\) to a measurable space \(\mathcal{X}\), sending \(\theta\) to the measure \(P_\theta\), let \(\pi\) be a finite measure on \(\mathbb{R}\), and write \(P^\dagger\pi\) for the posterior kernel from \(\mathcal{X}\) to \(\mathbb{R}\). A function \(f : \mathcal{X} \to \mathbb{R}\) is a measurable version of the posterior mean if \(f\) is measurable and \(f(x) = \int \theta \, d(P^\dagger\pi)(x)(\theta)\) (the posterior mean, taken to be \(0\) when the posterior has no finite first moment) for almost every \(x\) with respect to the marginal distribution of the data, the measure \(A \mapsto \int P_\theta(A) \, d\pi(\theta)\) on \(\mathcal{X}\).

structure IsPosteriorMean (P : Kernel ℝ 𝓧) [IsFiniteKernel P] (π : Measure ℝ) [IsFiniteMeasure π]
    (f : 𝓧 → ℝ) : Prop where
  measurable : Measurable f
  ae_eq : ∀ᵐ x ∂(P ∘ₘ π), f x = posteriorMean P π x

Uses 1 · Used by 1

Statement usesPosterior mean

Used byThe posterior mean is a Bayes estimator for squared loss

TheoremThe posterior mean is a Bayes estimator for squared loss#✓fully proved

Let \(P\) be a finite kernel from \(\mathbb{R}\) to a measurable space \(\mathcal{X}\), sending a parameter \(\theta\) to the measure \(P_\theta\) on \(\mathcal{X}\), let \(\pi\) be a finite prior measure on \(\mathbb{R}\), and let \(f : \mathcal{X} \to \mathbb{R}\) be a measurable version of the posterior mean. Then the deterministic estimator \(x \mapsto f(x)\) is a Bayes estimator for the squared loss \(\ell(\theta, y) = (\theta - y)^2\): its average risk \(\int \int (\theta - f(x))^2 \, dP_\theta(x) \, d\pi(\theta)\) equals the Bayes risk, the infimum of the average risks of all Markov kernels from \(\mathcal{X}\) to \(\mathbb{R}\), where risks take values in \([0, \infty]\).

theorem IsPosteriorMean.isBayesEstimator (hf : IsPosteriorMean P π f) :
    IsBayesEstimator sqLoss P (Kernel.deterministic f hf.measurable) π

Uses 4

Statement usesMeasurable versions of the posterior mean · Squared loss

Proof usesThe mean minimizes the expected squared loss · Posterior mean

Medians for absolute loss

DefinitionAbsolute loss#✓fully proved

The absolute loss of predicting \(y \in \mathbb{R}\) when the true value is \(\theta \in \mathbb{R}\) is \(|\theta - y|\), regarded as an element of \([0, \infty]\).

noncomputable def absLoss (θ y : ℝ) : ℝ≥0∞ :=
  ENNReal.ofReal |θ - y|

Used by 2

Used byA posterior median is a Bayes estimator for absolute loss · The expected absolute loss is minimized at every median

TheoremThe expected absolute loss is minimized at every median#✓fully proved

Let \(\nu\) be a probability measure on \(\mathbb{R}\) and let \(m\) be a median of \(\nu\). Then for every \(y \in \mathbb{R}\),

\[\int |\theta - m| \, d\nu(\theta) \le \int |\theta - y| \, d\nu(\theta),\]

where both integrals are taken in \([0, \infty]\).

theorem lintegral_absLoss_le_of_isMedian (ν : Measure ℝ) [IsProbabilityMeasure ν] {m : ℝ}
    (hm : IsMedian ν m) (y : ℝ) : ∫⁻ θ, absLoss θ m ∂ν ≤ ∫⁻ θ, absLoss θ y ∂ν

Uses 4 · Used by 1

Statement usesAbsolute loss · Median of a measure on the real line

Proof usesAbsolute deviations are integrable exactly when the mean exists · A median minimizes the expected absolute loss

Used byA posterior median is a Bayes estimator for absolute loss

StructureMeasurable choices of posterior medians#✓fully proved

Let \(P\) be a finite kernel from \(\mathbb{R}\) to a measurable space \(\mathcal{X}\), sending \(\theta\) to the measure \(P_\theta\), let \(\pi\) be a finite measure on \(\mathbb{R}\), and write \(P^\dagger\pi\) for the posterior kernel from \(\mathcal{X}\) to \(\mathbb{R}\). A function \(f : \mathcal{X} \to \mathbb{R}\) is a measurable choice of posterior medians if \(f\) is measurable and, for almost every \(x\) with respect to the marginal distribution \(A \mapsto \int P_\theta(A) \, d\pi(\theta)\) of the data, \(f(x)\) is a median of the posterior distribution \((P^\dagger\pi)(x)\).

structure IsPosteriorMedian (P : Kernel ℝ 𝓧) [IsFiniteKernel P] (π : Measure ℝ)
    [IsFiniteMeasure π] (f : 𝓧 → ℝ) : Prop where
  measurable : Measurable f
  ae_isMedian : ∀ᵐ x ∂(P ∘ₘ π), IsMedian ((P†π) x) (f x)

Uses 1 · Used by 1

Statement usesMedian of a measure on the real line

Used byA posterior median is a Bayes estimator for absolute loss

TheoremA posterior median is a Bayes estimator for absolute loss#✓fully proved

Let \(P\) be a finite kernel from \(\mathbb{R}\) to a measurable space \(\mathcal{X}\), sending a parameter \(\theta\) to the measure \(P_\theta\) on \(\mathcal{X}\), let \(\pi\) be a finite prior measure on \(\mathbb{R}\), and let \(f : \mathcal{X} \to \mathbb{R}\) be a measurable choice of posterior medians. Then the deterministic estimator \(x \mapsto f(x)\) is a Bayes estimator for the absolute loss \(\ell(\theta, y) = |\theta - y|\): its average risk \(\int \int |\theta - f(x)| \, dP_\theta(x) \, d\pi(\theta)\) equals the Bayes risk, the infimum of the average risks of all Markov kernels from \(\mathcal{X}\) to \(\mathbb{R}\), where risks take values in \([0, \infty]\).

theorem IsPosteriorMedian.isBayesEstimator (hf : IsPosteriorMedian P π f) :
    IsBayesEstimator absLoss P (Kernel.deterministic f hf.measurable) π

Uses 4

Statement usesMeasurable choices of posterior medians · Absolute loss

Proof usesThe expected absolute loss is minimized at every median · Median of a measure on the real line

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.