Port the MCMC Perron-Frobenius development - #412
Merged
Conversation
Ports the Perron-Frobenius formalization from or4nge19/MCMC (MCMC/PF, commit dba8102f, Apache-2.0, author Matteo Cipollina) into RealRooted/Mathlib/LinearAlgebra/Matrix/PerronFrobenius/, adapted to the pinned Mathlib (the original targeted a 2026-01 Mathlib; ours is 2026-06). Twelve files, ~6100 lines, sorry-free: DataList, QuiverPath, Spectrum, ExtremeValueUSC, CStarClasses, Auxiliary, Lemmas, CollatzWielandt, Primitive, Uniqueness, Irreducible, Dominance. Key theorems now available (issue #404): - `Matrix.pft_irreducible`: an irreducible nonnegative real matrix has a unique stdSimplex-normalized eigenvector, with positive eigenvalue; - `Matrix.perron_root_is_eigenvalue`: the Perron root of an irreducible nonnegative matrix is an eigenvalue; - `Matrix.eigenvalue_abs_le_perron_root`: every complex eigenvalue has modulus at most the Perron root; - the Collatz-Wielandt variational theory backing them. Adaptations for five months of Mathlib drift: - `Matrix.toQuiver` arrows became `PLift (0 < A i j)`: inserted `.down` / `⟨_⟩` at eight use sites; - `List.dropLast_cons_cons` upstreamed: dropped the local copy; - `stdSimplex` argument order: `isCompact_stdSimplex ℝ n`; - `inferInstanceAs (Nonempty n)` under postponed elaboration: replaced by anonymous-hypothesis syntax; - `Path.end` is now definitional: replaced dead `simpa`s by `exact`/`rfl` terms and repaired one `subst`-sensitive case split; - deprecated import `Data.Real.StarOrdered` -> `Algebra.Order.Star.Real`; - dropped two upstream-`sorry`d `spectralRadius` bridge theorems in Dominance (not needed by Gantmacher-Krein, which uses `perronRoot` directly) and one unused upstream-`sorry`d Quiver lemma; - `Aux.lean` renamed `Auxiliary.lean` (reserved file name). Ported files keep their original line layout (`set_option linter.style.longLine false`). Remaining for #404 / #394: the general (reducible) nonnegative case via the `A + eps J` limit, in a follow-up file. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Adds PerronFrobenius/Nonneg.lean, removing the irreducibility hypothesis -- the form Gantmacher-Krein (#394) needs, since compounds of totally nonnegative matrices are entrywise nonnegative but not irreducible. - `isIrreducible_of_pos`: an entrywise positive matrix is irreducible (single-edge paths in the positivity quiver); - `perronRoot_le_perronRoot_of_le`: entrywise matrix monotonicity of the Perron root, via `le_mulVec` -> `le_of_subinvariant` -> `collatzWielandtFn_le_perronRoot`; - `norm_le_perronRoot_of_eigenvalue`: every complex eigenvalue of a nonnegative real matrix has modulus at most the Perron root, with no irreducibility -- the ported subinvariance inequalities (`eigenvalue_abs_subinvariant`, `le_of_subinvariant`) never needed it; - `exists_nonneg_mulVec_eq_perronRoot_smul`: **the general theorem** -- a nonnegative matrix attains its Perron root as an eigenvalue with a nonnegative eigenvector. Proof: perturb to `A + ((k:R)+1)^-1 * J` (positive, hence irreducible), apply `perron_root_eq_positive_eigenvalue`, normalize eigenvectors to the standard simplex, extract a convergent subsequence in the compact set `Icc (perronRoot A) M x stdSimplex` and pass to the limit; the limit eigenvalue is squeezed to `perronRoot A` by matrix monotonicity from below and subinvariance from above. Together with the port this completes the mathematical content of #404. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
PerAlexandersson
commented
Aug 21, 2026
OwnerAuthor
Added |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for freeto join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The core of #404. Ports the Perron–Frobenius formalization from
or4nge19/MCMC (
MCMC/PF, commitdba8102f,Apache-2.0, author Matteo Cipollina) into
RealRooted/Mathlib/LinearAlgebra/Matrix/PerronFrobenius/, adapted to ourpinned Mathlib — twelve files, ~6100 lines, sorry-free.
Key theorems now available:
Matrix.pft_irreducible— unique normalized positive eigenvector with positive eigenvalue;Matrix.perron_root_is_eigenvalue— the Perron root of an irreducible nonnegative matrix is an eigenvalue;Matrix.eigenvalue_abs_le_perron_root— every complex eigenvalue has modulus ≤ the Perron root;Five months of Mathlib drift handled (details in the commit message):
toQuiverarrows became
PLift,stdSimplexargument order,Path.endnow definitional,one upstreamed list lemma, a reserved filename, a deprecated import. The two
upstream-
sorrydspectralRadiusbridge lemmas are omitted — Gantmacher–Krein(#394) works with
perronRootdirectly.Remaining for #404: the general (reducible) nonnegative case via the
A + εJlimit — follow-up file.
Full
RealRootedbuilds clean on top of this (9017 jobs).🤖 Generated with Claude Code