Descartes' Rule of Signs

Manuel Eberl 🌐

December 28, 2015

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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.

License

BSD License

Topics

Session Descartes_Sign_Rule