Polynomial Rolle and mean value

TauCeti.PolynomialRolle R states that equal polynomial values at distinct endpoints give an interior root of the formal derivative. From this explicit hypothesis, PolynomialRolle.exists_eval_sub_eq_derivative_eval_mul derives polynomial mean value; over an ordered field, PolynomialRolle.monotoneOn, antitoneOn, strictMonoOn, and strictAntiOn derive the corresponding order properties from derivative signs.

TauCeti.FieldTheory.RealClosure.AbstractRolle supplies this hypothesis from IsRealClosed and exports direct Polynomial versions of these results for real closed ordered fields. The IsRealClosed ℝ instance specializes those statements to the real numbers.

def TauCeti.PolynomialRolle (R : Type u_1) [Field R] [LinearOrder R] : Prop

Polynomial Rolle: whenever a polynomial takes equal values at a < b, its formal derivative has a root in Ioo a b.

Equations

• TauCeti.PolynomialRolle R = ∀ (p : Polynomial R) (a b : R), a < b → Polynomial.eval a p = Polynomial.eval b p → ∃ c ∈ Set.Ioo a b, Polynomial.eval c (Polynomial.derivative p) = 0

theorem TauCeti.PolynomialRolle.of_forall {R : Type u_1} [Field R] [LinearOrder R] (h : ∀ (p : Polynomial R) (a b : R), a < b → Polynomial.eval a p = Polynomial.eval b p → ∃ c ∈ Set.Ioo a b, Polynomial.eval c (Polynomial.derivative p) = 0) : PolynomialRolle R

Construct the polynomial Rolle property from its quantified statement.

theorem TauCeti.PolynomialRolle.exists_derivative_root {R : Type u_1} [Field R] [LinearOrder R] (h : PolynomialRolle R) (p : Polynomial R) {a b : R} (hab : a < b) (heq : Polynomial.eval a p = Polynomial.eval b p) : ∃ c ∈ Set.Ioo a b, Polynomial.eval c (Polynomial.derivative p) = 0

Equal polynomial values at distinct endpoints give an interior derivative root.

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

Polynomial Rolle implies the mean value equality p.eval b - p.eval a = p.derivative.eval c * (b - a) at some point c ∈ Ioo a b.

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

Polynomial Rolle implies monotonicity where the derivative is nonnegative.

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

Polynomial Rolle implies antitonicity where the derivative is nonpositive.

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

Strict positivity of the derivative gives strict monotonicity.

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

Strict negativity of the derivative gives strict antitonicity.