EconCSLib.Math.LinearAlgebra.PerronFrobenius

Formalises Perron-Frobenius for strictly positive square matrices [MFoGT, Section 2.8, Exercise 1(2)] over ℝ as an application of the general-B Loomis theorem.

For any M : Fin n → Fin n → ℝ with M i j > 0 for every i, j, there exist x, y ∈ Δ(Fin n) and λ > 0 such that

• x and y have strictly positive components;
• x M = λ · x (so x is a left eigenvector at eigenvalue λ);
• M y = λ · y (so y is a right eigenvector at the same λ).

λ = 1/v where v is the Loomis value of (I, M) (identity vs. M).

Proof strategy (per blueprint)

Apply Loomis.loomis_theorem with A := I (identity) and B := M. Loomis produces (x, y, v) with v · (xM)_j ≤ x_j and y_i ≤ v · (My)_i.

1. v > 0: from any y i₀ > 0 (some such i₀ exists since ∑ y i = 1), combine with (My)_{i₀} > 0 (since M > 0 and y ≥ 0 with full support… wait, just need (My)_i > 0).
2. x > 0 strictly: x_j ≥ v · (xM)_j > 0.
3. Tight inner product: ⟨x, y⟩ = v · ⟨x, My⟩ (sandwich is tight).
4. y > 0 strictly: from tightness on (2) weighted by x > 0, every y_i = v · (My)_i > 0.
5. Eigenvector: with y > 0 strict, tightness on (1) gives x_j = v · (xM)_j for all j, i.e., xM = (1/v) · x.

Blueprint

• docs/knowledge/nodes/zero_sum/perron_frobenius_positive_matrix.md

Identity matrix and its wsum

Perron-Frobenius theorem

theorem EconCSLib.LinearAlgebra.perron_frobenius {n : ℕ} [NeZero n] (M : Fin n → Fin n → ℝ) (hM_pos : ∀ (i j : Fin n), 0 < M i j) : ∃ (x : ↑(stdSimplex ℝ (Fin n))) (y : ↑(stdSimplex ℝ (Fin n))) (lam : ℝ), 0 < lam ∧ (∀ (i : Fin n), 0 < ↑x i) ∧ (∀ (i : Fin n), 0 < ↑y i) ∧ (∀ (j : Fin n), (wsum x fun (i : Fin n) => M i j) = lam * ↑x j) ∧ ∀ (i : Fin n), wsum y (M i) = lam * ↑y i

Perron-Frobenius for positive matrices [MFoGT, Section 2.8, Exercise 1(2)]. A square matrix with strictly positive entries has a strictly positive eigenvalue λ > 0 with both a strictly positive left eigenvector x and a strictly positive right eigenvector y (each a probability distribution on Fin n).