Lemma 8.1 — $U_1$ is unbiased with $\mathrm{Var}(U_1) = n\sum_i A_{ii}^2 - \mathrm{trace}^2(A)$

Proved

TraceEstimation.UnitVector.unit_vector_estimator_mean_variance

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

p2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1randomized-numerical-linear-algebratrace-estimationvariance

Let $A$ be an $n\times n$ real symmetric matrix with $n \ge 1$ , and let $U_1 = n\, z^TAz$ be the single-sample unit vector estimator, where $z$ is drawn uniformly from $\{e_1,\ldots,e_n\}$ . Then $U_1$ is an unbiased estimator of $\mathrm{trace}(A)$ , and its variance is explicit:

\mathrm{E}(U_1) = \mathrm{trace}(A), \qquad \mathrm{Var}(U_1) = n\sum_{i=1}^{n}A_{ii}^2 - \mathrm{trace}^2(A).

The variance vanishes exactly when all diagonal entries of $A$ are equal, and is large when the diagonal is concentrated on a few entries; this motivates mixing the matrix before sampling.

Formalization Note $U_1$ is unitVectorEstimator A 1 on the sample space Fin 1 → Fin n with the uniform law indexSampleMeasure n 1; the expectation is the Bochner integral and the variance is Mathlib's ProbabilityTheory.variance (the sample space is finite, so both are the genuine moments).

Preamble

import Mathlib
import Definitions.Def_TraceEstimation_UnitVector_unitVectorEstimator

Formal statement

namespace TraceEstimation.UnitVector

open MeasureTheory ProbabilityTheory Matrix

/-- Lemma 8.1 (Avron–Toledo, p. 8:12): for an `n × n` symmetric matrix `A` (`n ≥ 1`), the single
sample unit vector estimator `U_1 = n · zᵀ A z`, with `z` uniform on `{e_1, …, e_n}`, is an
unbiased estimator of `trace(A)`, `E(U_1) = trace(A)`, and
`Var(U_1) = n ∑_{i=1}^n A_ii² - trace²(A)`. -/
theorem unit_vector_estimator_mean_variance {n : ℕ} (hn : 0 < n)
    (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.IsSymm) :
    (∫ k, unitVectorEstimator A 1 k ∂(indexSampleMeasure n 1)) = A.trace ∧
      variance (unitVectorEstimator A 1) (indexSampleMeasure n 1) =
        (n : ℝ) * ∑ i : Fin n, A i i ^ 2 - A.trace ^ 2 := by sorry

end TraceEstimation.UnitVector

Source

Avron and Toledo, Randomized algorithms for estimating the trace of an implicit symmetric positive semi-definite matrix, J. ACM 58(2), Article 8 (2011), p. 8:12, Lemma 8.1

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Lemma 8.1 — U1U_1U1​ is unbiased with Var(U1)=n∑iAii2−trace2(A)\mathrm{Var}(U_1) = n\sum_i A_{ii}^2 - \mathrm{trace}^2(A)Var(U1​)=n∑i​Aii2​−trace2(A)

Lemma 8.1 — $U_1$ is unbiased with $\mathrm{Var}(U_1) = n\sum_i A_{ii}^2 - \mathrm{trace}^2(A)$