Perron–Frobenius Theorem for Nonneg Matrices

If A ≥ 0 is irreducible, then:

• The spectral radius r(A) is a simple eigenvalue of A
• There exists a corresponding eigenvector v > 0 (all entries strictly positive)
• |λ| ≤ r(A) for all eigenvalues λ

Proof strategy

We prove the existence part using the Collatz–Wielandt minimax characterization. For B = A^k with all entries strictly positive (from exists_pos_power):

1. Define ρ(v) = min_i (Bv)_i/v_i on the positive part of the simplex.
2. Restrict to compact subsets S_ε = {v | v_i ≥ ε, ∑ v_i = 1} and maximize ρ.
3. Show the maximizer has all ratios (Bv)_i/v_i equal (eigenvector of B).
4. Lift from B = A^k to A using commutativity and uniqueness of the Perron eigenvector of B.

References

• Horn–Johnson, Matrix Analysis, Cambridge, 2013, Ch. 8
• Seneta, Non-negative Matrices and Markov Chains, Springer, 2006

def Matrix.IsIrreducible {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) : Prop

A nonneg matrix A is irreducible if: (1) all entries are nonneg, (2) for every pair (i, j) there exists k > 0 such that (A^k)_{ij} > 0 (i.e., the directed graph of A is strongly connected), and (3) there exists a vertex with a positive self-loop (aperiodicity).

The aperiodicity condition (3) is necessary for exists_pos_power. Without it, periodic irreducible matrices (e.g., the permutation matrix of a 2-cycle [[0,1],[1,0]]) satisfy (1)-(2) but have no single power k with all entries of A^k strictly positive.

This definition therefore characterizes primitive nonneg matrices.

Equations

• A.IsIrreducible = (A.Nonneg ∧ (∀ (i j : n), ∃ (k : ℕ), 0 < k ∧ 0 < (A ^ k) i j) ∧ ∃ (i : n), 0 < A i i)

Submultiplicativity and padding lemmas

theorem Matrix.Nonneg.pos_pow_mul {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.Nonneg) {a b : ℕ} {i j l : n} (ha : 0 < (A ^ a) i j) (hb : 0 < (A ^ b) j l) : 0 < (A ^ (a + b)) i l

Submultiplicativity for nonneg matrix powers: if (A^a){ij} > 0 and (A^b){jl} > 0, then (A^{a+b}){il} > 0. This follows by extracting the single positive term (A^a){ij} * (A^b){jl} from the matrix product sum ∑m (A^a){im} * (A^b){ml}, with all other terms nonneg.

theorem Matrix.Nonneg.pos_pow_pad {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.Nonneg) {r : n} (hdiag : 0 < A r r) {k : ℕ} {i : n} (hk : 0 < (A ^ k) i r) (m : ℕ) : 0 < (A ^ (k + m)) i r

Padding lemma: if A is nonneg with A_{rr} > 0 and (A^k){ir} > 0, then (A^{k+m}){ir} > 0 for all m ≥ 0. The positive self-loop at r absorbs arbitrary additional steps: each extra step contributes a factor of A_{rr} > 0 through the path staying at r.

Primitive power existence

theorem Matrix.IsIrreducible.exists_pos_power {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsIrreducible) : ∃ (k : ℕ), 0 < k ∧ ∀ (i j : n), 0 < (A ^ k) i j

An irreducible nonneg matrix has a primitive power: there exists k such that A^k has all strictly positive entries.

Proof. Fix a vertex r with A_{rr} > 0 (the aperiodicity condition). For each i, choose kᵢ with (A^{kᵢ}){ir} > 0 (connectivity to r). For each j, choose kⱼ with (A^{kⱼ}){rj} > 0 (connectivity from r). By submultiplicativity through r: (A^{kᵢ + kⱼ}){ij} ≥ (A^{kᵢ}){ir} · (A^{kⱼ}){rj} > 0. By the padding lemma (using A{rr} > 0), we can inflate kᵢ by any amount: (A^{kᵢ + m}){ir} > 0 for all m ≥ 0. Setting K = max_i(kᵢ) + max_j(kⱼ) and writing K = kᵢ + slack + kⱼ with slack = K − kᵢ − kⱼ ≥ 0, the padded submultiplicativity gives (A^K){ij} ≥ (A^{kᵢ + slack}){ir} · (A^{kⱼ}){rj} > 0 for all i, j.

Perron–Frobenius theorem

Helper lemmas for mulVec positivity

