The Perron–Frobenius theorem for positive matrices

A square real matrix all of whose entries are strictly positive has an eigenvector all of whose entries are strictly positive, for a positive eigenvalue r, the Perron root. This eigenvector is unique up to a scalar: every eigenvector for r, of any sign, is a multiple of it, and every nonzero entrywise nonnegative eigenvector, for any eigenvalue, is a positive multiple of it. Finally r is the spectral radius: every complex eigenvalue has modulus at most r, and r is the only one of modulus r.

The comparison arguments work over any linearly ordered semifield; the eigenspace statement for vectors of arbitrary sign uses a linearly ordered field. Their heart is the Collatz–Wielandt bound: if A is entrywise nonnegative and A v ≤ r v with v strictly positive, then t y ≤ A y for a nonzero nonnegative y forces t ≤ r. This bound, and with it the spectral radius statement, needs only nonnegativity of A once a strictly positive eigenvector is given. Existence is specific to ℝ: the Perron root is the largest t for which some point x of the standard simplex (Mathlib's Convexity.StdSimplex) satisfies t x ≤ A x, and the maximum exists by compactness.

These are the statements used to define the Frobenius–Perron dimension of a transitive based ring: there one applies them to the matrix of multiplication by the sum of all basis elements, which is strictly positive by transitivity, and uses the uniqueness of nonnegative eigenvectors to see that the other structure matrices act on the Perron eigenvector by scalars.

Main results

• Matrix.le_of_smul_le_mulVec: the Collatz–Wielandt bound against a positive vector.
• Matrix.exists_eq_smul_of_mulVec_eq_smul: for a strictly positive matrix, the eigenspace of a strictly positive eigenvector is spanned by it.
• Matrix.eq_of_mulVec_eq_smul_of_nonneg and Matrix.exists_pos_eq_smul_of_mulVec_eq_smul: a nonzero nonnegative eigenvector of a strictly positive matrix has the Perron root as eigenvalue, and is a positive multiple of the Perron eigenvector.
• Matrix.exists_mulVec_eq_smul_of_pos: a strictly positive real matrix has a strictly positive eigenvector with positive eigenvalue.
• Matrix.norm_le_of_mulVec_le_smul: if A v ≤ r v for a strictly positive vector v and a nonnegative real matrix A, then every complex eigenvalue has modulus at most r.
• Matrix.spectralRadius_eq_of_mulVec_eq_smul_of_forall_norm_le: an eigenvalue of a real eigenvector that bounds the modulus of every complex eigenvalue is the spectral radius.
• Matrix.spectralRadius_eq_of_mulVec_eq_smul: the eigenvalue of a strictly positive eigenvector of a nonnegative real matrix is its spectral radius.
• Matrix.eq_of_norm_eq_of_mulVec_eq_smul: the Perron root of a strictly positive matrix is its only complex eigenvalue of maximal modulus.

References

• 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), Sections 3.2 (the Frobenius–Perron theorem) and 3.3 (Frobenius–Perron dimensions).

theorem Matrix.pos_of_mulVec_eq_smul {n : Type u_1} [Fintype n] {K : Type u_2} [Semiring K] [PartialOrder K] [IsStrictOrderedRing K] {A : Matrix n n K} {w : n → K} {μ : K} (hA : ∀ (i j : n), 0 < A i j) (hw : 0 ≤ w) (hw0 : w ≠ 0) (hAw : A.mulVec w = μ • w) (i : n) : 0 < w i

A nonzero nonnegative eigenvector of a strictly positive matrix has all entries strictly positive.

