Empirical spectral measures of matrices #

For a Hermitian matrix A of positive size n, the empirical spectral measure L_A = n⁻¹ ∑ᵢ δ_{λᵢ(A)} is the probability measure on ℝ putting mass 1/n at each eigenvalue, counted with multiplicity. For a general complex square matrix, the eigenvalue measure is the probability measure n⁻¹ ∑ δ_z on ℂ, the sum running over the roots of the characteristic polynomial with algebraic multiplicity. These are the basic objects of random matrix theory: global laws such as the semicircle and circular laws are limit theorems for them.

Both measures are built from TauCeti.Probability.empiricalMeasureOfFintype, whose evaluation, integration and pushforward API applies to them directly. The Hermitian measure depends only on the characteristic polynomial, not on the basis or on the eigenvector choice, and its pushforward along ℝ → ℂ is the eigenvalue measure. The eigenvalue measure of a nilpotent matrix is the Dirac mass at 0; this records that roots are counted with algebraic, not geometric, multiplicity.

The spectral measure depends continuously on the Hermitian matrix for the weak topology and measurably for the entrywise measurable structure. Thus a measurable random Hermitian matrix has a measurable empirical spectral measure, including when eigenvalues collide.

The moments and the resolvent transform of the Hermitian spectral measure are normalized traces: ∫ x ^ k dL_A = n⁻¹ Re tr (A ^ k) and, off the spectrum, m_{L_A}(z) = n⁻¹ tr (A - z • 1)⁻¹. These identities turn the moment method and the resolvent method for global laws into computations with traces of matrices.

If A.charpoly = X ^ k * B.charpoly, the spectral measure of A is the mixture of that of B and of the Dirac mass at 0, with weights proportional to the size of B and to k. For the Gram matrices of a card m × card n matrix A with card m ≤ card n this is the exact zero-mass correction L_{AᴴA} = (card m / card n) L_{AAᴴ} + (1 - card m / card n) δ₀, and with k = card n - card m the resolvent transforms satisfy the companion identity m_{L_{AᴴA}}(z) = (card m / card n) m_{L_{AAᴴ}}(z) - (k / card n) z⁻¹. These relate the spectral measures of a sample covariance matrix X * Xᴴ / n and of its companion Xᴴ * X / n.

Main definitions #

Matrix.spectralMeasure A hA — the empirical spectral measure of a Hermitian matrix;
Matrix.eigenvalueMeasure A — the empirical measure of the characteristic roots of a complex square matrix.

Main results #

Matrix.spectralMeasure_eq_of_charpoly_eq — Hermitian matrices with the same characteristic polynomial have the same spectral measure;
Matrix.spectralMeasure_units_conj, Matrix.eigenvalueMeasure_units_conj — both measures are invariant under conjugation by an invertible matrix;
Matrix.eigenvalueMeasure_apply — the eigenvalue measure of a set is the proportion of characteristic roots in it, counted with algebraic multiplicity;
Matrix.map_spectralMeasure_ofReal — for a complex Hermitian matrix, the eigenvalue measure is the pushforward of the spectral measure along ℝ → ℂ;
Matrix.spectralMeasure_apply_singleton_zero — the zero atom has mass equal to the normalized nullity;
Matrix.charpoly_roots_filter_ne_zero_mul_eq — rectangular products have the same nonzero characteristic roots, counted with multiplicity;
Matrix.gram_spectralMeasure_moments_mul_card_eq — their positive spectral moments agree after weighting by the matrix dimensions;
Matrix.PosSemidef.ae_mem_Ici_spectralMeasure — the spectral measure of a positive-semidefinite matrix is concentrated on the nonnegative reals;
Matrix.eigenvalueMeasure_toMeasure_of_isNilpotent — a nilpotent matrix has eigenvalue measure δ₀;
Matrix.integral_pow_spectralMeasure — the k-th moment of the spectral measure is the normalized trace of A ^ k;
Matrix.resolventTransform_spectralMeasure — the resolvent transform of the spectral measure is the normalized trace of the resolvent (A - z • 1)⁻¹;
Matrix.spectralMeasure_toMeasure_of_charpoly_eq_X_pow_mul, Matrix.integral_spectralMeasure_of_charpoly_eq_X_pow_mul and Matrix.resolventTransform_spectralMeasure_of_charpoly_eq_X_pow_mul — the spectral measure, its integrals and its resolvent transform when A.charpoly = X ^ k * B.charpoly;
Matrix.spectralMeasure_conjTranspose_mul_self, Matrix.spectralMeasure_mul_conjTranspose_self — the zero-mass correction between the spectral measures of Aᴴ * A and A * Aᴴ;
Matrix.IsHermitian.spectralMeasure_real_Iic — the distribution function of the spectral measure is the proportion of eigenvalues at most t.

References #

G. W. Anderson, A. Guionnet, O. Zeitouni, An Introduction to Random Matrices, Cambridge University Press (2010), §2.1.
T. Tao, Topics in Random Matrix Theory, American Mathematical Society (2012), §2.4.