Polynomial signs between roots in a real closed field

Signs are constant on root-free intervals. At a simple root, the signs on either side are determined by the sign of the derivative. Between two nonroots, the change of sign is the sum of the jumps signRight - signLeft of the one-sided signs at the roots in between.

theorem Polynomial.sign_eval_const {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p : Polynomial R) {a b : R} (hab : a ≤ b) (hz : ∀ x ∈ Set.Icc a b, eval x p ≠ 0) : SignType.sign (eval a p) = SignType.sign (eval b p)

A polynomial has a constant sign on a root-free interval.

theorem Polynomial.signs_at_nonroot {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p : Polynomial R) {a r b : R} (har : a < r) (hrb : r < b) (hr : eval r p ≠ 0) (hz : ∀ x ∈ Set.Icc a b, x ≠ r → eval x p ≠ 0) : SignType.sign (eval a p) = SignType.sign (eval r p) ∧ SignType.sign (eval b p) = SignType.sign (eval r p)

If a polynomial has no zeros except possibly at an interior point, and does not vanish there either, both endpoint signs agree with its sign at that point.

theorem Polynomial.signs_at_root {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p : Polynomial R) {a r b : R} (har : a < r) (hrb : r < b) (hr : eval r p = 0) (hd : eval r (derivative p) ≠ 0) (hz : ∀ x ∈ Set.Icc a b, x ≠ r → eval x p ≠ 0) : SignType.sign (eval a p) = -SignType.sign (eval r (derivative p)) ∧ SignType.sign (eval b p) = SignType.sign (eval r (derivative p))

Near an isolated simple root, a polynomial changes from the negative of its derivative's sign to its derivative's sign.

theorem Polynomial.sign_eval_sub_sign_eval_eq_sum {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p : Polynomial R) {a b : R} (hab : a < b) (ha : eval a p ≠ 0) (hb : eval b p ≠ 0) : ↑(SignType.sign (eval b p)) - ↑(SignType.sign (eval a p)) = ∑ x ∈ p.roots.toFinset with a < x ∧ x < b, (↑(p.signRight x) - ↑(p.signLeft x))

Between two nonroots, the change of sign of a polynomial is the sum of the jumps of its one-sided signs at the roots in between. Multiple roots are allowed.