M-matrix Inverse Positivity (strict + non-strict)

For a non-singular M-matrix M (positive definite Z-matrix; equivalently PD with non-positive off-diagonal entries), the inverse M⁻¹ is entrywise non-negative; on a "connected" lattice it is in fact strictly positive.

This file provides both forms:

• Matrix.MMatrix.inverse_nonneg — M⁻¹ ≥ 0 entrywise, no irreducibility required. Discharge: Laplace transform identity (laplace_transform_inverse_real) + metzler_exp_nonneg applied to -M (since M Z-matrix ⇒ -M Metzler) + setIntegral_nonneg.
• Matrix.MMatrix.inverse_pos — M⁻¹ > 0 strictly, requiring the Metzler shift Q := α • 1 - M to be Matrix.IsIrreducible (connectedness of the off-diagonal pattern).

References

• Berman & Plemmons, Nonnegative Matrices in the Mathematical Sciences, SIAM, 1994, Ch. 6, Thm 4.16 (Z-matrix inverse positivity).
• Horn & Johnson, Topics in Matrix Analysis, Cambridge, 1991, §2.5.
• Seneta, Non-negative Matrices and Markov Chains, Springer, 2006.

Downstream consumers

• markov-semigroups/Matrix/LaplaceTransform.lean re-exports inverse_nonneg under the historical name m_matrix_inverse_nonneg (formerly an axiom there; now backed by this file). Used in turn by pphi2N's QHJ thimble proofs (Pphi2N/QuantumHJ/ThimbleLocalGeneric.lean etc.) for the diamagnetic / Combes-Thomas resolvent bound on the path to the 2D mass gap.
• graphops-qft consumes the strict version for resolvent positivity.

theorem SpectralPositivity.nonneg_irreducible_matrix_exp_pos {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {Q : Matrix n n ℝ} (hQ_irr : Q.IsIrreducible) {t : ℝ} (ht : 0 < t) (x y : n) : 0 < NormedSpace.exp (t • Q) x y

Strict positivity of exp(t·Q) for irreducible non-negative Q.

For an irreducible non-negative matrix Q (in this library's Matrix.IsIrreducible sense: nonneg + per-pair exists_pos_power

• positive self-loop) and t > 0, every entry of the matrix exponential exp(t·Q) is strictly positive.

Proof: from Q.IsIrreducible.exists_pos_power, ∃ a single k₀ > 0 with (Q^k₀)_{xy} > 0 for ALL pairs (x, y). The matrix-exp series exp(t·Q) = ∑' k, (k!⁻¹) • (t·Q)^k has the k₀-th term strictly positive at every entry (since (t • Q)^k₀ = t^k₀ • Q^k₀ via smul_pow) and all other terms non-negative (Q^k nonneg by Matrix.Nonneg.pow). Entry projection follows the Pi.evalAddMonoidHom + HasSum.map pattern from MetzlerExp.nonneg_matrix_exp_nonneg; conclusion via Summable.tsum_pos.

theorem SpectralPositivity.mmatrix_exp_neg_pos {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {M : Matrix n n ℝ} {α : ℝ} (hQ_irr : (α • 1 - M).IsIrreducible) {t : ℝ} (ht : 0 < t) (x y : n) : 0 < NormedSpace.exp (-t • M) x y

Strict positivity of exp(-tM) for an M-matrix with irreducible Metzler shift.

For M : Matrix n n ℝ and α : ℝ, if the Metzler shift Q := α • 1 - M is irreducible, then for t > 0 every entry of exp(-tM) is strictly positive.

Proof: split (-t) • M = -t·α • 1 + t • Q (commutes since scalar matrices commute with everything). By Matrix.exp_add_of_commute, exp(-tM) = exp(-t·α • 1) * exp(t • Q) = Real.exp(-tα) • exp(t • Q). Both factors are strictly positive: Real.exp_pos for the scalar, nonneg_irreducible_matrix_exp_pos for the matrix. Mirrors the structure of MetzlerExp.metzler_exp_nonneg (non-strict version).

Step 5: Laplace transform identity for M⁻¹.

theorem SpectralPositivity.laplace_transform_inverse_real {n : Type u_1} [Fintype n] [DecidableEq n] (M : Matrix n n ℝ) (hM : M.PosDef) (x y : n) : M⁻¹ x y = ∫ (t : ℝ) in Set.Ioi 0, NormedSpace.exp (-t • M) x y

Laplace transform identity for the inverse of a PD matrix.

For a positive-definite real matrix M, M⁻¹ x y = ∫_(0,∞) (exp(-tM))_xy dt for every entry (x, y).

Proof via spectral decomposition M = U · diag(λ) · Uᵀ: both sides reduce to ∑ k, U(x,k) · (1/λ_k) · U(y,k) using ∫_(0,∞) exp(-λt) dt = 1/λ for λ > 0. (Horn-Johnson §6.2; Higham, Functions of Matrices, Thm 10.2.)

theorem SpectralPositivity.Matrix.MMatrix.inverse_pos {n : Type u_2} [Fintype n] [DecidableEq n] [Nonempty n] (M : Matrix n n ℝ) (hM_pd : M.PosDef) (_hM_off : ∀ (i j : n), i ≠ j → M i j ≤ 0) {α : ℝ} (_hα : ∀ (i : n), M i i ≤ α) (hQ_irr : (α • 1 - M).IsIrreducible) (x y : n) : 0 < M⁻¹ x y

Strict entrywise positivity of an M-matrix inverse (Berman-Plemmons Thm 4.16; Horn-Johnson §2.5).

The full discharge using:

• laplace_transform_inverse_real (Step 5: spectral decomposition)
• mmatrix_exp_neg_pos (Step 4: heat-kernel strict positivity)
• setIntegral_pos_iff_support_of_nonneg_ae (Mathlib: integral positivity from positive integrand on positive-measure support).

Only the α : ℝ parameter and hα are vestigial in this final form (carried for API stability with the original axiom shape).

theorem SpectralPositivity.Matrix.MMatrix.inverse_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] (M : Matrix n n ℝ) (hM_pd : M.PosDef) (hM_off : ∀ (i j : n), i ≠ j → M i j ≤ 0) (x y : n) : 0 ≤ M⁻¹ x y

Entrywise non-negativity of an M-matrix inverse (Berman-Plemmons Thm 4.16; Horn-Johnson §2.5).

For a real PD matrix M whose off-diagonal entries are non-positive (equivalently, a non-singular M-matrix), the inverse M⁻¹ is entrywise non-negative.

This is the non-strict version of Matrix.MMatrix.inverse_pos; it drops the irreducibility hypothesis. The proof uses laplace_transform_inverse_real (M⁻¹ = ∫_(0,∞) exp(-tM) dt) plus the heat-kernel entrywise non-negativity mmatrix_exp_neg_nonneg, combined with setIntegral_nonneg.

Used by markov-semigroups for the diamagnetic-inequality chain (the m_matrix_inverse_nonneg axiom there is replaced by this theorem).