Polynomial intermediate values over an abstract real closed field

The polynomial API gives roots from strict or weak endpoint sign changes and both orientations of closed-interval image inclusion. Polynomial.eval_mul_pos_of_no_roots is the constant-sign result used by polynomial Rolle.

Irreducible factors have degree at most two; quadratic factors have constant nonzero sign, so a sign change forces a root of a linear factor.

References

Salma Kuhlmann, Real Algebraic Geometry, Lecture 5, Corollaries 3.1 and 3.2.

theorem Polynomial.eval_mul_pos_of_no_roots {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p : Polynomial R) {a b : R} (hab : a ≤ b) (hroot : ∀ x ∈ Set.Icc a b, eval x p ≠ 0) : 0 < eval a p * eval b p

A polynomial has constant nonzero sign on any closed interval containing none of its roots.

theorem Polynomial.exists_root_Icc_of_mul_nonpos {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p : Polynomial R) {a b : R} (hab : a ≤ b) (h : eval a p * eval b p ≤ 0) : ∃ c ∈ Set.Icc a b, eval c p = 0

A nonpositive product of endpoint values gives a root on the closed interval.

theorem Polynomial.exists_root_Icc {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 : 0 ≤ eval b p) : ∃ c ∈ Set.Icc a b, eval c p = 0

Weakly opposite endpoint signs give a root on the closed interval.

theorem Polynomial.exists_root_Ioo {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 : 0 < eval b p) : ∃ c ∈ Set.Ioo a b, eval c p = 0

Polynomial IVT over an arbitrary real closed ordered field, including non-Archimedean fields.

theorem Polynomial.exists_root_Ioo_of_mul_neg {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p : Polynomial R) {a b : R} (hab : a < b) (h : eval a p * eval b p < 0) : ∃ c ∈ Set.Ioo a b, eval c p = 0

The symmetric sign-change form of polynomial IVT.

theorem Polynomial.intermediate_value_Icc {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p : Polynomial R) {a b : R} (hab : a ≤ b) : Set.Icc (eval a p) (eval b p) ⊆ (fun (x : R) => eval x p) '' Set.Icc a b

Polynomial intermediate value on a closed interval, for p.eval a ≤ y ≤ p.eval b.

theorem Polynomial.intermediate_value_Icc' {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p : Polynomial R) {a b : R} (hab : a ≤ b) : Set.Icc (eval b p) (eval a p) ⊆ (fun (x : R) => eval x p) '' Set.Icc a b

Polynomial intermediate value on a closed interval, for p.eval b ≤ y ≤ p.eval a.