Theorem 8.2 — $U_M$ is an $(\epsilon,\delta)$ -approximator for $M \ge \frac12\epsilon^{-2}\ln(2/\delta)r_D^2(A)$

Proved

TraceEstimation.UnitVector.unit_vector_estimator_approximator

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

hoeffdingp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1randomized-numerical-linear-algebratrace-estimation

Let $A \in \mathbb{R}^{n\times n}$ ( $n \ge 1$ ) be symmetric positive semi-definite, let $r_D(A) = n\max_i A_{ii}/\mathrm{trace}(A)$ , and let $0 < \epsilon$ and $0 < \delta < 1$ . If the number of samples $M \ge 1$ satisfies

M \ge \frac{1}{2}\,\epsilon^{-2}\ln(2/\delta)\,r_D^2(A),

then the unit vector estimator $U_M$ is an $(\epsilon,\delta)$ -approximator of $\mathrm{trace}(A)$ :

\Pr\bigl(|U_M - \mathrm{trace}(A)| \le \epsilon\,\mathrm{trace}(A)\bigr) \ge 1-\delta .

The bound depends on $A$ only through $r_D(A)$ , which is small when the diagonal of $A$ is nearly uniform and as large as $n$ when the trace sits on one diagonal entry.

Formalization Note The sentence of Theorem 8.2 names no hypothesis on $A$ ; the section's matrix is that of Definition 3.4 (positive definite), and the proof uses that samples lie in $[0, n\max_i A_{ii}]$ , i.e. $A_{ii} \ge 0$ . The statement is made for positive semi-definite $A$ , the weaker hypothesis. No hypothesis $\mathrm{trace}(A) > 0$ is added: for positive semi-definite $A$ with trace $0$ , $A = 0$ and the claim holds trivially (Lean's $r_D(0) = 0$ ).

Preamble

import Mathlib
import Definitions.Def_TraceEstimation_Shared_IsApproximator
import Definitions.Def_TraceEstimation_UnitVector_unitVectorEstimator
import Definitions.Def_TraceEstimation_UnitVector_rD

Formal statement

namespace TraceEstimation.UnitVector

open MeasureTheory ProbabilityTheory Matrix Real

/-- Theorem 8.2 (Avron–Toledo, p. 8:12): for a symmetric positive semi-definite `n × n` matrix `A`
(`n ≥ 1`), `0 < ε`, `0 < δ < 1` and `M ≥ 1` samples with
`M ≥ (1/2) ε⁻² ln(2/δ) r_D²(A)`, where `r_D(A) = n · max_i A_ii / trace(A)`, the unit vector
estimator `U_M` is an `(ε, δ)`-approximator of `trace(A)`. -/
theorem unit_vector_estimator_approximator {n : ℕ} (hn : 0 < n)
    (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.PosSemidef)
    (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) (hδ1 : δ < 1)
    (M : ℕ) (hM : 0 < M)
    (hMbound : (1 / 2 : ℝ) * ε⁻¹ ^ 2 * Real.log (2 / δ) * rD A ^ 2 ≤ (M : ℝ)) :
    Shared.IsApproximator (indexSampleMeasure n M) (unitVectorEstimator A M) A ε δ := 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, Theorem 8.2

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

Theorem 8.2 — UMU_MUM​ is an (ϵ,δ)(\epsilon,\delta)(ϵ,δ)-approximator for M≥12ϵ−2ln⁡(2/δ)rD2(A)M \ge \frac12\epsilon^{-2}\ln(2/\delta)r_D^2(A)M≥21​ϵ−2ln(2/δ)rD2​(A)

Theorem 8.2 — $U_M$ is an $(\epsilon,\delta)$ -approximator for $M \ge \frac12\epsilon^{-2}\ln(2/\delta)r_D^2(A)$