feat(Analysis/Polynomial): add Sturm's theorem for real polynomials - #42558
feat(Analysis/Polynomial): add Sturm's theorem for real polynomials#42558AMcRoberts wants to merge 3 commits into
Conversation
We introduce Sturm sequences for real polynomials and prove Sturm's theorem: the number of sign variations of the sequence decreases by exactly the number of distinct roots crossed on a half-open interval. The development follows the structure of Manuel Eberl's AFP entry *A Formalisation of Sturm's Theorem* (2014); see the module's own References section.
github-actions
Bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary df3f4a5620Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type (weak) |
|---|---|---|
| 5050 | 1 | exposed public sections |
Current commit df3f4a5620
Reference commit 87adeaebd3
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).
✅ PR Title Formatted CorrectlyThe title of this PR has been updated to match our commit style conventions. |
AMcRoberts
changed the title
…rd_msgs) Three real CI failures found and fixed: - PR title had a capitalized subject; mathlib's title linter requires a lowercase first word. - references.bib's new eberl2014sturm entry was in the wrong alphabetical position (bibtool's canonical sort wants it before Echenique2005, not after EinsiedlerWard2017) and left a stray blank line; applied the exact diff CI's own bibtool check computed. - MathlibTest/Sturm.lean used bare #check without #guard_msgs, so its info-level output was flagged as an unexpected build failure; wrapped each #check with #guard_msgs and the exact expected output.
CertifiedSturmChain packages the algebraic data a Euclidean or pseudo-remainder-sequence construction naturally produces (a positive-scaled recurrence at each step, a nonzero-constant Bezout identity between p and its derivative, and a nonzero-constant terminal element) and proves it satisfies IsSturmSequence, so a concrete PRS chain can drive Sturm's root-count theorem directly. This development was produced independently from the classical sources cited in the module's own References section, without consulting the formalisation cited by the abstract theorem this depends on (leanprover-community#42558).
Two stray blank lines (before Eisenbud1995 and before perfect1969matroid) had crept back in from upstream drift; bibtool's canonical pass removes them again.
|
Hi! Can you clarify if AI was used to help create this PR at all? This will help us to review appropriately. |
2 participants
We introduce Sturm sequences for real polynomials and prove Sturm's theorem:
the number of sign variations of the sequence decreases by exactly the
number of distinct roots crossed on a half-open interval. The development
follows the structure of Manuel Eberl's AFP entry A Formalisation of
Sturm's Theorem (2014); see the module's own
## Referencessection.A follow-up PR adds
CertifiedSturmChain, instantiating this theorem froman exact Euclidean/pseudo-remainder-sequence certificate.