Variations of a Sturm sequence at a point

The variation of a signed Euclidean remainder sequence is the number used in Sturm's root-counting formula. Mathlib's Polynomial.sturmSeq supplies the sequence and TauCeti.Sturm.signVariationsAt counts its evaluated sign changes. At a zero of the nonzero second polynomial where the first is nonzero, the first and third values are opposite, so deleting the zero reveals exactly one sign change. This file records that local calculation alongside the sequence recurrence. The existing empty-list and singleton variation lemmas supply the zero cases. The calculation works over any ordered field; it does not require real closedness. Negating both inputs or multiplying them by a polynomial nonzero at the evaluation point leaves the variation unchanged, while a common root makes it zero. The evaluated variation uses the existing TauCeti.Sturm.signVariationsAt API on Polynomial.sturmSeq p q.

theorem TauCeti.Sturm.signVariationsAt_sturmSeq_eq_of_eval_eq_zero {K : Type u_1} [Field K] [LinearOrder K] {p q : Polynomial K} {x : K} (hp : Polynomial.eval x p = 0) : signVariationsAt (p.sturmSeq q) x = signVariationsAt (q.sturmSeq (-p % q)) x

A zero first value is deleted when counting Sturm variations.

theorem TauCeti.Sturm.signVariationsAt_sturmSeq_eq_add_of_eval_ne_zero {K : Type u_1} [Field K] [LinearOrder K] {p q : Polynomial K} {x : K} (hp : Polynomial.eval x p ≠ 0) (hq : Polynomial.eval x q ≠ 0) : signVariationsAt (p.sturmSeq q) x = signVariationsAt (q.sturmSeq (-p % q)) x + if SignType.sign (Polynomial.eval x p) = SignType.sign (Polynomial.eval x q) then 0 else 1

When the first two evaluations are nonzero, a Sturm variation step adds one exactly when their signs differ.

theorem TauCeti.Sturm.signVariationsAt_sturmSeq_eq_add_one_of_eval_ne_zero_of_eval_eq_zero {K : Type u_1} [Field K] [LinearOrder K] [AddLeftStrictMono K] {p q : Polynomial K} {x : K} (hp : Polynomial.eval x p ≠ 0) (hq0 : q ≠ 0) (hq : Polynomial.eval x q = 0) : signVariationsAt (p.sturmSeq q) x = signVariationsAt (q.sturmSeq (-p % q)) x + 1

At a zero of the nonzero second polynomial that is not a zero of the first, the first Sturm variation step contributes exactly one sign change.

@[simp]

theorem TauCeti.Sturm.signVariationsAt_sturmSeq_mul_left {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {r : Polynomial K} (p q : Polynomial K) {x : K} (hrx : Polynomial.eval x r ≠ 0) : signVariationsAt ((r * p).sturmSeq (r * q)) x = signVariationsAt (p.sturmSeq q) x

Multiplying both inputs by a common polynomial does not alter their Sturm variation away from its roots.

@[simp]

theorem TauCeti.Sturm.signVariationsAt_sturmSeq_neg_neg {K : Type u_1} [Field K] [LinearOrder K] [AddLeftStrictMono K] (p q : Polynomial K) (x : K) : signVariationsAt ((-p).sturmSeq (-q)) x = signVariationsAt (p.sturmSeq q) x

Negating both inputs preserves their Sturm variation.

@[simp]

theorem TauCeti.Sturm.signVariationsAt_sturmSeq_eq_zero_of_eval_eq_zero_of_eval_eq_zero {K : Type u_1} [Field K] [LinearOrder K] {p q : Polynomial K} {x : K} (hp : Polynomial.eval x p = 0) (hq : Polynomial.eval x q = 0) : signVariationsAt (p.sturmSeq q) x = 0

A common root of the two input polynomials annihilates every entry of their Sturm sequence, so its variation at that point is zero.