[Merged by Bors] - feat(LinearAlgebra/RootSystem/Finite): Coxeter weights are bounded above by 4#19343
[Merged by Bors] - feat(LinearAlgebra/RootSystem/Finite): Coxeter weights are bounded above by 4#19343ScottCarnahan wants to merge 10 commits intomasterfrom
Conversation
PR summary fa0c7e1036
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear | 1380 | 1381 | +1 (+0.07%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear |
1 |
Declarations diff
+ apply_mul_apply_le_of_forall_zero_le
+ apply_mul_apply_lt_iff_linearIndependent
+ apply_smul_sub_smul_sub_eq
+ apply_sq_le_of_symm
+ apply_sq_lt_iff_linearIndependent_of_symm
+ coxeterWeight_le_four
+ coxeterWeight_mem_set_of_isCrystallographic
+ coxeterWeight_ne_four_of_linearIndependent
+ exists_int_eq_coxeterWeight
+ four_smul_rootForm_sq_eq_coxeterWeight_smul
+ infinite_of_linearIndependent_coxeterWeight_four
+ instIsRootPositiveRootForm
+ not_linearIndependent_of_apply_mul_apply_eq
+ toPerfectPairing_apply_CoPolarization
+ toPerfectPairing_apply_apply_Polarization
- infinite_of_linearly_independent_coxeterWeight_four
- rootForm_rootPositive
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
|
This looks great! I’m still travelling (with phone-only internet access) so I can’t review until Tuesday, but I’ll prioritise this then if it’s still pending. |
ocfnash
left a comment
There was a problem hiding this comment.
Just two quick comments for now; will return this evening.
ocfnash
left a comment
There was a problem hiding this comment.
I had a few moments over lunch.
|
Thanks for the suggestions! I hadn't noticed that positive-definiteness on the root span was not used. |
ocfnash
left a comment
There was a problem hiding this comment.
Another round of mostly nitpicks!
ocfnash
left a comment
There was a problem hiding this comment.
One last round of small suggestions. Thanks for going the extra mile with Cauchy-Schwarz!
bors d+
|
✌️ ScottCarnahan can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
…ove by 4 (#19343) This PR adds a version of the Cauchy-Schwarz inequality for positive semidefinite bilinear forms on modules over linearly ordered commutative rings, and applies it to restrict Coxeter weights for root systems. Co-authored-by: Oliver Nash <github@olivernash.org>
|
Pull request successfully merged into master. Build succeeded: |
This PR adds a version of the Cauchy-Schwarz inequality for positive semidefinite bilinear forms on modules over linearly ordered commutative rings, and applies it to restrict Coxeter weights for root systems.