
The
BudanFourier
Theorem
and
Counting
Real
Roots
with
Multiplicity
Title: 
The BudanFourier Theorem and Counting Real Roots with Multiplicity 
Author:

Wenda Li

Submission date: 
20180902 
Abstract: 
This entry is mainly about counting and approximating real roots (of a
polynomial) with multiplicity. We have first formalised the
BudanFourier theorem: given a polynomial with real coefficients, we
can calculate sign variations on Fourier sequences to overapproximate
the number of real roots (counting multiplicity) within an interval.
When all roots are known to be real, the overapproximation becomes
tight: we can utilise this theorem to count real roots exactly. It is
also worth noting that Descartes' rule of sign is a direct
consequence of the BudanFourier theorem, and has been included in
this entry. In addition, we have extended previous formalised
Sturm's theorem to count real roots with multiplicity, while the
original Sturm's theorem only counts distinct real roots.
Compared to the BudanFourier theorem, our extended Sturm's
theorem always counts roots exactly but may suffer from greater
computational cost. 
BibTeX: 
@article{Budan_FourierAFP,
author = {Wenda Li},
title = {The BudanFourier Theorem and Counting Real Roots with Multiplicity},
journal = {Archive of Formal Proofs},
month = sep,
year = 2018,
note = {\url{https://isaafp.org/entries/Budan_Fourier.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
Sturm_Tarski 
Used by: 
Three_Circles, Winding_Number_Eval 
Status: [ok] 
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.

