Polynomial Rolle over an abstract real closed field

polynomialRolle_of_isRealClosed supplies TauCeti.PolynomialRolle R from IsRealClosed R. The direct Polynomial.exists_derivative_root and Polynomial.exists_eval_sub_eq_derivative_eval_mul give Rolle and mean value without a separate Rolle premise. The four Polynomial.*On_of_derivative_* theorems give monotonicity, antitonicity, and their strict variants on closed intervals. Under IsRealClosed, use these direct statements; TauCeti.Algebra.Polynomial.Rolle instead derives the same consequences from an explicit polynomial Rolle hypothesis over a general ordered field.

Between consecutive roots, removing their multiplicities leaves a polynomial of constant nonzero sign. A factor of the derivative has opposite signs at the endpoints, so polynomial IVT supplies the required critical point.

References

Salma Kuhlmann, Real Algebraic Geometry, Lecture 6, Corollary 2.2.

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

Between any two distinct roots there is a root of the formal derivative.

theorem TauCeti.RealClosure.polynomialRolle_of_isRealClosed {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] : PolynomialRolle R

Polynomial Rolle follows from the abstract real-closed-field axioms.

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

Equal endpoint values give an interior derivative root over a real closed field.

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

Polynomial mean value over an ordered real closed field.

theorem Polynomial.monotoneOn_of_derivative_nonneg {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p : Polynomial R) {a b : R} (hd : ∀ x ∈ Set.Ioo a b, 0 ≤ eval x (derivative p)) : MonotoneOn (fun (x : R) => eval x p) (Set.Icc a b)

A nonnegative formal derivative makes polynomial evaluation monotone on an interval.

theorem Polynomial.antitoneOn_of_derivative_nonpos {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p : Polynomial R) {a b : R} (hd : ∀ x ∈ Set.Ioo a b, eval x (derivative p) ≤ 0) : AntitoneOn (fun (x : R) => eval x p) (Set.Icc a b)

A nonpositive formal derivative makes polynomial evaluation antitone on an interval.

theorem Polynomial.strictMonoOn_of_derivative_pos {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p : Polynomial R) {a b : R} (hd : ∀ x ∈ Set.Ioo a b, 0 < eval x (derivative p)) : StrictMonoOn (fun (x : R) => eval x p) (Set.Icc a b)

A positive formal derivative makes polynomial evaluation strictly monotone on an interval.

theorem Polynomial.strictAntiOn_of_derivative_neg {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p : Polynomial R) {a b : R} (hd : ∀ x ∈ Set.Ioo a b, eval x (derivative p) < 0) : StrictAntiOn (fun (x : R) => eval x p) (Set.Icc a b)

A negative formal derivative makes polynomial evaluation strictly antitone on an interval.