Descartes' Rule of Signs

 

Title: Descartes' Rule of Signs
Author: Manuel Eberl
Submission date: 2015-12-28
Abstract:

Descartes' Rule of Signs relates the number of positive real roots of a polynomial with the number of sign changes in its coefficient sequence.

Our proof follows the simple inductive proof given by Rob Arthan, which was also used by John Harrison in his HOL Light formalisation. We proved most of the lemmas for arbitrary linearly-ordered integrity domains (e.g. integers, rationals, reals); the main result, however, requires the intermediate value theorem and was therefore only proven for real polynomials.

BibTeX:
@article{Descartes_Sign_Rule-AFP,
  author  = {Manuel Eberl},
  title   = {Descartes' Rule of Signs},
  journal = {Archive of Formal Proofs},
  month   = dec,
  year    = 2015,
  note    = {\url{http://isa-afp.org/entries/Descartes_Sign_Rule.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License