Sturm sequences of positive multiples and generalized Sturm sequences

Candidates for Mathlib.Algebra.Polynomial.Sturm.Sequence: the Sturm sequence commutes with a map of fields (Polynomial.sturmSeq_map); over an ordered field, the Sturm sequences of positive multiples are entrywise positive multiples (Polynomial.forall₂_posAssoc_sturmSeq), and a list of nonzero polynomials, each from the third on a positive multiple of the negated remainder of the two before and the last a unit, is entrywise a list of positive multiples of the entries of the Sturm sequence of its first two (Polynomial.forall₂_posAssoc_sturmSeq_of_getElem): a generalized Sturm sequence, such as the remainder chain that integer arithmetic computes.

Main definitions

• Polynomial.PosAssoc: one polynomial a positive constant times another.

Main statements

• Polynomial.sturmSeq_map: the Sturm sequence of the images under a map of fields.
• Polynomial.forall₂_posAssoc_sturmSeq: the Sturm sequences of positive multiples.
• Polynomial.forall₂_posAssoc_sturmSeq_of_getElem: a generalized Sturm sequence.

theorem Polynomial.sturmSeq_map {K : Type u_1} {L : Type u_2} [Field K] [Field L] [DecidableEq K] [DecidableEq L] (φ : K →+* L) (p q : Polynomial K) : (map φ p).sturmSeq (map φ q) = List.map (map φ) (p.sturmSeq q)

The Sturm sequence commutes with a map of fields.

def Polynomial.PosAssoc {K : Type u_1} [Field K] [LinearOrder K] (p q : Polynomial K) : Prop

q is a positive constant times p.

Equations

• p.PosAssoc q = ∃ (c : K), 0 < c ∧ Polynomial.C c * p = q

theorem Polynomial.PosAssoc.eq_zero_iff {K : Type u_1} [Field K] [LinearOrder K] {p q : Polynomial K} (h : p.PosAssoc q) : p = 0 ↔ q = 0

theorem Polynomial.PosAssoc.natDegree_eq {K : Type u_1} [Field K] [LinearOrder K] {p q : Polynomial K} (h : p.PosAssoc q) : q.natDegree = p.natDegree

theorem Polynomial.PosAssoc.neg_mod {K : Type u_1} [Field K] [LinearOrder K] {p p' q q' : Polynomial K} (hp : p.PosAssoc p') (hq : q.PosAssoc q') : (-p % q).PosAssoc (-p' % q')

theorem Polynomial.forall₂_posAssoc_sturmSeq {K : Type u_1} [Field K] [LinearOrder K] [DecidableEq K] {p p' q q' : Polynomial K} (hp : p.PosAssoc p') (hq : q.PosAssoc q') : List.Forall₂ PosAssoc (p.sturmSeq q) (p'.sturmSeq q')

The Sturm sequences of positive multiples are entrywise positive multiples, of the same length.

theorem Polynomial.PosAssoc.refl {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p : Polynomial K) : p.PosAssoc p

theorem Polynomial.PosAssoc.symm {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {p q : Polynomial K} (h : p.PosAssoc q) : q.PosAssoc p

theorem Polynomial.PosAssoc.trans {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {p q r : Polynomial K} (h : p.PosAssoc q) (h' : q.PosAssoc r) : p.PosAssoc r

theorem Polynomial.forall₂_posAssoc_of_forall₂_of_forall₂ {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {l₁ l₂ l₃ : List (Polynomial K)} (h₁ : List.Forall₂ PosAssoc l₁ l₃) (h₂ : List.Forall₂ PosAssoc l₂ l₃) : List.Forall₂ PosAssoc l₁ l₂

Two lists of positive multiples of the entries of a third are entrywise positive multiples of each other.

theorem Polynomial.forall₂_posAssoc_sturmSeq_pair {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [DecidableEq K] {a b : Polynomial K} (ha : a ≠ 0) (hb : b ≠ 0) (hu : IsUnit b) : List.Forall₂ PosAssoc [a, b] (a.sturmSeq b)

A list [a, b] of nonzero polynomials with b a unit is, entrywise, the Sturm sequence of a and b.

theorem Polynomial.forall₂_posAssoc_sturmSeq_cons {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [DecidableEq K] {a b c : Polynomial K} {l : List (Polynomial K)} (ha : a ≠ 0) (hc : (-a % b).PosAssoc c) (h : List.Forall₂ PosAssoc (b :: l) (b.sturmSeq c)) : List.Forall₂ PosAssoc (a :: b :: l) (a.sturmSeq b)

A list b :: l of positive multiples of the entries of the Sturm sequence of b and a positive multiple of -a % b, preceded by a ≠ 0, is entrywise the Sturm sequence of a and b.

theorem Polynomial.forall₂_posAssoc_sturmSeq_of_getElem {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [DecidableEq K] {L : List (Polynomial K)} (hlen : 2 ≤ L.length) (h0 : ∀ p ∈ L, p ≠ 0) (hrem : ∀ (k : ℕ) (hk : k + 2 < L.length), (-L[k] % L[k + 1]).PosAssoc L[k + 2]) (hu : IsUnit (L.getLast ⋯)) : List.Forall₂ PosAssoc L (L[0].sturmSeq L[1])

A list s₀, s₁, …, s_m of nonzero polynomials whose last entry is a unit and in which each s_(k+2) is a positive multiple of -s_k % s_(k+1) is, entrywise, a list of positive multiples of the entries of sturmSeq s₀ s₁: a generalized (scaled) Sturm sequence.