Irreducibility and primitivity of nonnegative matrices

This file develops a graph-theoretic interface for studying the properties of nonnegative square matrices.

We associate a directed graph (quiver) with a matrix A, where an edge i ⟶ j exists if and only if the entry A i j is strictly positive. This allows translating algebraic properties of the matrix (like powers) into graph-theoretic properties of its quiver (like theexistence of paths).

Main definitions

• Matrix.toQuiver A: The quiver associated with a matrix A, where an edge i ⟶ j exists if 0 < A i j.
• Matrix.IsIrreducible A: A matrix A is defined as irreducible if it is entrywise nonnegative and its associated quiver toQuiver A is strongly connected. The theorem Matrix.isIrreducible_iff_exists_pow_pos proves this graph-theoretic definition is equivalent to the algebraic one in seneta2006 (Def 1.6, p.18): for every pair of indices (i, j), there exists a positive integer k such that (A ^ k) i j > 0.
• Matrix.IsPrimitive A: A matrix A is primitive if it is nonnegative and some power A ^ k is strictly positive (all entries are > 0), (seneta2006, Definition 1.1, p.14).

Main results

• Matrix.pow_apply_pos_iff_nonempty_path: Establishes the link between matrix powers and graph theory: (A ^ k) i j > 0 if and only if there is a path of length k from i to j in toQuiver A.
• Matrix.isIrreducible_iff_exists_pow_pos: Shows the equivalence between the graph-theoretic definition of irreducibility (strong connectivity) and the algebraic one (existence of a positive entry in some power).
• Matrix.IsPrimitive.to_IsIrreducible: Proves that a primitive matrix is also irreducible (Seneta, p.14).
• Matrix.IsIrreducible.transpose: Shows that the irreducibility property is preserved under transposition.

Implementation notes

Throughout we work over a LinearOrderedRing R. Some results require stronger assumptions, like PosMulStrictMono R or Nontrivial R. Some statements expand matrix powers and thus require [DecidableEq n] to reason about finite sums.

References

• E. Seneta, Non-negative Matrices and Markov Chains

Tags

matrix, nonnegative, positive, power, quiver, graph, irreducible, primitive, perron-frobenius

def Matrix.toQuiver {n : Type u_1} {R : Type u_2} [Ring R] [LinearOrder R] (A : Matrix n n R) : Quiver n

The directed graph (quiver) associated with a matrix A, with an edge i ⟶ j iff 0 < A i j.

Equations

• A.toQuiver = { Hom := fun (i j : n) => 0 < A i j }

structure Matrix.IsIrreducible {n : Type u_1} {R : Type u_2} [Ring R] [LinearOrder R] (A : Matrix n n R) : Prop

A matrix A is irreducible if it is entrywise nonnegative and its quiver of positive entries (toQuiver A) is strongly connected.

• nonneg (i j : n) : 0 ≤ A i j
• connected : Quiver.IsSStronglyConnected n

theorem Matrix.isIrreducible_iff {n : Type u_1} {R : Type u_2} [Ring R] [LinearOrder R] (A : Matrix n n R) : A.IsIrreducible ↔ (∀ (i j : n), 0 ≤ A i j) ∧ Quiver.IsSStronglyConnected n

structure Matrix.IsPrimitive {n : Type u_1} {R : Type u_2} [Ring R] [LinearOrder R] [Fintype n] [DecidableEq n] (A : Matrix n n R) : Prop

A matrix A is primitive if it is entrywise nonnegative and some positive power has all entries strictly positive.

• nonneg (i j : n) : 0 ≤ A i j
• exists_pos_pow : ∃ k > 0, ∀ (i j : n), 0 < (A ^ k) i j

theorem Matrix.isPrimitive_iff {n : Type u_1} {R : Type u_2} [Ring R] [LinearOrder R] [Fintype n] [DecidableEq n] (A : Matrix n n R) : A.IsPrimitive ↔ (∀ (i j : n), 0 ≤ A i j) ∧ ∃ k > 0, ∀ (i j : n), 0 < (A ^ k) i j

theorem Matrix.IsIrreducible.exists_pos {n : Type u_1} {R : Type u_2} [Ring R] [LinearOrder R] {A : Matrix n n R} [Nontrivial n] (h_irr : A.IsIrreducible) (i : n) : ∃ (j : n), 0 < A i j

If A is irreducible and n is non-trivial then every row has a positive entry.

theorem Matrix.pow_apply_pos_iff_nonempty_path {n : Type u_1} {R : Type u_2} [Ring R] [LinearOrder R] {A : Matrix n n R} [Fintype n] [IsOrderedRing R] [PosMulStrictMono R] [Nontrivial R] [DecidableEq n] (hA : ∀ (i j : n), 0 ≤ A i j) (k : ℕ) (i j : n) : 0 < (A ^ k) i j ↔ Nonempty { p : Quiver.Path i j // p.length = k }

For a matrix A with nonnegative entries, the (i, j)-entry of the k-th power A ^ k is strictly positive if and only if there exists a path of length k from i to j in the quiver associated to A via toQuiver.

theorem Matrix.isIrreducible_iff_exists_pow_pos {n : Type u_1} {R : Type u_2} [Ring R] [LinearOrder R] {A : Matrix n n R} [Fintype n] [IsOrderedRing R] [PosMulStrictMono R] [Nontrivial R] [DecidableEq n] (hA : ∀ (i j : n), 0 ≤ A i j) : A.IsIrreducible ↔ ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j

Irreducibility of a nonnegative matrix A is equivalent to entrywise positivity of some power: between any two indices i, j there exists a positive integer k such that the (i, j)-entry of A ^ k is strictly positive.

theorem Matrix.IsPrimitive.isIrreducible {n : Type u_1} {R : Type u_2} [Ring R] [LinearOrder R] {A : Matrix n n R} [Fintype n] [IsOrderedRing R] [PosMulStrictMono R] [Nontrivial R] [DecidableEq n] (h_prim : A.IsPrimitive) : A.IsIrreducible

If a nonnegative square matrix A is primitive, then A is irreducible.

Transposition

def Matrix.transposePath {n : Type u_1} {R : Type u_2} [Ring R] [LinearOrder R] {A : Matrix n n R} {i j : n} (p : Quiver.Path i j) : Quiver.Path j i

Reverse a path in toQuiver A to a path in toQuiver Aᵀ, swapping endpoints.

Equations

• Matrix.transposePath p = Quiver.Path.rec Quiver.Path.nil (fun {b c : n} (q : Quiver.Path i b) (e : b ⟶ c) (ih : Quiver.Path b i) => have eT := ⋯; eT.toPath.comp ih) p

theorem Matrix.IsIrreducible.transpose {n : Type u_1} {R : Type u_2} [Ring R] [LinearOrder R] {A : Matrix n n R} (hA : A.IsIrreducible) : A.transpose.IsIrreducible

Irreducibility is invariant under transpose.

@[simp]

theorem Matrix.isIrreducible_transpose_iff {n : Type u_1} {R : Type u_2} [Ring R] [LinearOrder R] {A : Matrix n n R} : A.transpose.IsIrreducible ↔ A.IsIrreducible