Perron's theorem for strictly positive matrices

Proved

ClassicalGaps.perron_positive_matrix

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

linear-algebramatricesperron-frobeniusspectral-theory

For a real $n \times n$ matrix $A$ with strictly positive entries 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

Formal statement

theorem ClassicalGaps.perron_positive_matrix {n : Type*} [Fintype n] [Nonempty n] [DecidableEq n]
    (A : Matrix n n ℝ) (hA : ∀ i j, 0 < A i j) :
    ∃ (μ : ℝ) (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

O. Perron, Grundlagen einer Theorie der Eigenschaften ganzer Funktionen, Math. Ann. 64 (1907); see https://en.wikipedia.org/wiki/Perron%E2%80%93Frobenius_theorem

View graph