noncomputable def PerronFrobenius.simplexFixedPoint_pos_matrix {ι : Type u_1} [Fintype ι] [Nonempty ι] (M : Matrix ι ι ℝ) (hM : ∀ (i j : ι), 0 < M i j) : (r : ℝ) ×' (v : ι → ℝ) ×' 0 < r ∧ (∀ (i : ι), 0 < v i) ∧ M.mulVec v = r • v

Existence of a positive Perron-Frobenius eigenvector and eigenvalue for a strictly positive matrix, packaged through the simplex fixed-point construction.

noncomputable def PerronFrobenius.nonneg_matrix_has_nonneg_eigenvector {ι : Type u_1} [Fintype ι] (M : Matrix ι ι ℝ) (hM : ∀ (i j : ι), 0 ≤ M i j) : (r : ℝ) ×' (v : ι → ℝ) ×' 0 ≤ r ∧ (∀ (i : ι), 0 ≤ v i) ∧ (∃ (i : ι), 0 < v i) ∧ M.mulVec v = r • v

A nonnegative matrix admits a nonnegative eigenvalue and a nonnegative eigenvector with at least one strictly positive coordinate.

theorem PerronFrobenius.nonneg_matrix_spectral_radius_dominates {ι : Type u_1} [DecidableEq ι] [Fintype ι] [Nonempty ι] (M : Matrix ι ι ℝ) (hM : ∀ (i j : ι), 0 ≤ M i j) (r : ℝ) (v : ι → ℝ) (hr : 0 ≤ r) (hv : ∀ (i : ι), 0 ≤ v i) (hv_ne : ∃ (i : ι), 0 < v i) (heig : M.mulVec v = r • v) (μ : ℂ) (w : ι → ℂ) (hw_ne : ∃ (i : ι), w i ≠ 0) (heig_c : ∀ (i : ι), ∑ j : ι, ↑(M i j) * w j = μ * w i) : ‖μ‖ ≤ r

For a nonnegative matrix M, the modulus of any complex eigenvalue is bounded above by the nonnegative Perron-Frobenius eigenvalue.