Perron–Frobenius theorem

For a square matrix $A$ with nonnegative real entries, the Perron root is the Collatz–Wielandt value

r(A) = \sup_{v \geq 0,\ v \neq 0}\ \min_{i\,:\,v_i > 0} \frac{(Av)_i}{v_i}.

Theorem (Perron–Frobenius).

Every nonnegative matrix has $r(A)$ as an eigenvalue, with a nonnegative eigenvector.
If $A$ is irreducible, the eigenvalue $r(A)$ is positive and has a strictly positive eigenvector. Moreover $r(A)$ is the spectral radius: every real eigenvalue $\mu$ satisfies $|\mu| \leq r(A)$.
If $A$ is primitive (some power is entrywise positive), a nonnegative eigenvector with positive eigenvalue is unique up to scaling.
A strictly positive eigenvector can only belong to the eigenvalue $r(A)$.

The proofs go through the Collatz–Wielandt function on the standard simplex, upper semicontinuity and compactness for existence, and a triangle-equality phase argument for dominance. The irreducible case is reduced to the primitive one through $1 + A$.

References

O. Perron, “Zur Theorie der Matrices,” Mathematische Annalen 64 (1907), 248–263.

G. Frobenius, “Über Matrizen aus nicht negativen Elementen,” Sitzungsberichte der Königlich Preussischen Akademie der Wissenschaften (1912), 456–477.

Theorems

The Perron root has a nonnegative eigenvector

Matrix.exists_nonneg_mulVec_eq_perronRoot_smulsource

theorem exists_nonneg_mulVec_eq_perronRoot_smul [Nonempty n]
    {A : Matrix n n ℝ} (hA_nonneg : ∀ i j, 0 ≤ A i j) :
    ∃ v : n → ℝ, (∀ i, 0 ≤ v i) ∧ v ≠ 0 ∧ A *ᵥ v = perronRoot A • v

Irreducible matrices have a positive eigenvector

Matrix.exists_positive_eigenvector_of_irreduciblesource

theorem exists_positive_eigenvector_of_irreducible [Nonempty n]
  (hA_irred : A.IsIrreducible) :
    ∃ (r : ℝ) (v : n → ℝ),
      0 < r ∧ (∀ i, 0 < v i) ∧ A *ᵥ v = r • v

Primitive matrices: uniqueness of the eigenvector

Matrix.pft_primitivesource

theorem pft_primitive
    {n : Type*} [Fintype n] [Nonempty n] [DecidableEq n]
    {A : Matrix n n ℝ} (hA_prim : IsPrimitive A)
    (hA_nonneg : ∀ i j, 0 ≤ A i j) :
    ∃! (v : RealRooted.standardSimplex ℝ n), ∃ (r : ℝ) (_ : r > 0), A *ᵥ v.val = r • v.val

The Perron root is the spectral radius

Matrix.perron_root_is_spectral_radiussource

theorem perron_root_is_spectral_radius (hA_irred : A.IsIrreducible) (hA_nonneg : ∀ i j, 0 ≤ A i j) :
    let r

A positive eigenvector belongs to the Perron root

Matrix.CollatzWielandt.eq_perron_root_of_positive_eigenvectorsource

theorem eq_perron_root_of_positive_eigenvector
    {A : Matrix n n ℝ} {r : ℝ} {v : n → ℝ}
    (hA_nonneg : ∀ i j, 0 ≤ A i j)
    (hv_pos : ∀ i, 0 < v i)
    (hr_pos : 0 < r)
    (h_eig : A *ᵥ v = r • v) :
    r = CollatzWielandt.perronRoot (A := A)

Perron–Frobenius theorem

References

≔ Definitions

⊢ Theorems

Definitions

Theorems