Theorems

Descartes' rule of signs

The number of positive real roots of a polynomial, counted with multiplicity, is at most the number of sign changes in its nonzero coefficients. The difference is even. Replacing $X$ by $-X$ gives the corresponding statement for negative roots.

References

R. Descartes, La Géométrie, 1637. See also the contextual account on symmetricfunctions.com.

Definitions

  • Number of positive roots

    Polynomial.positiveRootCountsource
    noncomputable def positiveRootCount (p : ℝ[X]) : ℕ :=
  p.roots.countP (0 < ·)

  • Number of negative roots

    Polynomial.negativeRootCountsource
    noncomputable def negativeRootCount (p : ℝ[X]) : ℕ :=
  p.roots.countP (· < 0)

Theorems

  • Descartes' rule of signs

    Polynomial.descartes_rule_of_signssource
    theorem descartes_rule_of_signs (p : ℝ[X]) :
    p.positiveRootCount ≤ p.signVariations ∧
      Even (p.signVariations - p.positiveRootCount)

  • Descartes' rule of signs for negative roots

    Polynomial.descartes_rule_of_signs_negativesource
    theorem descartes_rule_of_signs_negative (p : ℝ[X]) :
    p.negativeRootCount ≤ (p.comp (-X)).signVariations ∧
      Even ((p.comp (-X)).signVariations - p.negativeRootCount)

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