Nonneg Matrix Powers and Positivity

Proves that nonneg matrices have nonneg powers, and that the truncated matrix exponential of a nonneg matrix is nonneg. These are the building blocks for the Metzler matrix exponential theorem (in MetzlerExp.lean).

Main results (all PROVED)

• Matrix.Nonneg.pow — M ≥ 0 ⟹ M^k ≥ 0
• Matrix.Nonneg.sum — sum of nonneg matrices is nonneg
• Matrix.Nonneg.smul — c ≥ 0 and M ≥ 0 ⟹ cM ≥ 0
• truncated_exp_nonneg — Σ_{k≤N} (tM)^k/k! ≥ 0 for M ≥ 0, t ≥ 0
• markov_generator_nonneg_offdiag — M ≥ 0 ⟹ (M-I) nonneg off-diagonal

References

• Berman and Plemmons, Nonnegative Matrices, SIAM, 1994

def Matrix.NonnegOffDiag {n : Type u_1} (L : Matrix n n ℝ) : Prop

A matrix has nonneg off-diagonal entries (Metzler condition).

Equations

• L.NonnegOffDiag = ∀ (i j : n), i ≠ j → 0 ≤ L i j

def Matrix.Nonneg {n : Type u_1} (M : Matrix n n ℝ) : Prop

A matrix has all nonneg entries.

Equations

• M.Nonneg = ∀ (i j : n), 0 ≤ M i j

theorem Matrix.Nonneg.pow {n : Type u_1} [Fintype n] [DecidableEq n] {M : Matrix n n ℝ} (hM : M.Nonneg) (k : ℕ) : (M ^ k).Nonneg

A nonneg matrix has nonneg powers.

theorem Matrix.Nonneg.sum {n : Type u_1} {ι : Type u_2} {s : Finset ι} {M : ι → Matrix n n ℝ} (hM : ∀ i ∈ s, (M i).Nonneg) : (∑ i ∈ s, M i).Nonneg

Sum of nonneg matrices is nonneg.

theorem Matrix.Nonneg.smul {n : Type u_1} {M : Matrix n n ℝ} (hM : M.Nonneg) {c : ℝ} (hc : 0 ≤ c) : (c • M).Nonneg

Scalar multiple of a nonneg matrix by a nonneg scalar is nonneg.

theorem truncated_exp_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] {M : Matrix n n ℝ} (hM : M.Nonneg) {t : ℝ} (ht : 0 ≤ t) (N : ℕ) : (∑ k ∈ Finset.range (N + 1), (1 / ↑k.factorial) • (t • M) ^ k).Nonneg

The truncated matrix exponential Σ_{k=0}^{N} (tM)^k / k! is nonneg when M is nonneg and t ≥ 0.

theorem markov_generator_nonneg_offdiag {m : Type u_2} [DecidableEq m] (M : Matrix m m ℝ) (hM : M.Nonneg) : (M - 1).NonnegOffDiag

For a Markov operator M (nonneg entries), the generator L = M - I has nonneg off-diagonal entries: L_{xy} = M_{xy} ≥ 0 for x ≠ y.