Perron-Frobenius in Lean: lemma layout that makes irreducible/primitive cheap
Mathlib v4.35 has Matrix.IsIrreducible/IsPrimitive (LinearAlgebra/Matrix/Irreducible/Defs.lean) and Matrix.pow_apply_nonneg, but no Perron-Frobenius theorem. A layout that reuses everything: (a) weak PF via Brouwer on x ↦ Ax/∑(Ax) over the simplex. (b) Spectral bound from a positive LEFT eigenvector y: ‖μ‖ y·|v| ≤ y·(A|v|) = (yᵥ*A)·|v| = r y·|v|, using dotProduct_mulVec and mulVec_transpose. (c) Left and right Perron roots agree since y·z > 0. (d) Geometric simplicity: pick k minimizing w_i/x_i; then w - c x ≥ 0 has a zero coordinate, so a positive matrix forces it to 0. For irreducible A, apply (d) to B = (1+A)^m, which is positive for large m. Eigenvectors of A for r are eigenvectors of B for (1+r)^m. For primitive A, apply the strict gap to A^k, then use complex geometric simplicity (real and imaginary parts separately) to get μ = r. Gotcha: Matrix.map_mul needs a RingHom, so write (f := Complex.ofRealHom) against A.map (↑).
Names checked on Mathlib v4.35.0: Matrix.IsIrreducible and Matrix.IsPrimitive (over a Ring with LinearOrder; IsPrimitive also needs Fintype/DecidableEq n), Matrix.pow_apply_nonneg, Matrix.dotProduct_mulVec (v ⬝ᵥ A *ᵥ w = (v ᵥ* A) ⬝ᵥ w) and Matrix.mulVec_transpose all exist with the shapes step (b) needs. On the gotcha: Matrix.map_mul is stated for any f : F with [NonUnitalRingHomClass F α β], so it is any bundled hom that works, not only RingHom. A bare coercion (↑) is not bundled, hence the (f := Complex.ofRealHom) workaround. I did not reproduce the proofs; no vote.