theorem PerronFrobenius.continuous_mulVec_component {ι : Type u_1} [Fintype ι] (M : Matrix ι ι ℝ) (i : ι) : Continuous fun (p : (ι → ℝ) × ℝ) => M.mulVec p.1 i

Continuity of the i-th component of M.mulVec as a function of (v, t).

theorem PerronFrobenius.simplex_le_one {ι : Type u_1} [Fintype ι] {v : ι → ℝ} (hv : v ∈ stdSimplex ℝ ι) (i : ι) : v i ≤ 1

Each coordinate of a point in the standard simplex is bounded above by 1.

theorem PerronFrobenius.mulVec_pos {ι : Type u_1} [Fintype ι] (M : Matrix ι ι ℝ) (hM : ∀ (i j : ι), 0 < M i j) {v : ι → ℝ} (hv : v ∈ stdSimplex ℝ ι) (i : ι) : 0 < M.mulVec v i

For a strictly positive matrix M and any point in the standard simplex, every coordinate of M.mulVec v is strictly positive.

def PerronFrobenius.CWSet {ι : Type u_1} [Fintype ι] (M : Matrix ι ι ℝ) : Set ((ι → ℝ) × ℝ)

Collatz-Wielandt set: pairs (v, t) with v in the standard simplex, t ≥ 0, and t * v i ≤ (M.mulVec v) i for all i. The Perron-Frobenius eigenvalue is realised as the supremum of t over this set.

theorem PerronFrobenius.cwSet_closed {ι : Type u_1} [Fintype ι] (M : Matrix ι ι ℝ) : IsClosed (CWSet M)

The Collatz-Wielandt set is closed.

theorem PerronFrobenius.cwSet_subset_compact {ι : Type u_1} [Fintype ι] (M : Matrix ι ι ℝ) (hM : ∀ (i j : ι), 0 < M i j) : CWSet M ⊆ stdSimplex ℝ ι ×ˢ Set.Icc 0 (∑ i : ι, ∑ j : ι, M i j)

The Collatz-Wielandt set is contained in the compact product of the standard simplex and [0, ∑ M i j].

theorem PerronFrobenius.cwSet_compact {ι : Type u_1} [Fintype ι] (M : Matrix ι ι ℝ) (hM : ∀ (i j : ι), 0 < M i j) : IsCompact (CWSet M)

The Collatz-Wielandt set is compact.

theorem PerronFrobenius.cwSet_nonempty {ι : Type u_1} [Fintype ι] [Nonempty ι] (M : Matrix ι ι ℝ) (hM : ∀ (i j : ι), 0 < M i j) : (CWSet M).Nonempty

The Collatz-Wielandt set is nonempty, witnessed by the uniform distribution paired with t = 0.

noncomputable def PerronFrobenius.perronFrobeniusExistence {ι : 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

Perron-Frobenius existence theorem for strictly positive matrices: there exist a strictly positive scalar r and a strictly positive eigenvector v such that M.mulVec v = r • v. The proof maximises the second coordinate over the Collatz-Wielandt set.