Entries of a Sturm sequence

Reading a missing second entry as zero recovers the second input uniformly, including the singleton sequence with zero second input. Each entry after the second is the negated remainder of its two predecessors, and from the second entry on the degrees strictly decrease. These facts let results about one Euclidean step be propagated along the whole sequence.

@[simp]

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

A nonzero-headed Sturm sequence has its second input as its second entry, with zero representing the missing entry of a singleton sequence.

theorem Polynomial.eq_neg_mod_of_getElem?_sturmSeq {K : Type u_1} [Field K] [DecidableEq K] {p q a b c : Polynomial K} {i : ℕ} (ha : (p.sturmSeq q)[i]? = some a) (hb : (p.sturmSeq q)[i + 1]? = some b) (hc : (p.sturmSeq q)[i + 2]? = some c) : c = -a % b

Every entry of a Sturm sequence after the second is the negated remainder of its two predecessors.

theorem Polynomial.natDegree_lt_of_getElem?_sturmSeq {K : Type u_1} [Field K] [DecidableEq K] {p q s t : Polynomial K} {i : ℕ} (hs : (p.sturmSeq q)[i + 1]? = some s) (ht : (p.sturmSeq q)[i + 2]? = some t) : t.natDegree < s.natDegree

From the second entry on, the degrees of the entries of a Sturm sequence strictly decrease. The first two entries are unconstrained.

theorem Polynomial.natDegree_le_of_mem_sturmSeq {K : Type u_1} [Field K] [DecidableEq K] {p q s : Polynomial K} (hs : s ∈ p.sturmSeq q) (hq : q.natDegree ≤ p.natDegree) : s.natDegree ≤ p.natDegree

If the second input has degree at most that of the first, then so does every entry of the Sturm sequence.