Email Gateway (Nov 25 2024 at 16:08): Email Gateway (Nov 25 2024 at 16:08):From: Lawrence Paulson <lp15@cam.ac.uk>
I am happy to announce an impressive new development by Sage Binder and Zilin Jiang: Two Theorems on Hermitian Matrices.
We formalize two results on Hermitian matrices. First, Sylvester's criterion: a Hermitian matrix is positive definite if and only if all its leading principal submatrices have positive determinant. Second, Cauchy's eigenvalue interlacing theorem: given a principal submatrix B of a Hermitian matrix A, the eigenvalues of B interlace those of A. Our approach to Sylvester's criterion is fairly standard, and required us to formalize Schur's block matrix determinant formula, which gives a formula for the determinant of a block matrix (A,B,C,D) when A is invertible. Our approach to Cauchy's eigenvalue interlacing theorem follows a proof given in a set of lecture notes by Dr. David Bindel. This approach involved formalizing the Courant-Fischer minimax theorem (a theorem about the Rayleigh quotient, which we define in this entry). In our statement of the Courant-Fischer minimax theorem, we refer to the infimum and supremum instead of the minimum and maximum, as this simplifies the proof and is sufficient to prove Cauchy's eigenvalue interlacing theorem.
Now online at https://www.isa-afp.org/entries/Two_Hermitian_Results.html
Larry Paulson
Last updated: Jan 04 2025 at 20:18 UTC