The Perron–Frobenius theorem for nonnegative matrices

An entrywise nonnegative real square matrix A has its spectral radius r as an eigenvalue, with an eigenvector whose entries are nonnegative and not all zero. Moreover r dominates every t satisfying t y ≤ A y entrywise for some nonzero nonnegative vector y, which is the lower half of the Collatz–Wielandt formula.

Without positivity or irreducibility these statements cannot be sharpened: the eigenvector may have zero entries, and other nonnegative eigenvectors may belong to smaller eigenvalues, as the diagonal matrix with entries 1 and 2 shows; and it need not be unique up to scalars, as the identity matrix of size two shows. For strictly positive and for irreducible matrices see TauCeti.LinearAlgebra.Matrix.PerronFrobenius.Positive and TauCeti.LinearAlgebra.Matrix.PerronFrobenius.Irreducible.

The proof is the classical continuity argument. For ε > 0 the matrix A + ε J, where J has all entries 1, is strictly positive, so it has a Perron eigenvector v_ε in the standard simplex, with eigenvalue r_ε. Since A v_ε ≤ r_ε v_ε, the Collatz–Wielandt bounds for A against the strictly positive vector v_ε show that r_ε dominates every complex eigenvalue of A in modulus, and every t as above. The standard simplex is compact, so along a sequence ε → 0 the vectors v_ε have a limit point v, at which the eigenvalues r_ε converge to some r; in the limit A v = r v, and r keeps both domination properties, so it is the spectral radius.

Main results

• Matrix.exists_mulVec_eq_smul_of_nonneg: an entrywise nonnegative real square matrix has a nonzero nonnegative eigenvector whose eigenvalue is its spectral radius.
• Matrix.ofReal_le_spectralRadius_of_smul_le_mulVec: if t y ≤ A y for a nonzero nonnegative vector y, then t is at most the spectral radius of A.

References

• R. A. Horn, C. R. Johnson, Matrix Analysis, 2nd ed., Cambridge University Press (2013), Section 8.3 (Theorem 8.3.1 and its proof by approximation with positive matrices).
• E. Seneta, Non-negative Matrices and Markov Chains, Springer (2006), Chapter 1.
• P. Etingof, S. Gelaki, D. Nikshych, V. Ostrik, Tensor Categories, Mathematical Surveys and Monographs 205, AMS (2015), Section 3.2 (the Frobenius–Perron theorem).

theorem Matrix.exists_mulVec_eq_smul_of_nonneg {n : Type u_1} [Fintype n] {A : Matrix n n ℝ} [Nonempty n] (hA : ∀ (i j : n), 0 ≤ A i j) : ∃ (r : ℝ), 0 ≤ r ∧ spectralRadius ℂ (A.map Complex.ofReal) = ENNReal.ofReal r ∧ ∃ (v : n → ℝ), 0 ≤ v ∧ v ≠ 0 ∧ A.mulVec v = r • v

Perron–Frobenius theorem for nonnegative matrices: an entrywise nonnegative real square matrix has its spectral radius r, viewed as a complex matrix, as an eigenvalue, with an eigenvector whose entries are nonnegative and not all zero.

Unlike the strictly positive and irreducible cases (Matrix.exists_mulVec_eq_smul_of_pos and Matrix.IsIrreducible.exists_mulVec_eq_smul), the eigenvector may have zero entries and need not be unique up to scalars, and r may be zero.

theorem Matrix.ofReal_le_spectralRadius_of_smul_le_mulVec {n : Type u_1} [Fintype n] {A : Matrix n n ℝ} (hA : ∀ (i j : n), 0 ≤ A i j) {y : n → ℝ} {t : ℝ} (hy : 0 ≤ y) (hy0 : y ≠ 0) (h : t • y ≤ A.mulVec y) : ENNReal.ofReal t ≤ spectralRadius ℂ (A.map Complex.ofReal)

Collatz–Wielandt bound for nonnegative matrices. If t y ≤ A y entrywise for an entrywise nonnegative real square matrix A and a nonzero vector y with nonnegative entries, then t is at most the spectral radius of A, viewed as a complex matrix.