Local variation jumps for alternating polynomial chains

IsAlternating records the sign conditions of a chain whose last entry has no roots. Interior zeros preserve sign variations. Crossing a simple root of the first entry changes the variation by the sign of its derivative times the second entry. These local identities supply the signed root sum in Sturm.Sum.

structure TauCeti.Sturm.IsAlternating {R : Type u_1} [Ring R] [LinearOrder R] (cs : List (Polynomial R)) : Prop

A alternating chain has opposite neighbors at every interior zero and no real zero in its last entry. These are the properties of a signed remainder chain after its common polynomial factor has been removed.

• nonzero (q : Polynomial R) : q ∈ cs → q ≠ 0

  Every entry is a nonzero polynomial.

• last (q : Polynomial R) : cs.getLast? = some q → ∀ (r : R), Polynomial.eval r q ≠ 0

  The terminal polynomial has no root in the coefficient ring.

• alternate (i : ℕ) (q0 q1 q2 : Polynomial R) : cs[i]? = some q0 → cs[i + 1]? = some q1 → cs[i + 2]? = some q2 → ∀ (r : R), Polynomial.eval r q1 = 0 → Polynomial.eval r q0 * Polynomial.eval r q2 < 0

  At an interior zero the adjacent values are nonzero and have opposite signs.

theorem TauCeti.Sturm.IsAlternating.tail {R : Type u_1} [Ring R] [LinearOrder R] {p : Polynomial R} {cs : List (Polynomial R)} (h : IsAlternating (p :: cs)) : IsAlternating cs

theorem TauCeti.Sturm.IsAlternating.signVariationsAt_eq {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {cs : List (Polynomial R)} (h : IsAlternating cs) (a r : R) (hne : ∀ q ∈ cs, Polynomial.eval a q ≠ 0) (hfront : ∀ (q : Polynomial R), cs.head? = some q → Polynomial.eval r q ≠ 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

A alternating chain has the same variations at two points if no entry vanishes at the first, the head does not vanish at the second, and all surviving signs agree.

theorem TauCeti.Sturm.IsAlternating.second_eval_ne_zero {R : Type u_1} [Ring R] [LinearOrder R] {p q : Polynomial R} {cs : List (Polynomial R)} (h : IsAlternating (p :: q :: cs)) {r : R} (hr : Polynomial.eval r p = 0) : Polynomial.eval r q ≠ 0

Consecutive entries of a alternating chain cannot both vanish.

theorem TauCeti.Sturm.IsAlternating.signVariationsAt_nonroot {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {cs : List (Polynomial R)} (h : IsAlternating cs) {a r b : R} (har : a < r) (hrb : r < b) (hfront : ∀ (q : Polynomial R), cs.head? = some q → Polynomial.eval r q ≠ 0) (hz : ∀ q ∈ cs, ∀ x ∈ Set.Icc a b, x ≠ r → Polynomial.eval x q ≠ 0) : signVariationsAt cs a = signVariationsAt cs r ∧ signVariationsAt cs r = signVariationsAt cs b

Crossing isolated interior zeros does not change variations.

theorem TauCeti.Sturm.IsAlternating.root_jump {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {p q : Polynomial R} {cs : List (Polynomial R)} (h : IsAlternating (p :: q :: cs)) {a r b : R} (har : a < r) (hrb : r < b) (hr : Polynomial.eval r p = 0) (hd : Polynomial.eval r (Polynomial.derivative p) ≠ 0) (hz : ∀ s ∈ p :: q :: cs, ∀ x ∈ Set.Icc a b, x ≠ r → Polynomial.eval x s ≠ 0) : ↑(signVariationsAt (p :: q :: cs) a) - ↑(signVariationsAt (p :: q :: cs) b) = ↑(SignType.sign (Polynomial.eval r (Polynomial.derivative p) * Polynomial.eval r q))

At a simple root of the head, the variation jump is the sign of the product of the head derivative and the second entry.