Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: The Theorem of Three Circles

view this post on Zulip Email Gateway (Sep 01 2021 at 12:00):

From: "Thiemann, René" <>
Dear all,

I’m happy to announce a new AFP-entry on polynomial root isolation.

The Theorem of Three Circles
by Fox Thomson and Wenda Li

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.


Last updated: Dec 08 2021 at 08:24 UTC