feat(PerronFrobenius): Perron–Frobenius for irreducible matrices

[mkaratarakis]

Add Mathlib/LinearAlgebra/Matrix/PerronFrobenius/Irreducible.lean: existence and uniqueness of the Perron eigenpair for irreducible non-negative matrices.

Part of the Perron–Frobenius formalization (with @or4nge19).

---

---

• depends on: feat(PerronFrobenius): core lemmas for non-negative matrices #39918
• depends on: feat(PerronFrobenius): uniqueness of the Perron eigenvector #39921

cc @or4nge19 for review

[github-actions]

PR summary 751dff5ba0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.Matrix.PerronFrobenius.Irreducible (new file)	805

---

Declarations diff

+ Irreducible.add_one
+ Irreducible.exists_pos_entry
+ eigenvector_is_positive_of_irreducible
+ eigenvector_no_zero_entries_of_irreducible
+ exists_positive_eigenvector_of_irreducible
+ pft_irreducible
+ pft_primitive
+ uniqueness_of_positive_eigenvector_gen

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(PerronFrobenius): core lemmas for non-negative matrices #39918
• feat(PerronFrobenius): uniqueness of the Perron eigenvector #39921
  By Dependent Issues (🤖). Happy coding!