Resolvents of Hermitian matrices

For a square matrix A and a scalar z outside its spectrum, the resolvent of A at z is the matrix R_A(z) = (A - z • 1)⁻¹. This is the sign convention of MeasureTheory.resolventTransform, whose kernel at a point x is (x - z)⁻¹, so that the normalized trace of R_A(z) is the resolvent transform of the empirical spectral measure of A. Mathlib's resolvent A z is (z • 1 - A)⁻¹, the negative of R_A(z).

For a Hermitian matrix A with eigenvector unitary U and eigenvalues λ, the resolvent is diagonal in the eigenbasis: R_A(z) = U * diagonal (fun j ↦ (λ j - z)⁻¹) * Uᴴ. This file reads off its entries, its trace and its Euclidean operator norm. For a non-real z it proves the resolvent bound ‖R_A(z)‖ ≤ |Im z|⁻¹ and the Ward identity ∑ j, ‖R_A(z) i j‖ ^ 2 = Im (R_A(z) i i) / Im z, whose consequence is that the diagonal entries of the resolvent lie in the upper half-plane when z does. These deterministic facts drive the resolvent method for global spectral laws of random matrices: the bound keeps the resolvent and its entries under control in the upper half-plane, and the Ward identity converts sums of squared entries back into diagonal entries. The resolvent identities specialize Mathlib's Matrix.inv_sub_inv.

Main results

• Matrix.IsHermitian.inv_sub_smul_one_eq_conjStarAlgAut_diagonal — the resolvent of a Hermitian matrix is conjugate, by the eigenvector unitary, to diagonal fun j ↦ (λ j - z)⁻¹;
• Matrix.IsHermitian.inv_sub_smul_one_apply — the entrywise spectral expansion of the resolvent;
• Matrix.IsHermitian.trace_inv_sub_smul_one — its trace is ∑ j, (λ j - z)⁻¹;
• Matrix.IsHermitian.l2_opNorm_inv_sub_smul_one — its Euclidean operator norm is the largest of the moduli |λ j - z|⁻¹;
• Matrix.IsHermitian.conjTranspose_inv_sub_smul_one — the conjugate transpose of the resolvent at z is the resolvent at conj z;
• Matrix.IsHermitian.notMem_spectrum_of_im_ne_zero — a non-real scalar lies outside the spectrum of a Hermitian matrix;
• Matrix.IsHermitian.l2_opNorm_inv_sub_smul_one_le — the resolvent bound ‖(A - z • 1)⁻¹‖ ≤ |Im z|⁻¹;
• Matrix.IsHermitian.l2_opNorm_one_add_sub_conj_smul_inv_sub_smul_one_le — the Cayley expression has norm at most one;
• Matrix.IsHermitian.l2_opNorm_inv_sub_smul_one_sub_le — the difference of two resolvents at the same parameter has norm at most |Im z|⁻¹;
• Matrix.IsHermitian.im_inv_sub_smul_one_apply_self and Matrix.IsHermitian.sum_norm_inv_sub_smul_one_apply_sq — the Ward identity;
• Matrix.IsHermitian.im_inv_sub_smul_one_apply_self_pos — 0 < Im (R_A(z) i i) when 0 < Im z.

References

• G. W. Anderson, A. Guionnet, O. Zeitouni, An Introduction to Random Matrices, Cambridge University Press (2010), §2.4.
• T. Tao, Topics in Random Matrix Theory, American Mathematical Society (2012), §2.4.3.
• L. Erdős, H.-T. Yau, A Dynamical Approach to Random Matrix Theory, Courant Lecture Notes 28, AMS (2017), Lemma 8.3 (the Ward identity).

theorem Matrix.inv_sub_smul_one_sub_inv_sub_smul_one {α : Type u_1} {n : Type u_2} [CommRing α] [Fintype n] [DecidableEq n] {A B : Matrix n n α} {z w : α} (h : IsUnit (A - z • 1) ↔ IsUnit (B - w • 1)) : (A - z • 1)⁻¹ - (B - w • 1)⁻¹ = (A - z • 1)⁻¹ * (B - A + (z - w) • 1) * (B - w • 1)⁻¹

