Sturm's Theorem

 

Title: Sturm's Theorem
Author: Manuel Eberl
Submission date: 2014-01-11
Abstract: Sturm's Theorem states that polynomial sequences with certain properties, so-called Sturm sequences, can be used to count the number of real roots of a real polynomial. This work contains a proof of Sturm's Theorem and code for constructing Sturm sequences efficiently. It also provides the “sturm” proof method, which can decide certain statements about the roots of real polynomials, such as “the polynomial P has exactly n roots in the interval I” or “P(x) > Q(x) for all x ∈ ℝ”.
BibTeX:
@article{Sturm_Sequences-AFP,
  author  = {Manuel Eberl},
  title   = {Sturm's Theorem},
  journal = {Archive of Formal Proofs},
  month   = jan,
  year    = 2014,
  note    = {\url{http://isa-afp.org/entries/Sturm_Sequences.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Used by: Algebraic_Numbers, Perron_Frobenius, Safe_Distance, Special_Function_Bounds
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.