Sturm sequences

This file defines the Sturm sequence (signed remainder sequence) of two polynomials p and q over a field: the list [p, q, -(p % q), …] in which every entry from the third on is the negated remainder of the division of the two previous entries, stopping at the last nonzero remainder. It is the sequence produced by the Euclidean algorithm, up to signs.

For q = derivative p this is the sequence of Sturm's theorem, which counts the distinct real roots of p in an interval as the difference of the numbers of sign variations (List.signVariations) of the sequence evaluated at the endpoints. For q = derivative p * g it is the sequence of the Sturm–Tarski theorem, which computes the sum of the signs of g at the roots of p. This file only contains the algebraic properties of the sequence, which hold over any field.

Main definitions

• Polynomial.sturmSeq p q: the Sturm sequence of p and q, as a list of polynomials.

Main results

• Polynomial.sturmSeq_cons: the unfolding equation sturmSeq p q = p :: sturmSeq q (-p % q) for p ≠ 0.
• Polynomial.sturmSeq_zero_left, Polynomial.sturmSeq_zero_right, Polynomial.sturmSeq_eq_nil_iff: the degenerate cases.
• Polynomial.zero_notMem_sturmSeq: no entry of a Sturm sequence is the zero polynomial.
• Polynomial.dvd_of_mem_sturmSeq: every common divisor of p and q divides every entry of sturmSeq p q.
• Polynomial.sturmSeq_mul_left: sturmSeq (r * p) (r * q) = (sturmSeq p q).map (r * ·) for r ≠ 0.

Implementation notes

The definition is by well-founded recursion on the measure if p = 0 then 0 else if q = 0 then 1 else 2 + q.natDegree. At every step the second argument goes from q to -p % q, which is either 0 or of smaller degree than q; if q = 0 the next call is sturmSeq 0 (-p), which is the base case. The two special values of the measure correspond to these two terminal cases. Proofs about sturmSeq should go through sturmSeq_cons and the functional induction principle sturmSeq.induct and never unfold the definition.

References

• S. Basu, R. Pollack, M.-F. Roy, Algorithms in Real Algebraic Geometry, §2.2.2
• W. Li, The Sturm–Tarski Theorem, Archive of Formal Proofs

@[irreducible]

noncomputable def Polynomial.sturmSeq {K : Type u_1} [Field K] [DecidableEq K] (p q : Polynomial K) : List (Polynomial K)

The Sturm sequence of p and q: the list [p, q, -(p % q), …] of successive negated remainders, ending at the last nonzero one.

Equations

• p.sturmSeq q = if p = 0 then [] else p :: q.sturmSeq (-p % q)

@[simp]

theorem Polynomial.sturmSeq_zero_left {K : Type u_1} [Field K] [DecidableEq K] (q : Polynomial K) : sturmSeq 0 q = []

The Sturm sequence of 0 and q is the empty sequence.

theorem Polynomial.sturmSeq_cons {K : Type u_1} [Field K] [DecidableEq K] {p q : Polynomial K} (hp : p ≠ 0) : p.sturmSeq q = p :: q.sturmSeq (-p % q)

If p is not 0, the Sturm sequence of p and q is p followed by the Sturm sequence of q and -p % q.

@[simp]

theorem Polynomial.sturmSeq_eq_nil_iff {K : Type u_1} [Field K] [DecidableEq K] {p q : Polynomial K} : p.sturmSeq q = [] ↔ p = 0

@[simp]

theorem Polynomial.sturmSeq_zero_right {K : Type u_1} [Field K] [DecidableEq K] (p : Polynomial K) : p.sturmSeq 0 = if p = 0 then [] else [p]

theorem Polynomial.mem_sturmSeq_self {K : Type u_1} [Field K] [DecidableEq K] {p q : Polynomial K} (hp : p ≠ 0) : p ∈ p.sturmSeq q

theorem Polynomial.zero_notMem_sturmSeq {K : Type u_1} [Field K] [DecidableEq K] (p q : Polynomial K) : 0 ∉ p.sturmSeq q

theorem Polynomial.ne_zero_of_mem_sturmSeq {K : Type u_1} [Field K] [DecidableEq K] {p q s : Polynomial K} (hs : s ∈ p.sturmSeq q) : s ≠ 0

@[simp]

theorem Polynomial.head?_sturmSeq {K : Type u_1} [Field K] [DecidableEq K] {p q : Polynomial K} (hp : p ≠ 0) : (p.sturmSeq q).head? = some p

The first entry of the Sturm sequence of a nonzero polynomial is the polynomial itself.

theorem Polynomial.dvd_of_mem_sturmSeq {K : Type u_1} [Field K] [DecidableEq K] {d p q s : Polynomial K} (hp : d ∣ p) (hq : d ∣ q) (hs : s ∈ p.sturmSeq q) : d ∣ s

Every common divisor of p and q divides every entry of their Sturm sequence. In particular this holds for gcd p q.

theorem Polynomial.sturmSeq_mul_left {K : Type u_1} [Field K] [DecidableEq K] {r : Polynomial K} (hr : r ≠ 0) (p q : Polynomial K) : (r * p).sturmSeq (r * q) = List.map (fun (x : Polynomial K) => r * x) (p.sturmSeq q)

Multiplying both arguments by a nonzero polynomial multiplies every entry of the Sturm sequence by it.