The Perron–Frobenius theorem for irreducible matrices

A square real matrix A is irreducible (Matrix.IsIrreducible) when its entries are nonnegative and the directed graph of its positive entries is strongly connected. For such a matrix some power of 1 + A is strictly positive, that is 1 + A is primitive, and this reduces the theory to the one for strictly positive matrices in TauCeti.LinearAlgebra.Matrix.PerronFrobenius.Positive.

The conclusions are those of the Perron–Frobenius theorem for irreducible matrices. A has an eigenvector all of whose entries are strictly positive, for a strictly positive eigenvalue r, the Perron root, which is the spectral radius of A (Matrix.spectralRadius_eq_of_mulVec_eq_smul). Every nonzero nonnegative eigenvector of A, for any eigenvalue, has strictly positive entries and is a positive multiple of the Perron eigenvector, so its eigenvalue is r. The root r is simple: its eigenspace is spanned by the Perron eigenvector, and its multiplicity as a root of the characteristic polynomial is one. Finally, r y ≤ A y for a real vector y forces A y = r y.

The primitivity of 1 + A and the positivity of nonnegative eigenvectors hold over any linearly ordered commutative ring, such as ℤ. The other statements about a given positive eigenvector work over any linearly ordered field. Existence, and the two statements that use a positive eigenvector of the transpose (simplicity as a root of the characteristic polynomial, and the equality case r y ≤ A y), are stated over ℝ.

Main results

• Matrix.IsIrreducible.isPrimitive_one_add: if A is irreducible, then 1 + A is primitive.
• Matrix.IsIrreducible.exists_mulVec_eq_smul: an irreducible real matrix has an eigenvector with strictly positive entries, for a strictly positive eigenvalue.
• Matrix.IsIrreducible.exists_pos_eq_smul_of_mulVec_eq_smul: a nonzero nonnegative eigenvector of an irreducible matrix is a positive multiple of any eigenvector with strictly positive entries.
• Matrix.IsIrreducible.exists_eq_smul_of_mulVec_eq_smul: the eigenspace of the Perron root is spanned by the Perron eigenvector.
• Matrix.IsIrreducible.rootMultiplicity_charpoly_eq_one: the Perron root is a simple root of the characteristic polynomial.
• Matrix.IsIrreducible.mulVec_eq_smul_of_smul_le_mulVec: if r y ≤ A y, then A y = r y.

References

• E. Seneta, Non-negative Matrices and Markov Chains, Springer (2006), Chapter 1 (irreducible matrices, the reduction to (1 + A) ^ k, and the subinvariance theorem).
• 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.IsIrreducible.isPrimitive_one_add {n : Type u_1} [Fintype n] {K : Type u_2} [CommRing K] [LinearOrder K] [IsStrictOrderedRing K] {A : Matrix n n K} [DecidableEq n] (hA : A.IsIrreducible) : (1 + A).IsPrimitive

If A is irreducible, then 1 + A is primitive: some power of 1 + A has all its entries strictly positive.

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

A nonzero nonnegative eigenvector of an irreducible matrix has all its entries strictly positive.

theorem Matrix.IsIrreducible.exists_pos_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 : A.IsIrreducible) (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 an irreducible matrix is a positive multiple of any eigenvector with strictly positive entries, whatever eigenvalue it was taken for.

theorem Matrix.IsIrreducible.eq_of_mulVec_eq_smul_of_nonneg {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 : A.IsIrreducible) (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 an irreducible matrix has the same eigenvalue as any eigenvector with strictly positive entries.

theorem Matrix.IsIrreducible.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 : A.IsIrreducible) (hv : ∀ (i : n), 0 < v i) (hAv : A.mulVec v = r • v) (hAw : A.mulVec w = r • w) : ∃ (c : K), w = c • v

For an irreducible 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.IsIrreducible.exists_mulVec_eq_smul {n : Type u_1} [Fintype n] {A : Matrix n n ℝ} (hA : A.IsIrreducible) : ∃ (r : ℝ), 0 < r ∧ ∃ (v : n → ℝ), (∀ (i : n), 0 < v i) ∧ A.mulVec v = r • v

Perron–Frobenius theorem for irreducible matrices, existence: an irreducible real square matrix 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), its eigenspace is spanned by the eigenvector (Matrix.IsIrreducible.exists_eq_smul_of_mulVec_eq_smul), and it is a simple root of the characteristic polynomial (Matrix.IsIrreducible.rootMultiplicity_charpoly_eq_one). For empty n the statement holds trivially, with the zero vector.

theorem Matrix.IsIrreducible.mulVec_eq_smul_of_smul_le_mulVec {n : Type u_1} [Fintype n] {A : Matrix n n ℝ} {v y : n → ℝ} {r : ℝ} (hA : A.IsIrreducible) (hv : ∀ (i : n), 0 < v i) (hAv : A.mulVec v = r • v) (hy : r • y ≤ A.mulVec y) : A.mulVec y = r • y

Subinvariance: if A is irreducible with a strictly positive eigenvector for r, and a real vector y satisfies r y ≤ A y entrywise, then y is an eigenvector for r.

theorem Matrix.IsIrreducible.rootMultiplicity_charpoly_eq_one {n : Type u_1} [Fintype n] {A : Matrix n n ℝ} {v : n → ℝ} {r : ℝ} [DecidableEq n] [Nonempty n] (hA : A.IsIrreducible) (hv : ∀ (i : n), 0 < v i) (hAv : A.mulVec v = r • v) : Polynomial.rootMultiplicity r A.charpoly = 1

Perron–Frobenius: the eigenvalue r of a strictly positive eigenvector of an irreducible real matrix is a simple root of its characteristic polynomial.