Prove Gantmacher-Krein for matrices with primitive compounds - #414
Merged
Conversation
The triangular half of the compound eigenvalue theorem (issue #405 item 3): - `BlockTriangular.det_of_injective`, `BlockTriangular.charpoly_of_injective`: a block triangular matrix with an injective block map has determinant and characteristic polynomial given by its diagonal (generalizes `Matrix.det_of_upperTriangular` to indices without a linear order); - `compound_apply_eq_zero_of_blockTriangular`: minors of an upper triangular matrix vanish unless the row selection is pointwise dominated by the column selection (permutation expansion plus a pigeonhole step); - `powersetCode`: the binary encoding of a selection, injective via Mathlib's colex `Finset.geomSum_injective`, monotone for pointwise domination; - `blockTriangular_compound`, `compound_apply_self_of_blockTriangular`, `charpoly_compound_of_blockTriangular`: the compound of a triangular matrix is triangular for the binary encoding, with diagonal the selected products, so its charpoly is `∏_s (X - C ∏_{i ∈ s} T i i)`; - `compound_one`, `charpoly_compound_conj`: the compound charpoly is invariant under conjugation, by multiplicativity. What remains for the full eigenvalue statement is matrix-level triangularization over an algebraically closed field, which Mathlib lacks. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Closes the mathematical content of issue #405: over an algebraically closed field there is an enumeration mu of the eigenvalues of A (with multiplicity) such that for every q the characteristic polynomial of `compound q A` is `prod_s (X - C (prod_{i in s} mu i))` over the increasing q-selections. Pure assembly of the two merged halves plus one new ingredient: - triangularize A (`exists_unitsConj_blockTriangular`, #410); - sort the height function of the triangular form into the index order by a permutation-matrix conjugation (`Tuple.sort` + `permMatrixHom.toHomUnits` + `PEquiv.toMatrix_toPEquiv_mul` / `PEquiv.mul_toMatrix_toPEquiv`); - read off the compound charpoly of the sorted triangular form (`charpoly_compound_of_blockTriangular`), transporting along both conjugations with `charpoly_compound_conj` and `charpoly_units_conj`. This is the spectral input Gantmacher-Krein (#394) consumes: TN matrices have entrywise nonnegative compounds, so Perron-Frobenius (#404) on each compound controls the eigenvalue products. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
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>
Adds RealRooted/Mathlib/LinearAlgebra/Matrix/GantmacherKrein.lean, the density-free case of Gantmacher-Krein: `exists_charpoly_eq_prod_of_forall_compound_primitive`: if every compound `compound q A` (1 <= q <= n) of a real matrix `A` is primitive, then `A.charpoly = prod_i (X - C (mu i))` with all `mu i > 0`. This covers the oscillatory case. The argument needs no tie analysis: sort a complex eigenvalue enumeration (from `exists_charpoly_compound_eq_prod`) by descending modulus; for each q the Perron root of `compound q A` is an attained selection product (general PF, `mem_spectrum_iff_isRoot_charpoly`), and by strict spectral dominance for primitive matrices (`spectral_dominance_of_primitive'`) the top product must equal it -- else its modulus would be simultaneously strictly below and at least the Perron root. Hence every partial product mu_1 ... mu_q equals the q-th Perron root, and mu_q is the quotient of consecutive Perron roots, real and positive. Injectivity of `Polynomial.map` along `algebraMap R C` brings the factorization back to the reals. Supporting lemmas: `compound_map` (compounds commute with entrywise ring homomorphisms), `prod_powersetEnum` (selection products as finite-set products), `prod_powersetCard_comp_perm` (permutation invariance of the compound factorization), and the `topFinset` initial-segment kit. The general totally nonnegative case additionally needs Whitney density and root continuity (see #394 for the corrected roadmap). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
- `compound_pow`: compounds commute with matrix powers; - `isPrimitive_compound_of_pow`: a totally nonnegative matrix, some power of which has strictly positive compound entries (the oscillatory situation), has all compounds primitive; - `exists_charpoly_eq_prod_of_pow_compound_pos`: oscillatory matrices have real positive spectrum; - `charpoly_splits_of_forall_compound_primitive`: the splitting form -- `A.charpoly.Splits` with all roots strictly positive. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Owner
Author
|
Added the oscillatory bridge on the same branch: |
This was referenced Aug 22, 2026
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 free
to 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.
Stacked on #411 and #412 (this branch merges both; review the last commit —
GantmacherKrein.lean— the rest lands with those PRs).exists_charpoly_eq_prod_of_forall_compound_primitive: if every compoundcompound q Aof a real matrix is primitive, then∃ μ : Fin n → ℝ, (∀ i, 0 < μ i) ∧ A.charpoly = ∏ i, (X - C (μ i))— the characteristic polynomial splits over ℝ with strictly positive roots.
This is the oscillatory case of Gantmacher–Krein, proved without Whitney
density or root continuity: strict spectral dominance for primitive matrices
forces the sorted top-
qeigenvalue product to equal the Perron root of theq-th compound (otherwise its modulus is simultaneously< ρ_qand≥ ρ_q),so every
μ_q = ρ_q/ρ_{q−1}is real positive. The tie obstruction that blocksthe naive argument for general TN matrices (see #394: the multiset
{1, i, −i})never arises.
Chain consumed: #411 (
exists_charpoly_compound_eq_prod) + #412(
exists_nonneg_mulVec_eq_perronRoot_smul,spectral_dominance_of_primitive',perronRoot_pos_of_irreducible).Supporting lemmas:
compound_map,prod_powersetEnum,prod_powersetCard_comp_perm, and atopFinsetinitial-segment kit.Sorry-free; full library builds (9020 jobs).
🤖 Generated with Claude Code