Eigenvalues and the L2 operator norm of a real symmetric matrix

Matrix.IsHermitian.spectral_theorem diagonalises a Hermitian matrix by a unitary change of basis; since unitaries are isometries for the L2 operator norm and the norm of a diagonal matrix is the sup norm of its diagonal, this bounds ‖A‖ by the largest absolute eigenvalue (Matrix.IsHermitian.l2_opNorm_le_of_abs_eigenvalues_le).

In the other direction, an eigenvector for μ exhibits μ in the spectrum, which for a Hermitian matrix is the range of the eigenvalue function; hence μ ≤ ⨆ i, eigenvalues i (Matrix.IsHermitian.le_ciSup_eigenvalues). Applying this to the top eigenvector, whose norm the operator norm bounds, gives the reverse inequality ⨆ i, eigenvalues i ≤ ‖A‖ (Matrix.IsHermitian.ciSup_eigenvalues_le_l2_opNorm).

Together these are the two directions of the variational characterisation of the largest eigenvalue that Section 14 of bs_lambda.txt needs. Nothing here is specific to the sensitivity graph; it is all material that belongs upstream in Mathlib, and it is stated in the Matrix.IsHermitian namespace accordingly.

Adapted for Lean Pool from Timeroot/BS_Lam at commit 7bd39a8d41ee7910d3296d0477ad18f8fff9d870; ported to Lean Pool with proof and dependency cleanup.

theorem Matrix.IsHermitian.l2_opNorm_le_of_abs_eigenvalues_le {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} [Nonempty n] (hA : A.IsHermitian) {c : ℝ} (hc : ∀ (i : n), |hA.eigenvalues i| ≤ c) : ‖A‖ ≤ c

The L2 operator norm of a symmetric matrix is bounded by any bound on the absolute values of its eigenvalues.

theorem Matrix.IsHermitian.le_ciSup_eigenvalues {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) {μ : ℝ} {v : n → ℝ} (hv : v ≠ 0) (hev : A.mulVec v = μ • v) : μ ≤ ⨆ (i : n), hA.eigenvalues i

Every eigenvalue of a symmetric matrix is at most the largest eigenvalue.

theorem Matrix.IsHermitian.ciSup_eigenvalues_le_l2_opNorm {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} [Nonempty n] (hA : A.IsHermitian) : ⨆ (i : n), hA.eigenvalues i ≤ ‖A‖

The largest eigenvalue of a symmetric matrix is at most its L2 operator norm.

theorem Matrix.IsHermitian.exists_eigenvector_ciSup_eigenvalues {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} [Nonempty n] (hA : A.IsHermitian) : ∃ (v : n → ℝ), v ≠ 0 ∧ A.mulVec v = (⨆ (i : n), hA.eigenvalues i) • v

The largest eigenvalue of a symmetric matrix is attained by an eigenvector.