The Theorem of Three Circles

Fox Thomson šŸ“§ and Wenda Li šŸŒ

August 21, 2021

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

The Descartes test based on Bernstein coefficients and Descartesā€™ rule of signs effectively (over-)approximates the number of real roots of a univariate polynomial over an interval. In this entry we formalise the theorem of three circles, which gives sufficient conditions for when the Descartes test returns 0 or 1. This is the first step for efficient root isolation.

License

BSD License

Topics

Session Three_Circles

Depends on

Cite

× 
@article{Three_Circles-AFP,
  author  = {Fox Thomson and Wenda Li},
  title   = {The Theorem of Three Circles},
  journal = {Archive of Formal Proofs},
  month   = {August},
  year    = {2021},
  note    = {\url{https://isa-afp.org/entries/Three_Circles.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: