Prove real eigenvalues of totally nonnegative matrices are nonnegative - #413
Merged
Conversation
Adds TotallyNonneg/Charpoly.lean: - `IsTotallyNonneg.principalMinor_nonneg`: principal minors of a TN matrix are nonnegative (bridging the Finset-subtype index to the strictly monotone enumeration via `Finset.orderIsoOfFin` and `det_submatrix_equiv_self`); - `IsTotallyNonneg.eval_charpoly_ne_zero_of_neg`: the characteristic polynomial of a TN matrix does not vanish at negative arguments -- by `Matrix.charpoly_coeff_eq_sum_minors` every term of the evaluation at `t < 0` carries the same sign `(-1) ^ card`, with the empty-minor term strictly positive; - `IsTotallyNonneg.nonneg_of_isRoot_charpoly`: **every real eigenvalue of a totally nonnegative matrix is nonnegative**. This is the elementary half of Gantmacher-Krein (#394); realness of the full spectrum additionally needs strict Perron-Frobenius dominance for totally positive matrices, Whitney density, and root continuity (see the issue for the corrected roadmap). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
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.
The elementary half of Gantmacher–Krein (#394), independent of the compound /
Perron–Frobenius machinery.
RealRooted/Mathlib/LinearAlgebra/Matrix/TotallyNonneg/Charpoly.lean:IsTotallyNonneg.principalMinor_nonneg— principal minors of a TN matrix arenonnegative;
IsTotallyNonneg.eval_charpoly_ne_zero_of_neg— the charpoly of a TN matrixcannot vanish at a negative argument: by Mathlib's
charpoly_coeff_eq_sum_minors, every term of the evaluation att < 0carries the same sign
(-1)^card, and the empty-minor term is strictlypositive;
IsTotallyNonneg.nonneg_of_isRoot_charpoly— every real eigenvalue of atotally nonnegative matrix is nonnegative.
Note (recorded on #394): realness of the whole spectrum is genuinely harder —
the eigenvalue multiset
{1, i, −i}passes every "Perron root ofC_qis anattained product" test, so the remaining work needs strict TP dominance,
Whitney density, and root continuity.
Sorry-free.
🤖 Generated with Claude Code