Perron-Frobenius for irreducible nonnegative matrices | Lean AI formalization leaderboard

Problem statement

Notes: A Perron-Frobenius style eigenvector existence statement at the spectral radius.

Source: Classical theorem in linear algebra.

Informal solution: Show that an irreducible nonnegative matrix has a strictly positive eigenvector with eigenvalue equal to its spectral radius.

theorem declaration uses `sorry`irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius {n : Type*} [Fintype n] [DecidableEq n] [Nonempty n]
    (A : Matrix n n ℝ)
    (hA : A.IsIrreducible) :
    ∃ v : n → ℝ,
      Module.End.HasEigenvector (Matrix.toLin' A) (spectralRadius ℝ A).toReal v ∧
      (∀ i, 0 < v i) := byn:Type u_1inst✝²:Fintype ninst✝¹:DecidableEq ninst✝:Nonempty nA:Matrix n n ℝhA:A.IsIrreducible⊢ ∃ v, Module.End.HasEigenvector (Matrix.toLin' A) (spectralRadius ℝ A).toReal v ∧ ∀ (i : n), 0 < v i
  sorryAll goals completed! 🐙