theorem Matrix.Nonneg.mulVec_nonneg {n : Type u_1} [Fintype n] {A : Matrix n n ℝ} (hA : A.Nonneg) {v : n → ℝ} (hv : ∀ (i : n), 0 ≤ v i) (i : n) : 0 ≤ A.mulVec v i

A nonneg matrix applied to a nonneg vector gives a nonneg vector.

theorem Matrix.mulVec_pos_of_allPos {n : Type u_1} [Fintype n] {B : Matrix n n ℝ} (hB : ∀ (i j : n), 0 < B i j) {v : n → ℝ} (hv_nn : ∀ (i : n), 0 ≤ v i) (hv_ne : ∃ (j : n), 0 < v j) (i : n) : 0 < B.mulVec v i

A matrix with all positive entries, applied to a nonneg nonzero vector, gives a strictly positive vector.

theorem Matrix.mulVec_pos_of_pos {n : Type u_1} [Fintype n] {A : Matrix n n ℝ} (hA : A.Nonneg) (hrows : ∀ (i : n), ∃ (j : n), 0 < A i j) {v : n → ℝ} (hv : ∀ (i : n), 0 < v i) (i : n) : 0 < A.mulVec v i

A nonneg matrix applied to a positive vector gives a positive vector, provided each row has a positive entry.

theorem Matrix.IsIrreducible.row_has_pos_entry {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsIrreducible) (i : n) : ∃ (j : n), 0 < A i j

An irreducible nonneg matrix has at least one positive entry in each row (since for each i, there exists k > 0 and j with (A^k)_{ij} > 0, and the first step of the path gives a positive entry in row i of A).

theorem Matrix.pow_mulVec_comp {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} {m l : ℕ} {v : n → ℝ} : (A ^ m).mulVec ((A ^ l).mulVec v) = (A ^ (m + l)).mulVec v

pow and mulVec interaction: (A^m).mulVec ((A^l).mulVec v) = (A^(m+l)).mulVec v.

theorem collatz_wielandt_monotone {n : Type u_1} [Fintype n] {B : Matrix n n ℝ} (hB_nn : ∀ (i j : n), 0 ≤ B i j) {v : n → ℝ} {lam : ℝ} (hBv_ge : ∀ (i : n), lam * v i ≤ B.mulVec v i) (i : n) : lam * B.mulVec v i ≤ (B * B).mulVec v i

Key Collatz–Wielandt monotonicity: if Bv >= lamv componentwise and B >= 0, then B^2 v >= lam(Bv) componentwise.

theorem collatz_wielandt_strict {n : Type u_1} [Fintype n] {B : Matrix n n ℝ} (hB : ∀ (i j : n), 0 < B i j) {v : n → ℝ} {lam : ℝ} (hBv_ge : ∀ (i : n), lam * v i ≤ B.mulVec v i) (hBv_strict : ∃ (j : n), lam * v j < B.mulVec v j) (i : n) : lam * B.mulVec v i < (B * B).mulVec v i

Strict version: if B > 0 entrywise and Bv > lamv at some coordinate, then B^2 v > lam(Bv) at every coordinate.

theorem allpos_has_pos_eigenvec {n : Type u_1} [Fintype n] (hn : Nonempty n) {B : Matrix n n ℝ} (hB : ∀ (i j : n), 0 < B i j) : ∃ (μ : ℝ) (w : n → ℝ), 0 < μ ∧ (∀ (i : n), 0 < w i) ∧ B.mulVec w = μ • w

theorem perron_frobenius {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsIrreducible) : ∃ (lam₀ : ℝ) (v : n → ℝ), 0 < lam₀ ∧ (∀ (i : n), 0 < v i) ∧ A.mulVec v = lam₀ • v

Perron–Frobenius (existence): an irreducible nonneg matrix has a positive eigenvalue with a strictly positive eigenvector.

Proof. We use the Collatz–Wielandt minimax characterization.

1. From exists_pos_power, get k > 0 with B = A^k all entries positive.
2. Define ρ(v) = min_i (Bv)_i / v_i on the positive simplex.
3. For B with all entries positive, the map v ↦ Bv/‖Bv‖₁ maps the simplex into its interior, and ρ is well-defined and continuous.
4. On the compact set {v | v_i ≥ ε, ∑ v_i = 1}, ρ attains its maximum.
5. At the maximizer v*, all ratios are equal: Bv* = μv* with μ > 0.
6. Since A commutes with B = A^k, Av* is also an eigenvector of B with eigenvalue μ. By uniqueness of the Perron eigenvector of B (all-positive matrix), Av* = λv* for some λ, and λ > 0 follows from v* > 0.