Matrix products: positivity of powers and nonvanishing of factors

Over a strictly ordered semiring, once some power A ^ k with k > 0 of an entrywise nonnegative square matrix A is strictly positive, every later power is strictly positive too: each row of A has a positive entry, so multiplying a strictly positive matrix by A on the left keeps it strictly positive. This is the form in which positivity propagates along the powers of a primitive matrix.

If a product of matrices is nonzero, then the inner index type is nonempty and neither factor is zero.

Main results

• Matrix.pow_apply_pos_of_le: if A is entrywise nonnegative and A ^ k is strictly positive for some k > 0, then so is A ^ m for every m ≥ k.
• Matrix.nonempty_of_mul_ne_zero, Matrix.left_ne_zero_of_mul_ne_zero, Matrix.right_ne_zero_of_mul_ne_zero: if a matrix product is nonzero, then the inner index type is nonempty and neither factor is zero.

theorem Matrix.pow_apply_pos_of_le {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {A : Matrix n n R} (hA : ∀ (i j : n), 0 ≤ A i j) {k : ℕ} (hk : 0 < k) (hAk : ∀ (i j : n), 0 < (A ^ k) i j) {m : ℕ} (hkm : k ≤ m) (i j : n) : 0 < (A ^ m) i j

If A is entrywise nonnegative and its power A ^ k, for some k > 0, is strictly positive, then every power A ^ m with m ≥ k is strictly positive.

theorem Matrix.nonempty_of_mul_ne_zero {K : Type u_2} [NonUnitalNonAssocSemiring K] {m : Type u_3} {n : Type u_4} {p : Type u_5} [Fintype n] {A : Matrix m n K} {B : Matrix n p K} (h : A * B ≠ 0) : Nonempty n

If a matrix product is nonzero, then the inner index type is nonempty.

theorem Matrix.left_ne_zero_of_mul_ne_zero {K : Type u_2} [NonUnitalNonAssocSemiring K] {m : Type u_3} {n : Type u_4} {p : Type u_5} [Fintype n] {A : Matrix m n K} {B : Matrix n p K} (h : A * B ≠ 0) : A ≠ 0

If a matrix product is nonzero, then its left factor is nonzero.

theorem Matrix.right_ne_zero_of_mul_ne_zero {K : Type u_2} [NonUnitalNonAssocSemiring K] {m : Type u_3} {n : Type u_4} {p : Type u_5} [Fintype n] {A : Matrix m n K} {B : Matrix n p K} (h : A * B ≠ 0) : B ≠ 0

If a matrix product is nonzero, then its right factor is nonzero.