The Perron–Frobenius theorem for primitive matrices

A square real matrix A is primitive (Matrix.IsPrimitive) when its entries are nonnegative and some power A ^ k with k > 0 is strictly positive. Every later power is then strictly positive too (Matrix.pow_apply_pos_of_le). A primitive matrix is irreducible (Matrix.IsPrimitive.isIrreducible), so the theorem for irreducible matrices applies: it has a Perron root r > 0 with an eigenvector v whose entries are strictly positive (Matrix.IsIrreducible.exists_mulVec_eq_smul), r is its spectral radius (Matrix.spectralRadius_eq_of_mulVec_eq_smul), and r is a simple root of the characteristic polynomial (Matrix.IsIrreducible.rootMultiplicity_charpoly_eq_one).

What primitivity adds is that r strictly dominates every other complex eigenvalue: if A z = μ z for a nonzero complex vector z and μ ≠ r, then ‖μ‖ < r. This fails for irreducible matrices in general: the permutation matrix of a cycle of length p is irreducible, with Perron root 1, and all p-th roots of unity are eigenvalues. The proof applies the strictly positive case, Matrix.eq_of_norm_eq_of_mulVec_eq_smul, to the strictly positive matrices A ^ k and A ^ (k + 1): an eigenvalue μ of modulus r has μ ^ k = r ^ k and μ ^ (k + 1) = r ^ (k + 1), hence μ = r.

Main results

• Matrix.IsPrimitive.eq_of_norm_eq_of_mulVec_eq_smul: the Perron root of a primitive matrix is its only complex eigenvalue of maximal modulus.
• Matrix.IsPrimitive.norm_lt_of_mulVec_eq_smul and Matrix.IsPrimitive.norm_lt_of_mem_spectrum: every other complex eigenvalue of a primitive matrix has modulus strictly less than its Perron root.

References

• E. Seneta, Non-negative Matrices and Markov Chains, Springer (2006), Chapter 1 (primitive matrices, Theorem 1.1).

theorem Matrix.IsPrimitive.eq_of_norm_eq_of_mulVec_eq_smul {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} {v : n → ℝ} {r : ℝ} {μ : ℂ} (hA : A.IsPrimitive) (hv : ∀ (i : n), 0 < v i) (hAv : A.mulVec v = r • v) {z : n → ℂ} (hz : z ≠ 0) (hAz : (A.map Complex.ofReal).mulVec z = μ • z) (hμ : ‖μ‖ = r) : μ = ↑r

Perron–Frobenius: if A v = r v for a primitive real matrix A and a vector v with strictly positive entries, then r is the only complex eigenvalue of A of modulus r.

theorem Matrix.IsPrimitive.norm_lt_of_mulVec_eq_smul {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} {v : n → ℝ} {r : ℝ} {μ : ℂ} (hA : A.IsPrimitive) (hv : ∀ (i : n), 0 < v i) (hAv : A.mulVec v = r • v) {z : n → ℂ} (hz : z ≠ 0) (hAz : (A.map Complex.ofReal).mulVec z = μ • z) (hμ : μ ≠ ↑r) : ‖μ‖ < r

Perron–Frobenius: if A v = r v for a primitive real matrix A and a vector v with strictly positive entries, then every complex eigenvalue μ ≠ r of A has ‖μ‖ < r.

theorem Matrix.IsPrimitive.norm_lt_of_mem_spectrum {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} {v : n → ℝ} {r : ℝ} {μ : ℂ} (hA : A.IsPrimitive) (hv : ∀ (i : n), 0 < v i) (hAv : A.mulVec v = r • v) (hμ : μ ∈ spectrum ℂ (A.map Complex.ofReal)) (hμr : μ ≠ ↑r) : ‖μ‖ < r

Perron–Frobenius: if A v = r v for a primitive real matrix A and a vector v with strictly positive entries, then every point μ ≠ r of the spectrum of A, viewed as a complex matrix, has ‖μ‖ < r.