Documentation

TauCeti.Analysis.Matrix.MulVecNorm

Entrywise norms of complex eigenvectors of nonnegative real matrices #

Let A be an entrywise nonnegative real square matrix, viewed as a complex matrix. If A z = μ z for a complex vector z, then the triangle inequality in each row gives ‖μ‖ ‖z‖ ≤ A ‖z‖ entrywise, where ‖z‖ is the real vector of moduli of the entries of z. Comparison theorems for nonnegative real matrices, such as the Collatz–Wielandt bound of Perron–Frobenius theory, then control the complex eigenvalues of A through this real inequality.

Main results #

theorem Matrix.norm_smul_le_mulVec_norm {n : Type u_1} [Fintype n] {A : Matrix n n ℝ} (hA : ∀ (i j : n), 0 ≤ A i j) {μ : ℂ} {z : n → ℂ} (hAz : (A.map Complex.ofReal).mulVec z = μ • z) :
(‖μ‖ • fun (i : n) => ‖z i‖) ≤ A.mulVec fun (i : n) => ‖z i‖

For an entrywise nonnegative real matrix A and a complex eigenvector z for μ, the moduli of the entries of z satisfy ‖μ‖ ‖z‖ ≤ A ‖z‖, by the triangle inequality.