Markov chain Monte Carlo asymptotic variance for a stationary Markov chain and is
whenever the limit and series exist. If a reversible Markov chain has positive spectral gap , then the spectral theorem for normal operators on a separable Hilbert space gives
Let and let be its orthogonal projection. For , define
Because is unitary,
The displayed finite Hermitian matrix uses only finitely many matrix entries of , and its least eigenvalue can be approximated by an arithmetic algorithm in the SCI hierarchy.
As increases densely,
A unitary operator is normal, so the spectral theorem for normal operators on a separable Hilbert space identifies the limit as
The functions are continuous and decrease to a continuous function on the compact unit circle. The Dini theorem therefore gives uniform convergence there.
Take successively finer rational meshes around . From the finitely computed values of , retain the mesh minima in the comparison neighborhoods whose radii are ; equivalently, use the standard local-minimum construction for a decreasing approximation to a distance function. Call the resulting finite set . Uniform convergence and the shrinking mesh imply
in Hausdorff distance. Every operation at stage is finite and arithmetic, so is the required one-limit sequence.
There is no finite-stage certificate that the whole output has the correct Hausdorff error: the convergence of has no uniform computable rate over all unitary operators, and unseen matrix entries can still reveal a missing spectral component. A small computed residual can certify that an individual output point lies near the spectrum, but it cannot verify that covers all of . Thus the full finite-stage output is not verifiable without additional information.
A projection-valued measure on the Borel sets of is a map into the orthogonal projections on a separable Hilbert space such that
and for pairwise disjoint ,
for every , with convergence in norm.
The spectral theorem for normal operators on a separable Hilbert space states that a bounded normal operator has a unique projection-valued measure supported on for which
More generally, the Borel functional calculus for a normal operator is
For , the scalar spectral measures are
If is self-adjoint, its spectrum and hence the support of lie in . Moreover,
so is a positive measure, and
The paper prints total mass ; with the standard definition it is , so the unsquared norm is a typographical error.
Let and be the projection-valued measures of and . Using the projection , define
The scalar spectral measures converge weakly when
for every bounded continuous function and every . By the spectral theorem for normal operators on a separable Hilbert space, this is equivalent to
The assumed moment identities say precisely that this convergence holds for every monomial . It follows by linearity for every polynomial. For , the identity gives
so Markov inequality makes the positive measures tight. Higher even moments similarly control the tails of any fixed polynomial.
Given a bounded continuous and , choose so that the measure tails are uniformly small. The Weierstrass approximation theorem supplies a polynomial with
Moment convergence handles ; tightness and a sufficiently high even moment handle the two tails. Hence . The polarization identity then gives the same conclusion for . This proves weak convergence of scalar spectral measures.
The assertion fails if only is assumed. Let , let , take , and let
The reversal matrices are self-adjoint unitaries. For fixed ,
because the finite head of one vector is paired with the vanishing tail of the other. Thus the condition holds. However, , so
in general. Taking shows that the spectral measures do not converge weakly.
The spectral theorem for normal operators on a separable Hilbert space states that a normal operator has a unique projection-valued measure on its spectrum such that
For bounded this integral acts on all of . For an unbounded normal operator,
Equivalently, is unitarily equivalent to multiplication by a measurable function on a direct sum of spaces.
Positive square root of an operator Created 2026-09-24 Updated 2026-10-05