Theorems

Sturm root counting

Evaluate the signed Euclidean remainder sequence of a polynomial and its derivative at the two endpoints of an interval, omit zero values, and count sign changes. The drop in sign changes is exactly the number of distinct real roots in the open interval.

Repeated factors are removed by a canonical squarefree normalization. If the interval contains every root, the same count tests whether all roots are real.

References

J. C. F. Sturm, “Mémoire sur la résolution des équations numériques,” Bulletin des Sciences de Férussac 11 (1829), 419–422. See also the root-counting overview on symmetricfunctions.com.

Definitions

  • Signed remainder sequence

    Polynomial.signedRemainderSequencesource
    def signedRemainderSequence (p q : K[X]) : List K[X] :=
  if _hq : q = 0 then [p]
  else p :: signedRemainderSequence q (-(p % q))
termination_by q.degree
decreasing_by
  simpa only [degree_neg] using degree_mod_lt p _hq

  • Sign variations of the Sturm sequence

    RealRooted.sturmVariationssource
    def sturmVariations (p : ℝ[X]) (x : ℝ) : ℕ :=
  (sturmValues p x).signVariations

  • Number of distinct roots in an interval

    RealRooted.distinctRootCountIoosource
    def distinctRootCountIoo (p : ℝ[X]) (a b : ℝ) : ℕ :=
  (p.roots.toFinset.filter fun r ↦ a < r ∧ r < b).card

Theorems

  • Sturm's theorem

    RealRooted.distinctRootCountIoo_eq_distinctSturmVariations_subsource
    theorem distinctRootCountIoo_eq_distinctSturmVariations_sub
    {p : ℝ[X]} (hp : p ≠ 0) {a b : ℝ} (hab : a < b)
    (ha : ¬ p.IsRoot a) (hb : ¬ p.IsRoot b) :
    distinctRootCountIoo p a b =
      distinctSturmVariations p a - distinctSturmVariations p b

  • A Sturm test for real-rootedness

    RealRooted.splits_iff_distinctSturmVariations_sub_eq_natDegreesource
    theorem splits_iff_distinctSturmVariations_sub_eq_natDegree
    {p : ℝ[X]} (hp : p ≠ 0) {a b : ℝ} (hab : a < b)
    (hbound : ∀ r : ℝ, p.IsRoot r → a < r ∧ r < b) :
    p.Splits ↔
      distinctSturmVariations p a - distinctSturmVariations p b =
        (sturmSquarefreePart p).natDegree

Lean source RealRooted/Challenges/Sturm.lean at revision 5827550b.