The sign of a polynomial immediately to the right of a point

A nonzero real polynomial has finitely many roots, so its sign is constant on a small interval (x, x + ε) to the right of any point x. This file defines that sign, Polynomial.signRight x p, as the limit of sign (p.eval y) as y → x from the right, and develops its basic properties: it vanishes only for p = 0, it is multiplicative, and it is computed by the recursion signRight x p = sign (p.eval x) if p.eval x ≠ 0 and signRight x p = signRight x (derivative p) otherwise.

This is the local invariant behind Sturm's theorem, where it determines the direction in which the sign of a Sturm sequence changes across a root.

Main definitions

• Polynomial.signRight x p: the sign of p immediately to the right of x.

Main results

• Polynomial.eventually_sign_eq_signRight, Polynomial.signRight_eq_iff: the defining property, sign (p.eval y) = signRight x p for all y in some interval (x, x + ε).
• Polynomial.signRight_eq_zero_iff: signRight x p = 0 if and only if p = 0.
• Polynomial.signRight_mul, Polynomial.signRight_neg, Polynomial.signRight_C: signRight x is multiplicative and compatible with negation and constants.
• Polynomial.signRight_of_eval_ne_zero: away from the roots of p, signRight x p is the sign of p.eval x.
• Polynomial.signRight_of_eval_eq_zero: at a root of p, signRight x p is signRight x of the derivative of p.

Implementation notes

The definition and all results are stated over ℝ, but they hold over any real closed field, and should eventually be generalised to IsRealClosed. Two ingredients stand in the way: the intermediate value theorem for polynomials over a real closed field, which Mathlib does not have yet and which is needed for exists_eventually_sign_eq (the proof here uses connectedness of intervals in ℝ), and the mean value theorem, used in signRight_of_eval_eq_zero, which can be replaced by an algebraic argument factoring the root out of p.

theorem Polynomial.exists_eventually_sign_eq (x : ℝ) (p : Polynomial ℝ) : ∃ (s : SignType), ∀ᶠ (y : ℝ) in nhdsWithin x (Set.Ioi x), SignType.sign (eval y p) = s

Immediately to the right of x, a polynomial has a constant sign.

noncomputable def Polynomial.signRight (x : ℝ) (p : Polynomial ℝ) : SignType

The sign of p immediately to the right of x: the eventual value of sign (eval y p) as y → x from the right.

Equations

• Polynomial.signRight x p = (nhdsWithin x (Set.Ioi x)).limUnder fun (y : ℝ) => SignType.sign (Polynomial.eval y p)

theorem Polynomial.eventually_sign_eq_signRight (x : ℝ) (p : Polynomial ℝ) : ∀ᶠ (y : ℝ) in nhdsWithin x (Set.Ioi x), SignType.sign (eval y p) = signRight x p

The equation sign (eval y p) = signRight x p holds for all y in some interval (x, x + ε).

theorem Polynomial.signRight_eq_of_eventually {x : ℝ} {p : Polynomial ℝ} {s : SignType} (h : ∀ᶠ (y : ℝ) in nhdsWithin x (Set.Ioi x), SignType.sign (eval y p) = s) : signRight x p = s

theorem Polynomial.signRight_eq_iff {x : ℝ} {p : Polynomial ℝ} {s : SignType} : signRight x p = s ↔ ∀ᶠ (y : ℝ) in nhdsWithin x (Set.Ioi x), SignType.sign (eval y p) = s

signRight x p is the unique sign s such that sign (eval y p) = s for all y in some interval (x, x + ε).

@[simp]

theorem Polynomial.signRight_zero (x : ℝ) : signRight x 0 = 0

theorem Polynomial.signRight_ne_zero {x : ℝ} {p : Polynomial ℝ} (hp : p ≠ 0) : signRight x p ≠ 0

@[simp]

theorem Polynomial.signRight_eq_zero_iff {x : ℝ} {p : Polynomial ℝ} : signRight x p = 0 ↔ p = 0

signRight x p can only be 0 if p is 0.

theorem Polynomial.signRight_mul (x : ℝ) (p q : Polynomial ℝ) : signRight x (p * q) = signRight x p * signRight x q

signRight is a multiplicative function.

theorem Polynomial.signRight_neg (x : ℝ) (p : Polynomial ℝ) : signRight x (-p) = -signRight x p

signRight commutes with negation.

@[simp]

theorem Polynomial.signRight_C (x c : ℝ) : signRight x (C c) = SignType.sign c

signRight of a constant equals the sign of the constant.

theorem Polynomial.signRight_C_mul (x c : ℝ) (p : Polynomial ℝ) : signRight x (C c * p) = SignType.sign c * signRight x p

theorem Polynomial.signRight_X_sub_C_pow (a : ℝ) (n : ℕ) : signRight a ((X - C a) ^ n) = 1

theorem Polynomial.signRight_mul_self {x : ℝ} {p : Polynomial ℝ} (hp : p ≠ 0) : signRight x (p * p) = 1

theorem Polynomial.signRight_of_eval_ne_zero {x : ℝ} {p : Polynomial ℝ} (h : eval x p ≠ 0) : signRight x p = SignType.sign (eval x p)

Away from its roots, the sign of p to the right of x is the sign of p x.

theorem Polynomial.signRight_of_eval_eq_zero {x : ℝ} {p : Polynomial ℝ} (hev : eval x p = 0) : signRight x p = signRight x (derivative p)

At a root of p, the sign of p to the right of x is that of derivative p.

theorem Polynomial.signRight_derivative_mul {x : ℝ} {p : Polynomial ℝ} (hp : p ≠ 0) (hev : eval x p = 0) : signRight x (derivative p * p) = 1

theorem Polynomial.signRight_add {x : ℝ} {p q : Polynomial ℝ} (hp : eval x p = 0) (hq : eval x q ≠ 0) : signRight x (p + q) = signRight x q

theorem Polynomial.signRight_mod {x : ℝ} {p q : Polynomial ℝ} (hp : eval x p = 0) (hq : eval x q ≠ 0) : signRight x (q % p) = signRight x q