Spectral projectors, traces, continuity and measurability of the Hermitian functional calculus #

For a Hermitian matrix A over 𝕜 = ℝ or ℂ (any RCLike field) and a real function f, Mathlib's continuous functional calculus defines the matrix cfc f A. Every real function is continuous on the finite spectrum of A, so cfc f A is meaningful for arbitrary f. This file relates it to the eigenspaces of A and studies its dependence on A.

Eigenvectors and spectral projectors. The Euclidean operator of cfc f A multiplies an eigenvector of A with eigenvalue μ by f μ, so it is the functional calculus LinearMap.IsSymmetric.cfc of the symmetric operator Matrix.toEuclideanLin A. For a set Ω ⊆ ℝ, the Euclidean operator of the star projection cfc (Ω.indicator 1) A (see TauCeti.isStarProjection_cfc_indicator) is therefore the orthogonal projection onto the sum Module.End.pointSpectralSubspace A.toEuclideanLin Ω of the eigenspaces of A at eigenvalues in Ω. For Ω = [c, ∞) this is the fixed-threshold spectral projector P_[c,∞)(A), the cluster object used for spectral subspaces in the presence of eigenvalue multiplicity.

Intertwiners. A rectangular matrix V with A * V = V * B for Hermitian A and B also satisfies cfc f A * V = V * cfc f B, since both functional calculi agree with one polynomial on the two finite spectra. Compressing cfc f A to an A-invariant subspace thus gives the functional calculus of the compression of A.

Traces. The trace of cfc f A is ∑ᵢ f(aᵢ) over the eigenvalues aᵢ of A. For a second Hermitian matrix B with eigenvalues bⱼ, the trace of cfc f A * cfc g B is ∑ᵢ ∑ⱼ f(aᵢ) g(bⱼ) ‖⟪uᵢ, vⱼ⟫‖², where uᵢ and vⱼ are the orthonormal eigenvectors. This reduces trace inequalities for noncommuting Hermitian matrices, such as the positivity of relative entropy, to scalar inequalities between eigenvalues.

Continuity. For continuous f, the map A ↦ cfc f A is continuous on the Hermitian matrices for the entrywise topology. This is Mathlib's continuity of the isometric functional calculus in its operator variable, which is available for matrices under the scoped ℓ² operator norm.

Measurability. For continuous f, the map A ↦ cfc f A is Borel measurable on all of Matrix n n 𝕜: it is continuous on the closed set of Hermitian matrices and zero off it. Since the spectrum of a matrix is finite, pointwise convergence F k → f gives cfc (F k) A → cfc f A, so measurability passes to pointwise limits of continuous functions. The indicator of a closed set is such a limit, so spectral projectors A ↦ cfc (Ω.indicator 1) A for closed Ω, in particular the fixed-threshold projectors, are Borel measurable even though they are not continuous. Composing with a measurable random matrix ω ↦ A ω gives measurability of ω ↦ cfc f (A ω) and of ω ↦ P_[c,∞)(A ω); no Hermitian hypothesis on A ω is needed for this.

Main results #

Matrix.IsHermitian.cfc_mul_eq_mul_cfc — A * V = V * B implies cfc f A * V = V * cfc f B;
Matrix.IsHermitian.toEuclideanLin_cfc_apply_of_apply_eq_smul — cfc f A acts by f μ on an eigenvector of A with eigenvalue μ;
Matrix.IsHermitian.toEuclideanLin_cfc — the Euclidean operator of cfc f A is the symmetric functional calculus LinearMap.IsSymmetric.cfc f of A.toEuclideanLin;
Matrix.IsHermitian.toEuclideanLin_cfc_indicator — the Euclidean operator of cfc (Ω.indicator 1) A is the orthogonal projection onto the point-spectral subspace Module.End.pointSpectralSubspace A.toEuclideanLin Ω;
Matrix.IsHermitian.trace_cfc, Matrix.IsHermitian.trace_cfc_mul_cfc and Matrix.IsHermitian.re_trace_cfc_mul_cfc — the traces of cfc f A and of cfc f A * cfc g B in terms of eigenvalues and eigenvector overlaps;
TauCeti.continuousOn_matrix_cfc — for continuous f, A ↦ cfc f A is continuous on the Hermitian matrices;
TauCeti.tendsto_matrix_cfc_fun — pointwise convergence of functions gives convergence of their functional calculi at every matrix;
TauCeti.measurable_matrix_cfc — for continuous f, A ↦ cfc f A is measurable;
TauCeti.measurable_matrix_cfc_of_tendsto — the same for pointwise limits of continuous f;
TauCeti.measurable_matrix_cfc_indicator — for closed Ω, the spectral projector A ↦ cfc (Ω.indicator 1) A is measurable.

References #

R. A. Horn, C. R. Johnson, Matrix Analysis, 2nd ed., Cambridge University Press (2013), §§2.5 and 7.2 (the spectral theorem and functions of Hermitian matrices).
R. Bhatia, Matrix Analysis, Graduate Texts in Mathematics 169, Springer (1997), §VII.3 (spectral projectors of Hermitian matrices).