Sturm's theorem

DefinitionNegated-remainder sequence with fuel#✓fully proved

For real polynomials \(a\), \(b\) and a natural number \(n\), this is the list of polynomials defined recursively by: for \(n = 0\) it is the one-entry list \((a)\); for fuel \(n + 1\) it is \((a)\) if \(b = 0\), and otherwise it is \(a\) followed by the list for the pair \(b\), \(-(a \bmod b)\) with fuel \(n\), where \(a \bmod b\) is the remainder of \(a\) on division by \(b\).

noncomputable def sturmAux : ℝ[X] → ℝ[X] → ℕ → List ℝ[X]
  | a, _, 0       => [a]
  | a, b, (n + 1) =>
    if b = 0 then [a] else a :: sturmAux b (-(a % b)) n

Used by 1

Used bySturm chain

DefinitionSturm chain#✓fully proved

The Sturm chain of a real polynomial \(p\) is the list \(p_0, p_1, \dots, p_m\) with \(p_0 = p\), \(p_1 = p'\) and \(p_{k+1} = -(p_{k-1} \bmod p_k)\), the negated remainder of \(p_{k-1}\) on division by \(p_k\), where the list stops at \(p_m\) as soon as the next entry would be \(0\); thus \(p_m\) is its last entry and, for \(p \ne 0\), every entry is nonzero. For \(p = 0\) the chain is the one-entry list \((0)\).

noncomputable def sturmChain (p : ℝ[X]) : List ℝ[X] :=
  sturmAux p (derivative p) (p.natDegree + 2)

noncomputable def sturmAux : ℝ[X] → ℝ[X] → ℕ → List ℝ[X]
  | a, _, 0       => [a]
  | a, b, (n + 1) =>
    if b = 0 then [a] else a :: sturmAux b (-(a % b)) n

WantedExt/Algebra/SturmWanted.lean:69

Uses 1 · Used by 1

Statement usesNegated-remainder sequence with fuel

Used bySturm sign-variation function

DefinitionNumber of sign changes in a list of reals#✓fully proved

For a list \(x_1, \dots, x_n\) of real numbers, let \(y_1, \dots, y_m\) be the entries of the list that are nonzero, in their original order. The number of sign changes of the list is the number of indices \(i\) with \(1 \le i < m\) and \(y_i y_{i+1} < 0\), that is, the number of adjacent pairs of opposite sign once the zeros are removed.

noncomputable def signChanges (xs : List ℝ) : ℕ :=
  let ys := xs.filter (· ≠ 0)
  ((ys.zip ys.tail).filter (fun q => q.1 * q.2 < 0)).length

Used by 1

Used bySturm sign-variation function

DefinitionSturm sign-variation function#✓fully proved

For a real polynomial \(p\) with Sturm chain \(p_0, p_1, \dots, p_m\) and a real number \(x\), \(\sigma_p(x)\) is the number of sign changes, ignoring zeros, in the sequence of values \(p_0(x), p_1(x), \dots, p_m(x)\).

noncomputable def sigma (p : ℝ[X]) (x : ℝ) : ℕ :=
  signChanges ((sturmChain p).map fun q => q.eval x)

noncomputable def signChanges (xs : List ℝ) : ℕ :=
  let ys := xs.filter (· ≠ 0)
  ((ys.zip ys.tail).filter (fun q => q.1 * q.2 < 0)).length

WantedExt/Algebra/SturmWanted.lean:82

noncomputable def sturmChain (p : ℝ[X]) : List ℝ[X] :=
  sturmAux p (derivative p) (p.natDegree + 2)

WantedExt/Algebra/SturmWanted.lean:77

Uses 2 · Used by 1

Statement usesNumber of sign changes in a list of reals · Sturm chain

Used bySturm's theorem

TheoremSturm's theorem#●ready to prove

Let \(p\) be a squarefree real polynomial and let \(a < b\) be real numbers with \(p(a) \ne 0\) and \(p(b) \ne 0\). Then the number of distinct real roots \(x\) of \(p\) with \(a < x < b\) equals \(\sigma_p(a) - \sigma_p(b)\), where \(\sigma_p\) is the Sturm sign-variation function of \(p\) and the subtraction is truncated subtraction of natural numbers.

public theorem_wanted sturm (p : ℝ[X]) (hp : Squarefree p) {a b : ℝ} (hab : a < b)
    (ha : p.eval a ≠ 0) (hb : p.eval b ≠ 0) :
    ((p.roots.toFinset).filter (fun x => a < x ∧ x < b)).card =
      sigma p a - sigma p b

Sources

J. C. F. Sturm (1829). Listed as §97 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Formalized in Isabelle/HOL by Manuel Eberl (AFP entry Sturm_Sequences). Problem sturm of the lean-eval benchmark.

Uses 1

Statement usesSturm sign-variation function

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.