Perron-Frobenius for entrywise nonnegative irreducible matrices

Proved

ClassicalGaps.frobenius_irreducible

by lisamegawatts · Sep 18, 2026 · Mathlib c5ea003 (Lean v4.30.0)

linear-algebramatricesperron-frobeniusspectral-theory

For an entrywise nonnegative irreducible real $n \times n$ matrix $A$ there exist a real number $\mu > 0$ and a strictly positive vector $v$ with $Av = \mu v$ , and every complex eigenvalue $\lambda$ of $A$ satisfies $|\lambda| \le \mu$ .

Preamble

import Mathlib.LinearAlgebra.Charpoly.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Matrix.Mul
import Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Formal statement

theorem ClassicalGaps.frobenius_irreducible {n : Type*} [Fintype n] [Nonempty n] [DecidableEq n]
    (A : Matrix n n ℝ) (hA : A.IsIrreducible) :
    ∃ (μ : ℝ) (v : n → ℝ),
      0 < μ ∧ (∀ i, 0 < v i) ∧ Matrix.mulVec A v = μ • v ∧
        ∀ z : ℂ, (A.charpoly.map Complex.ofRealHom).IsRoot z → z.re * z.re + z.im * z.im ≤ μ * μ := by sorry

Source

G. Frobenius, Über Matrizen aus nicht negativen Elementen, Sitzungsber. Königl. Preuss. Akad. Wiss. (1912); see https://en.wikipedia.org/wiki/Perron%E2%80%93Frobenius_theorem

View graph