Metzler Matrix Exponential Positivity

A Metzler matrix (nonneg off-diagonal) generates a positive semigroup: e^{tL} ≥ 0 for all t ≥ 0.

Proof strategy

Decompose L = -cI + N where c = max_i |L_{ii}| and N ≥ 0 (nonneg entries). Then e^{tL} = e^{-ct} e^{tN}, and e^{tN} ≥ 0 follows from truncated_exp_nonneg (in NonnegPower.lean) plus a limit argument using the entrywise convergence of partial sums to the matrix exponential.

References

• Berman–Plemmons, Nonnegative Matrices, SIAM, 1994, Ch. 6
• Horn–Johnson, Matrix Analysis, Cambridge, 2013, Thm 8.5.5

theorem metzler_decomp {n : Type u_2} [Finite n] [DecidableEq n] (L : Matrix n n ℝ) (hL : L.NonnegOffDiag) : ∃ (c : ℝ) (N : Matrix n n ℝ), 0 ≤ c ∧ N.Nonneg ∧ L = -c • 1 + N

Metzler decomposition: a Metzler matrix L can be written as L = -cI + N where c ≥ 0 and N has all nonneg entries.

theorem nonneg_matrix_exp_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] {N : Matrix n n ℝ} (hN : N.Nonneg) {t : ℝ} (ht : 0 ≤ t) : (NormedSpace.exp (t • N)).Nonneg

The matrix exponential of a nonneg matrix is nonneg: if N ≥ 0 then exp(tN) ≥ 0 for all t ≥ 0. This follows from truncated_exp_nonneg and entrywise convergence of the power series.

theorem metzler_exp_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] {L : Matrix n n ℝ} (hL : L.NonnegOffDiag) {t : ℝ} (ht : 0 ≤ t) : (NormedSpace.exp (t • L)).Nonneg

Main theorem: if L is Metzler (nonneg off-diagonal entries), then e^{tL} ≥ 0 for all t ≥ 0. The semigroup generated by a Metzler matrix is a positive semigroup.