theorem Matrix.le_of_smul_le_mulVec {n : Type u_1} [Fintype n] {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {A : Matrix n n K} {v y : n → K} {r t : K} (hA : ∀ (i j : n), 0 ≤ A i j) (hv : ∀ (i : n), 0 < v i) (hAv : A.mulVec v ≤ r • v) (hy : 0 ≤ y) (hy0 : y ≠ 0) (h : t • y ≤ A.mulVec y) : t ≤ r

Collatz–Wielandt bound. Let A be entrywise nonnegative with A v ≤ r v for a vector v all of whose entries are strictly positive. If t y ≤ A y entrywise for some nonzero nonnegative vector y, then t ≤ r.

theorem Matrix.eq_of_mulVec_eq_smul_of_nonneg {n : Type u_1} [Fintype n] {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {A : Matrix n n K} {v w : n → K} {r μ : K} (hA : ∀ (i j : n), 0 < A i j) (hv : ∀ (i : n), 0 < v i) (hAv : A.mulVec v = r • v) (hw : 0 ≤ w) (hw0 : w ≠ 0) (hAw : A.mulVec w = μ • w) : μ = r

A nonzero nonnegative eigenvector of a strictly positive matrix has the same eigenvalue as any eigenvector with strictly positive entries.

theorem Matrix.exists_pos_eq_smul_of_mulVec_eq_smul {n : Type u_1} [Fintype n] {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {A : Matrix n n K} {v w : n → K} {r μ : K} (hA : ∀ (i j : n), 0 < A i j) (hv : ∀ (i : n), 0 < v i) (hAv : A.mulVec v = r • v) (hw : 0 ≤ w) (hw0 : w ≠ 0) (hAw : A.mulVec w = μ • w) : ∃ (c : K), 0 < c ∧ w = c • v

A nonzero nonnegative eigenvector of a strictly positive matrix is a positive multiple of any eigenvector with strictly positive entries, whatever eigenvalue it was taken for.

theorem Matrix.exists_eq_smul_of_mulVec_eq_smul {n : Type u_1} [Fintype n] {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {A : Matrix n n K} {v w : n → K} {r : K} (hA : ∀ (i j : n), 0 < A i j) (hv : ∀ (i : n), 0 < v i) (hAv : A.mulVec v = r • v) (hAw : A.mulVec w = r • w) : ∃ (c : K), w = c • v

For a strictly positive matrix, the eigenspace of an eigenvector v with strictly positive entries is spanned by v: every eigenvector for the same eigenvalue, of any sign, is a multiple of v.

theorem Matrix.exists_mulVec_eq_smul_of_pos {n : Type u_1} [Fintype n] {A : Matrix n n ℝ} (hA : ∀ (i j : n), 0 < A i j) : ∃ (r : ℝ), 0 < r ∧ ∃ (v : n → ℝ), (∀ (i : n), 0 < v i) ∧ A.mulVec v = r • v

Perron–Frobenius theorem for positive matrices, existence: a real square matrix whose entries are all strictly positive has an eigenvector whose entries are all strictly positive, for a strictly positive eigenvalue.

When n is nonempty, this eigenvalue is the spectral radius (Matrix.spectralRadius_eq_of_mulVec_eq_smul), and the eigenvector is unique up to a scalar (Matrix.exists_eq_smul_of_mulVec_eq_smul). For empty n the statement holds trivially, with the zero vector.

theorem Matrix.norm_le_of_mulVec_le_smul {n : Type u_1} [Fintype n] {A : Matrix n n ℝ} {v : n → ℝ} {r : ℝ} (hA : ∀ (i j : n), 0 ≤ A i j) (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) : ‖μ‖ ≤ r

If A v ≤ r v for a vector v with strictly positive entries and an entrywise nonnegative real matrix A, then r bounds the modulus of every complex eigenvalue.

theorem Matrix.eq_of_norm_eq_of_mulVec_eq_smul {n : Type u_1} [Fintype n] {A : Matrix n n ℝ} {v : n → ℝ} {r : ℝ} (hA : ∀ (i j : n), 0 < A i j) (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: the Perron root r of a strictly positive real square matrix is its only complex eigenvalue of modulus r. Together with Matrix.norm_le_of_mulVec_le_smul, every other complex eigenvalue has modulus strictly smaller than r.

theorem Matrix.spectralRadius_eq_of_mulVec_eq_smul_of_forall_norm_le {n : Type u_1} [Fintype n] {A : Matrix n n ℝ} {v : n → ℝ} {r : ℝ} (hv0 : v ≠ 0) (hAv : A.mulVec v = r • v) (hμ : ∀ (μ : ℂ) (z : n → ℂ), z ≠ 0 → (A.map Complex.ofReal).mulVec z = μ • z → ‖μ‖ ≤ r) : spectralRadius ℂ (A.map Complex.ofReal) = ENNReal.ofReal r

If a real square matrix A has a nonzero real eigenvector for an eigenvalue r, and r bounds the modulus of every complex eigenvalue of A, then r is the spectral radius of A, viewed as a complex matrix.

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

Perron–Frobenius: the eigenvalue r of an eigenvector with strictly positive entries of an entrywise nonnegative real square matrix is the spectral radius of the matrix, viewed as a complex matrix. Together with Matrix.exists_mulVec_eq_smul_of_pos, a strictly positive matrix has its spectral radius as an eigenvalue, with an eigenvector whose entries are strictly positive.