feat(PerronFrobenius): Perron–Frobenius for primitive matrices

[mkaratarakis]

Add Mathlib/LinearAlgebra/Matrix/PerronFrobenius/Primitive.lean: a Collatz–Wielandt maximizer is a Perron eigenvector, and existence of the Perron eigenpair for primitive matrices.

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

---

---

• depends on: feat(PerronFrobenius): Collatz–Wielandt function and Perron root bounds #39919

cc @or4nge19 for review

[github-actions]

PR summary e48b577891

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.Matrix.PerronFrobenius.Primitive (new file)	2802

---

Declarations diff

+ collatzWielandtFn_of_ones_is_pos
+ collatzWielandt_sup_is_pos
+ eigenvector_of_primitive_is_positive
+ exists_positive_eigenvector_of_primitive
+ max_is_eig
+ maximizer_is_eigenvector
+ perron_root_pos_of_primitive
+ ratio_le_max_row_sum_simple

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): Collatz–Wielandt function and Perron root bounds #39919
  By Dependent Issues (🤖). Happy coding!