The Riesz projector of a Hermitian matrix #

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #158 (out of ~~#88~~, the first brick of Kato's adiabatic theorem).

For a Hermitian H : Matrix (Fin N) (Fin N) ℂ, a centre c and a radius r ≥ 0 such that no eigenvalue of H lies on the circle |z − c| = r, the Riesz projector

rieszProj hH c r = (2πi)⁻¹ ∮_{|z−c|=r} (z·1 − H)⁻¹ dz

is the orthogonal projection onto the span of the eigenvectors whose eigenvalue lies inside the disc. Mathlib has the continuous functional calculus for a self-adjoint element, but no projector of an isolated part of the spectrum written as a contour integral — and it is the integral form that the adiabatic theorem differentiates along a path (#159).

conjD hH d = U diag(d) U† — the conjugation of a diagonal by the eigenvector unitary U of spectral_theorem; every operator in the file has this form, and the form is closed under the algebra operations with the diagonals composing pointwise (conjD_mul_conjD, conjD_smul, conjD_sub, conjD_conjTranspose, rank_conjD, conjD_mulVec_eigenvectorBasis); eq_conjD is the spectral theorem as H = conjD eigC, and eigenProj j = conjD (Pi.single j 1) is the eigenprojection of the j-th eigenvector (conjD_eq_sum);
smul_one_sub_eq_conjD, ★ inv_smul_one_sub_eq_conjD — the resolvent in the eigenbasis: off the spectrum, (z·1 − H)⁻¹ = U diag((z − μⱼ)⁻¹) U†, equivalently ∑ⱼ (z − μⱼ)⁻¹ • eigenProj j (inv_smul_one_sub_eq_sum);
circleIntegral_sub_inv_eq_ite — the Cauchy evaluation: ∮ (z − μ)⁻¹ dz is 2πi if μ is inside the disc and 0 if outside (Cauchy's integral formula on one side, Cauchy's theorem on the other);
★★ rieszProj_eq_sum / ★★ rieszProj_eq_conjD — the Riesz projector is the spectral projection: ∑ⱼ discInd j • eigenProj j = conjD discInd, discInd the indicator 𝟙_{|μⱼ−c|<r} of the disc on the eigenvalues;
the corollaries: rieszProj_mul_self (idempotent), rieszProj_isHermitian, rieszProj_mul_comm (H P = P H), rank_rieszProj (the number of eigenvalues in the disc), ★ mul_rieszProj_eq_smul — when the disc isolates one eigenvalue λ, H P = λ • P; rieszProj_mulVec_eigenvectorBasis — on the eigenbasis it keeps or kills each vector.

Honest scope #

Finite dimensions, Fin N, and 𝕜 = ℂ, as the adiabatic theorem needs; the matrix norm is the L2Operator scope's, under which Matrix is a complete normed ℂ-algebra and the circle integral is a Bochner integral.
The eigenvalues are Mathlib's hH.eigenvalues, so "inside the disc" is a condition on those reals; nothing about multiplicities is assumed.

References: T. Kato, Perturbation Theory for Linear Operators, I §5.3 (the Riesz projector); Mathlib/Analysis/Matrix/Spectrum.lean (spectral_theorem, eigenvectorUnitary), Mathlib/MeasureTheory/Integral/CircleIntegral.lean (integral_sub_inv_of_mem_ball, integral_smul_const, integral_fun_sum), Mathlib/Analysis/Complex/CauchyIntegral.lean; specs/BACKLOG.md #158, ~~#88~~.

The Riesz projector of a Hermitian matrix #

Honest scope #

The eigenbasis and the conjugation d ↦ U diag(d) U† #

The resolvent in the eigenbasis #

The Cauchy evaluation #

The Riesz projector #

The corollaries #

The eigenbasis and the conjugation `d ↦ U diag(d) U†` #