SpectralPositivity

spectral-positivity

Perron-Frobenius theory, Jentzsch's theorem, and matrix/operator positivity in Lean 4. A shared library used by:

pphi2 — transfer matrix spectral gap
graphops-qft — heat kernel positivity on graphops
markov-semigroups — positivity of Markov semigroups

What this package provides

Matrix level (`Matrix/`)

Nonneg matrix powers: (proved)
Metzler matrix exponential: nonneg off-diagonal for (the heat kernel on a graph has nonneg entries)
Decomposition: with , so
M-matrix inverse positivity: if is a nonsingular M-matrix (a -matrix with positive principal minors / equivalently with entrywise and ), then entrywise. Theorem Matrix.MMatrix.inverse_pos in Matrix/MMatrixInverse.lean. Used by markov-semigroups for the diamagnetic-inequality chain and by graphops-qft for resolvent positivity.
M-matrix inverse non-negativity: the same conclusion without the irreducibility hypothesis: PD with for entrywise. Theorem Matrix.MMatrix.inverse_nonneg in Matrix/MMatrixInverse.lean. Used by markov-semigroups (Matrix/LaplaceTransform.lean re-exports it as m_matrix_inverse_nonneg, the previously axiomatized form) for the diamagnetic chain consumed by pphi2N's QHJ thimble proofs.

Operator level (`Operator/`)

Positivity-preserving: (on )
Positivity-improving: , a.e.
Jentzsch's theorem: For compact self-adjoint positivity-improving :
- Simple ground eigenvalue
- Ground eigenfunction a.e.
- Spectral gap: for all other eigenvalues

The Jentzsch proof was originally developed in pphi2 (1082 lines, fully proved) for the P(Phi)_2 transfer matrix. This package extracts and generalizes it to work on any measure space, making it reusable.

The matrix positivity was developed in graphops-qft for heat kernels on graphop semigroups.

File structure

SpectralPositivity/
  Matrix/
    NonnegPower.lean      -- M ≥ 0 ⟹ M^k ≥ 0, truncated exp nonneg
    MetzlerExp.lean       -- Metzler decomposition, e^{tL} ≥ 0
    MMatrixInverse.lean   -- M-matrix ⟹ M⁻¹ > 0 entrywise
  Operator/
    PositivityPreserving.lean -- IsPositivityPreserving, IsPositivityImproving
    Jentzsch.lean             -- Jentzsch theorem (spectral gap)

Building

lake update
lake build

References

Reed and Simon, Methods of Modern Mathematical Physics IV, 1978, Theorems XIII.43–44.
Horn and Johnson, Matrix Analysis, Cambridge, 2013, Thm 8.5.5.
Berman and Plemmons, Nonnegative Matrices in the Mathematical Sciences, SIAM, 1994.

SpectralPositivity0.1.0