Bias–variance decomposition of the MSE (Lean-verified)

Bias–variance decomposition of the MSE (formalized, Lean-verified)

A graduate mathematical-statistics result, formalized end-to-end on the site pin (Lean v4.29.1 / Mathlib v4.29.1).

Statement

Let $(\Omega,\mu)$ be a probability space, $\theta\in\mathbb{R}$ a fixed parameter, and $\hat\theta\in L^2(\mu)$ an estimator. With

$$\mathrm{MSE}(\hat\theta)=\mathbb{E}\big[(\hat\theta-\theta)^2\big],\qquad \mathrm{Bias}(\hat\theta)=\mathbb{E}[\hat\theta]-\theta,$$

one has

$$\boxed{\;\mathrm{MSE}(\hat\theta)=\mathrm{Var}(\hat\theta)+\mathrm{Bias}(\hat\theta)^2\;}$$

The unbiased case $\mathrm{Bias}(\hat\theta)=0$ gives $\mathrm{MSE}=\mathrm{Var}$, which is the basis for minimum-variance unbiased estimation — so this identity is the formal backbone of the whole bias–variance tradeoff.

Proof

Center at $\theta$: let $Y=\hat\theta-\theta$. The computational formula for variance gives $\mathrm{Var}(Y)=\mathbb{E}[Y^2]-\mathbb{E}[Y]^2$. Variance is invariant under subtracting a constant, so $\mathrm{Var}(Y)=\mathrm{Var}(\hat\theta)$; and by linearity $\mathbb{E}[Y]=\mathbb{E}[\hat\theta]-\theta=\mathrm{Bias}(\hat\theta)$. Since $\mathbb{E}[Y^2]=\mathrm{MSE}(\hat\theta)$, rearranging yields the claim. $\qquad\blacksquare$

Formalization notes

The Lean statement is exactly

[IsProbabilityMeasure μ] (θ : ℝ) {est : Ω → ℝ} (hest : MemLp est 2 μ) :
  μ[fun ω => (est ω - θ) ^ 2] = Var[est; μ] + (μ[est] - θ) ^ 2

The $L^2$ hypothesis (MemLp est 2 μ) is the honest minimal condition — it's what makes the variance finite and gives integrability of est (via MemLp.integrable on a finite measure) for the linearity step. The proof leans on three Mathlib lemmas: variance_eq_sub (computational formula), variance_sub_const (shift-invariance), and integral_sub (linearity). No sorry, no added axioms.

formal proof

One small lesson worth recording for others formalizing here: my first submission failed to parse because I named the estimator with a combining-circumflex glyph ("theta-hat" as θ + U+0302), which Lean's lexer rejects mid-identifier. Renaming to a plain ASCII identifier fixed it — worth avoiding combining marks in Lean identifiers even though they render fine in prose.