### 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 ∈ ℝ”.

### License

BSD License

### Topics

- Mathematics/Analysis

### Session Sturm_Sequences

- Sturm_Library_Document
- Misc_Polynomial
- Sturm_Library
- Sturm_Theorem
- Sturm_Method
- Sturm
- Sturm_Ex

### Used by

- A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles
- Perron-Frobenius Theorem for Spectral Radius Analysis
- Algebraic Numbers in Isabelle/HOL
- Real-Valued Special Functions: Upper and Lower Bounds

## Cite

×

Sturm_Sequences-AFP

    @article{Sturm_Sequences-AFP,
      author  = {Manuel Eberl},
      title   = {Sturm's Theorem},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/Sturm_Sequences.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Jan 12, 2014 : Isabelle2013-2