feat(PerronFrobenius): Collatz–Wielandt function and Perron root bounds

[mkaratarakis]

Add Mathlib/LinearAlgebra/Matrix/PerronFrobenius/CollatzWielandt.lean: the Collatz–Wielandt formula, alternative Perron-root characterizations, upper semicontinuity on the standard simplex, and maximizer existence via UpperSemicontinuousOn.exists_isMaxOn.

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

---

---

• depends on: feat(PerronFrobenius): core lemmas for non-negative matrices #39918
• depends on: feat(PerronFrobenius): auxiliary matrix and topology lemmas #39917

cc @or4nge19 for review

[github-actions]

PR summary 4cbc90324d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.Matrix.PerronFrobenius.CollatzWielandt (new file)	1494

---

Declarations diff

+ P_set
+ bddAbove
+ bddAbove_image_P_set
+ collatzWielandtFn
+ csSup_nonneg
+ dotProduct_mulVec_eq_eigenvalue_mul_dotProduct
+ eigenvalue_is_ub_of_positive_eigenvector
+ eigenvalue_le_perron_root_of_positive_eigenvector
+ eq_eigenvalue_of_positive_eigenvector
+ eq_iInf_of_nonempty
+ eq_perron_root_of_positive_eigenvector
+ exists_maximizer
+ exists_mulVec_eq_zero_on_support_of_nonpos
+ forall_exists_min_le_max
+ le_any_ratio
+ le_eigenvalue_of_left_eigenvector
+ le_eigenvalue_of_right_eigenvector
+ le_mulVec
+ le_of_max_le_row_sum
+ le_of_subinvariant
+ le_ratio
+ left_eigenvector_of_transpose
+ maxRatio
+ maximizer_satisfies_le_mulVec
+ minRatio
+ minRatio_le_maxRatio
+ min_max_sets_nonempty
+ mulVec_continuousLinearMap
+ mulVec_eq_smul_of_eigenvector
+ ones_eigenvector_of_similarity_transform
+ perronRoot
+ perronRoot'
+ perronRoot'_le_maxRatio_of_min_ge_perronRoot'
+ perronRoot_alt
+ perronRoot_nonneg
+ perron_root_le_eigenvalue_of_left_eigenvector
+ r
+ r_x
+ r_x_continuousOn_pos
+ row_sum_of_similarity_transformed_matrix
+ set_nonempty
+ smul
+ upperSemicontinuousOn
+ val_eq_zero_of_nonpos

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): auxiliary matrix and topology lemmas #39917
  By Dependent Issues (🤖). Happy coding!