Eigenvalues and spectral norm of Hermitian matrices

TheoremHermitian matrices have real-rooted characteristic polynomials#✓fully proved

The characteristic polynomial of a Hermitian complex matrix is real-rooted.

public theorem IsHermitian.charpoly_isRealRooted
    {n : Type*} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ}
    (hA : A.IsHermitian) : A.charpoly.IsRealRooted

Uses 1 · Used by 1

Statement usesReal-rooted polynomials

Used bySpectral norm of a positive semidefinite matrix

TheoremSpectral norm of a positive semidefinite matrix#✓fully proved

Let \(A\) be a positive semidefinite complex square matrix indexed by a nonempty finite set. Then the operator norm of \(A\) with respect to the Euclidean (\(\ell^2\)) norm equals the largest real part of a root of the characteristic polynomial of \(A\). Since these roots are real, this is its largest root.

public theorem PosSemidef.l2_opNorm_eq_maxRealRoot_charpoly
    {n : Type*} [Fintype n] [DecidableEq n] [Nonempty n] {A : Matrix n n ℂ}
    (hA : A.PosSemidef) : ‖A‖ = A.charpoly.maxRealRoot

Uses 4 · Used by 1

Statement usesLargest real part of a root

Proof usesHermitian matrices have real-rooted characteristic polynomials · For a real-rooted polynomial, the largest real part of a root is a root · Real parts of roots are bounded by the largest one

Used byMarcus--Spielman--Srivastava bound, finite-support form

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.