Sign bookkeeping for abstract Sturm chains

Zero-skipping variations are unchanged when an interior zero has neighbors of opposite signs. This bookkeeping works over a strictly ordered ring. The closing constancy lemma uses the intermediate value property of a real closed field.

noncomputable def TauCeti.Sturm.signVariationsAt {R : Type u_1} [Semiring R] [LinearOrder R] (cs : List (Polynomial R)) (x : R) : ℕ

The zero-skipping variations of a polynomial list at a point.

Equations

• TauCeti.Sturm.signVariationsAt cs x = (List.map (Polynomial.eval x) cs).signVariations

theorem TauCeti.Sturm.signVariationsAt_def {R : Type u_1} [Semiring R] [LinearOrder R] (cs : List (Polynomial R)) (x : R) : signVariationsAt cs x = (List.map (Polynomial.eval x) cs).signVariations

Variations are computed on the list of evaluations.

@[simp]

theorem TauCeti.Sturm.signVariationsAt_nil {R : Type u_1} [Semiring R] [LinearOrder R] (x : R) : signVariationsAt [] x = 0

@[simp]

theorem TauCeti.Sturm.signVariationsAt_singleton {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) (x : R) : signVariationsAt [p] x = 0

theorem TauCeti.Sturm.signVariationsAt_cons {R : Type u_1} [Semiring R] [LinearOrder R] (cs : List (Polynomial R)) {p : Polynomial R} {x : R} : signVariationsAt (p :: cs) x = (if SignType.sign (Polynomial.eval x p) * (List.map (Polynomial.eval x) cs).firstSign = -1 then 1 else 0) + signVariationsAt cs x

Prepending an evaluation contributes one variation exactly when its sign is opposite to the first nonzero sign of the remaining evaluations.

theorem TauCeti.Sturm.signVariationsAt_map_mul {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (cs : List (Polynomial R)) {d : Polynomial R} {x : R} (hd : Polynomial.eval x d ≠ 0) : signVariationsAt (List.map (fun (x : Polynomial R) => d * x) cs) x = signVariationsAt cs x

Multiplying every entry by a polynomial that does not vanish at the point preserves the sign variations at that point.

theorem TauCeti.Sturm.signVariationsAt_eq_of_alternate {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] (cs : List (Polynomial R)) (a r : R) (hne : ∀ q ∈ cs, Polynomial.eval a q ≠ 0) (hfront : ∀ (q : Polynomial R), cs.head? = some q → Polynomial.eval r q ≠ 0) (hlast : ∀ (q : Polynomial R), cs.getLast? = some q → Polynomial.eval r q ≠ 0) (halt : ∀ (i : ℕ) (q0 q1 q2 : Polynomial R), cs[i]? = some q0 → cs[i + 1]? = some q1 → cs[i + 2]? = some q2 → Polynomial.eval r q1 = 0 → Polynomial.eval r q0 * Polynomial.eval r q2 < 0) (hsame : ∀ q ∈ cs, Polynomial.eval r q ≠ 0 → SignType.sign (Polynomial.eval a q) = SignType.sign (Polynomial.eval r q)) : signVariationsAt cs a = signVariationsAt cs r

Evaluations at a and r have the same variation count if no entry vanishes at a, the first and last entries do not vanish at r, zeros at r have nonvanishing opposite-sign neighbours, and the surviving signs agree.

theorem TauCeti.Sturm.signVariationsAt_const {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (cs : List (Polynomial R)) {a b : R} (hab : a ≤ b) (hz : ∀ q ∈ cs, ∀ x ∈ Set.Icc a b, Polynomial.eval x q ≠ 0) : signVariationsAt cs a = signVariationsAt cs b

Variations are constant if no chain entry vanishes on the interval.