The first resolvent identity for matrices with simultaneously invertible resolvents.

theorem Matrix.inv_sub_smul_one_sub_inv_sub_smul_one_eq {α : Type u_1} {n : Type u_2} [CommRing α] [Fintype n] [DecidableEq n] {A : Matrix n n α} {z w : α} (h : IsUnit (A - z • 1) ↔ IsUnit (A - w • 1)) : (A - z • 1)⁻¹ - (A - w • 1)⁻¹ = (z - w) • ((A - z • 1)⁻¹ * (A - w • 1)⁻¹)

The first resolvent identity for a change of spectral parameter.

theorem Matrix.IsHermitian.sub_smul_one_eq_conjStarAlgAut_diagonal {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) (z : 𝕜) : A - z • 1 = ((Unitary.conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary) (diagonal fun (j : n) => ↑(hA.eigenvalues j) - z)

The shifted matrix A - z • 1 of a Hermitian matrix is conjugate, by the eigenvector unitary of A, to the diagonal matrix with entries hA.eigenvalues j - z.

theorem Matrix.IsHermitian.inv_sub_smul_one_eq_conjStarAlgAut_diagonal {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) {z : 𝕜} (hz : z ∉ spectrum 𝕜 A) : (A - z • 1)⁻¹ = ((Unitary.conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary) (diagonal fun (j : n) => (↑(hA.eigenvalues j) - z)⁻¹)

Off the spectrum, the resolvent (A - z • 1)⁻¹ of a Hermitian matrix is conjugate, by the eigenvector unitary of A, to the diagonal matrix with entries (hA.eigenvalues j - z)⁻¹.

theorem Matrix.IsHermitian.trace_inv_sub_smul_one {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) {z : 𝕜} (hz : z ∉ spectrum 𝕜 A) : (A - z • 1)⁻¹.trace = ∑ j : n, (↑(hA.eigenvalues j) - z)⁻¹

Off the spectrum, the trace of the resolvent of a Hermitian matrix is ∑ j, (hA.eigenvalues j - z)⁻¹.

theorem Matrix.IsHermitian.l2_opNorm_inv_sub_smul_one {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) {z : 𝕜} (hz : z ∉ spectrum 𝕜 A) : ‖(A - z • 1)⁻¹‖ = ‖fun (j : n) => (↑(hA.eigenvalues j) - z)⁻¹‖

Off the spectrum, the Euclidean operator norm of the resolvent of a Hermitian matrix is the largest of the moduli ‖hA.eigenvalues j - z‖⁻¹, written as the sup norm of that family.

theorem Matrix.IsHermitian.inv_sub_smul_one_apply {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) {z : 𝕜} (hz : z ∉ spectrum 𝕜 A) (i j : n) : (A - z • 1)⁻¹ i j = ∑ k : n, ↑hA.eigenvectorUnitary i k * (↑(hA.eigenvalues k) - z)⁻¹ * star (↑hA.eigenvectorUnitary j k)

The entrywise spectral expansion of the resolvent of a Hermitian matrix: with U = hA.eigenvectorUnitary and λ = hA.eigenvalues, off the spectrum (A - z • 1)⁻¹ i j = ∑ k, U i k * (λ k - z)⁻¹ * conj (U j k).

theorem Matrix.IsHermitian.conjTranspose_inv_sub_smul_one {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) (z : 𝕜) : (A - z • 1)⁻¹.conjTranspose = (A - (starRingEnd 𝕜) z • 1)⁻¹

The conjugate transpose of the resolvent of a Hermitian matrix at z is the resolvent at conj z.

theorem Matrix.IsHermitian.notMem_spectrum_of_im_ne_zero {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) {z : 𝕜} (hz : RCLike.im z ≠ 0) : z ∉ spectrum 𝕜 A

A scalar with nonzero imaginary part lies outside the spectrum of a Hermitian matrix, whose eigenvalues are real. Unlike IsSelfAdjoint.im_eq_zero_of_mem_spectrum, this needs no C⋆-algebra structure on Matrix n n 𝕜.

theorem Matrix.IsHermitian.isUnit_sub_smul_one_of_im_ne_zero {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) {z : 𝕜} (hz : RCLike.im z ≠ 0) : IsUnit (A - z • 1)

A shifted Hermitian matrix A - z • 1 is invertible when z is not real.

theorem Matrix.IsHermitian.inv_sub_smul_one_sub_inv_sub_smul_one {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) {B : Matrix n n 𝕜} (hB : B.IsHermitian) {z w : 𝕜} (hz : RCLike.im z ≠ 0) (hw : RCLike.im w ≠ 0) : (A - z • 1)⁻¹ - (B - w • 1)⁻¹ = (A - z • 1)⁻¹ * (B - A + (z - w) • 1) * (B - w • 1)⁻¹

The first resolvent identity for two Hermitian matrices and two non-real parameters.

theorem Matrix.IsHermitian.inv_sub_smul_one_sub_inv_sub_smul_one_eq {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) {z w : 𝕜} (hz : RCLike.im z ≠ 0) (hw : RCLike.im w ≠ 0) : (A - z • 1)⁻¹ - (A - w • 1)⁻¹ = (z - w) • ((A - z • 1)⁻¹ * (A - w • 1)⁻¹)

The first resolvent identity for a change of spectral parameter.

theorem Matrix.IsHermitian.l2_opNorm_inv_sub_smul_one_le {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) {z : 𝕜} (hz : RCLike.im z ≠ 0) : ‖(A - z • 1)⁻¹‖ ≤ |RCLike.im z|⁻¹

Resolvent bound. For a Hermitian matrix and a non-real z, the Euclidean operator norm of the resolvent (A - z • 1)⁻¹ is at most |Im z|⁻¹.

theorem Matrix.IsHermitian.l2_opNorm_one_add_sub_conj_smul_inv_sub_smul_one_le {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (hA : A.IsHermitian) {z : ℂ} (hz : z.im ≠ 0) : ‖1 + (z - (starRingEnd ℂ) z) • (A - z • 1)⁻¹‖ ≤ 1

The Cayley expression of a Hermitian resolvent has Euclidean operator norm at most one. The inequality, unlike equality with one, includes the empty matrix.

theorem Matrix.IsHermitian.l2_opNorm_inv_sub_smul_one_sub_le {n : Type u_2} [Fintype n] [DecidableEq n] {A B : Matrix n n ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) {z : ℂ} (hz : z.im ≠ 0) : ‖(A - z • 1)⁻¹ - (B - z • 1)⁻¹‖ ≤ |z.im|⁻¹

At a fixed nonreal parameter the difference of two Hermitian resolvents has operator norm at most 1 / |Im z|, independently of the size of the perturbation.

theorem Matrix.IsHermitian.im_inv_sub_smul_one_apply_self {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) (z : 𝕜) (i : n) : RCLike.im ((A - z • 1)⁻¹ i i) = RCLike.im z * ∑ j : n, ‖(A - z • 1)⁻¹ i j‖ ^ 2

The Ward identity for the resolvent R = (A - z • 1)⁻¹ of a Hermitian matrix, in multiplicative form: Im (R i i) = Im z * ∑ j, ‖R i j‖ ^ 2. No hypothesis on z is needed: when A - z • 1 is singular the nonsingular inverse is 0 and both sides vanish.

theorem Matrix.IsHermitian.sum_norm_inv_sub_smul_one_apply_sq {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) {z : 𝕜} (hz : RCLike.im z ≠ 0) (i : n) : ∑ j : n, ‖(A - z • 1)⁻¹ i j‖ ^ 2 = RCLike.im ((A - z • 1)⁻¹ i i) / RCLike.im z

Ward identity. For a Hermitian matrix and a non-real z, the squared moduli of the entries in a row of the resolvent R = (A - z • 1)⁻¹ sum to Im (R i i) / Im z.

theorem Matrix.IsHermitian.im_inv_sub_smul_one_apply_self_pos {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) {z : 𝕜} (hz : 0 < RCLike.im z) (i : n) : 0 < RCLike.im ((A - z • 1)⁻¹ i i)

The diagonal entries of the resolvent of a Hermitian matrix lie in the upper half-plane when z does.