One-sided polynomial signs

The first nonzero formal derivative determines a polynomial's sign immediately to the right of a point. To the left, the parity of its root multiplicity supplies the additional sign. These algebraic signs allow endpoint root-count formulas to include multiple roots without choosing nearby evaluation points.

Both signs are zero for the zero polynomial. Over any ordered field they agree with evaluation on sufficiently small open intervals on the appropriate side. No completeness or Archimedean assumption is needed.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapters 2 and 10.

noncomputable def Polynomial.signRight {R : Type u_1} [CommRing R] [LinearOrder R] (p : Polynomial R) (a : R) : SignType

The right-hand sign, computed from the derivative at the root multiplicity. For a nonzero polynomial over an ordered field this is its first nonzero derivative. The zero polynomial has sign zero.

Equations

• p.signRight a = p.derivativeSign a (Polynomial.rootMultiplicity a p)

noncomputable def Polynomial.signLeft {R : Type u_1} [CommRing R] [LinearOrder R] (p : Polynomial R) (a : R) : SignType

The left-hand sign is the right-hand sign corrected by multiplicity parity.

Equations

• p.signLeft a = (-1) ^ Polynomial.rootMultiplicity a p * p.signRight a

theorem Polynomial.signRight_def {R : Type u_1} [CommRing R] [LinearOrder R] (p : Polynomial R) (a : R) : p.signRight a = SignType.sign (eval a ((⇑derivative)^[rootMultiplicity a p] p))

The derivative formula for the right-hand sign.

theorem Polynomial.signLeft_def {R : Type u_1} [CommRing R] [LinearOrder R] (p : Polynomial R) (a : R) : p.signLeft a = (-1) ^ rootMultiplicity a p * p.signRight a

The parity formula for the left-hand sign.

@[simp]

theorem Polynomial.signRight_zero {R : Type u_1} [CommRing R] [LinearOrder R] (a : R) : signRight 0 a = 0

@[simp]

theorem Polynomial.signLeft_zero {R : Type u_1} [CommRing R] [LinearOrder R] (a : R) : signLeft 0 a = 0

@[simp]

theorem Polynomial.signRight_C {R : Type u_1} [CommRing R] [LinearOrder R] (c a : R) : (C c).signRight a = SignType.sign c

@[simp]

theorem Polynomial.signLeft_C {R : Type u_1} [CommRing R] [LinearOrder R] (c a : R) : (C c).signLeft a = SignType.sign c

theorem Polynomial.signRight_eq_sign_eval {R : Type u_1} [CommRing R] [LinearOrder R] (p : Polynomial R) {a : R} (ha : eval a p ≠ 0) : p.signRight a = SignType.sign (eval a p)

Away from a root, the right-hand sign is the sign of the value itself.

theorem Polynomial.signLeft_eq_sign_eval {R : Type u_1} [CommRing R] [LinearOrder R] (p : Polynomial R) {a : R} (ha : eval a p ≠ 0) : p.signLeft a = SignType.sign (eval a p)

Away from a root, the left-hand sign is also the sign of the value.

theorem Polynomial.signRight_add_eq_left_of_dvd {R : Type u_1} [CommRing R] [LinearOrder R] {p q : Polynomial R} {a : R} (hp : p ≠ 0) (hq : (X - C a) ^ (rootMultiplicity a p + 1) ∣ q) : (p + q).signRight a = p.signRight a

Adding a multiple of a higher power of X - C a leaves the right-hand sign at a of a nonzero polynomial unchanged.

theorem Polynomial.signLeft_add_eq_left_of_dvd {R : Type u_1} [CommRing R] [LinearOrder R] {p q : Polynomial R} {a : R} (hp : p ≠ 0) (hq : (X - C a) ^ (rootMultiplicity a p + 1) ∣ q) : (p + q).signLeft a = p.signLeft a

Adding a multiple of a higher power of X - C a leaves the left-hand sign at a of a nonzero polynomial unchanged.

@[simp]

theorem Polynomial.signRight_map {R : Type u_1} [CommRing R] [LinearOrder R] {S : Type u_2} [CommRing S] [LinearOrder S] (p : Polynomial R) (f : R →+* S) (hf : StrictMono ⇑f) (a : R) : (map f p).signRight (f a) = p.signRight a

Strictly monotone ring embeddings preserve right-hand signs.

@[simp]

theorem Polynomial.signLeft_map {R : Type u_1} [CommRing R] [LinearOrder R] {S : Type u_2} [CommRing S] [LinearOrder S] (p : Polynomial R) (f : R →+* S) (hf : StrictMono ⇑f) (a : R) : (map f p).signLeft (f a) = p.signLeft a

Strictly monotone ring embeddings preserve left-hand signs.

theorem Polynomial.signRight_eq_sign_eval_divByMonic {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (a : R) : p.signRight a = SignType.sign (eval a (p /ₘ (X - C a) ^ rootMultiplicity a p))

Removing the full root factor gives the same sign as the first nonzero derivative.

@[simp]

theorem Polynomial.signRight_eq_zero_iff {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (a : R) : p.signRight a = 0 ↔ p = 0

A one-sided sign vanishes exactly when the polynomial is zero.

@[simp]

theorem Polynomial.signLeft_eq_zero_iff {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (a : R) : p.signLeft a = 0 ↔ p = 0

theorem Polynomial.eval_ne_zero_of_sign_eq_signRight {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {p : Polynomial R} (hp : p ≠ 0) {a x : R} (h : SignType.sign (eval x p) = p.signRight a) : eval x p ≠ 0

A nonzero polynomial does not vanish where it has its right-hand sign.

theorem Polynomial.eval_ne_zero_of_sign_eq_signLeft {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {p : Polynomial R} (hp : p ≠ 0) {a x : R} (h : SignType.sign (eval x p) = p.signLeft a) : eval x p ≠ 0

A nonzero polynomial does not vanish where it has its left-hand sign.

theorem Polynomial.signLeft_eq_signRight_of_even {R : Type u_1} [CommRing R] [LinearOrder R] (p : Polynomial R) (a : R) (h : Even (rootMultiplicity a p)) : p.signLeft a = p.signRight a

An even root multiplicity gives equal signs on the two sides.

theorem Polynomial.signLeft_eq_neg_signRight_of_odd {R : Type u_1} [CommRing R] [LinearOrder R] (p : Polynomial R) (a : R) (h : Odd (rootMultiplicity a p)) : p.signLeft a = -p.signRight a

An odd root multiplicity gives opposite signs on the two sides.

@[simp]

theorem Polynomial.signRight_mul {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p q : Polynomial R) (a : R) : (p * q).signRight a = p.signRight a * q.signRight a

Multiplication multiplies right-hand signs, including when a factor is zero.

@[simp]

theorem Polynomial.signLeft_mul {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p q : Polynomial R) (a : R) : (p * q).signLeft a = p.signLeft a * q.signLeft a

Multiplication multiplies left-hand signs, including when a factor is zero.

@[simp]

theorem Polynomial.signRight_one {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (a : R) : signRight 1 a = 1

@[simp]

theorem Polynomial.signLeft_one {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (a : R) : signLeft 1 a = 1

@[simp]

theorem Polynomial.signRight_neg {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (a : R) : (-p).signRight a = -p.signRight a

Negation reverses the right-hand sign.

@[simp]

theorem Polynomial.signLeft_neg {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (a : R) : (-p).signLeft a = -p.signLeft a

Negation reverses the left-hand sign.

@[simp]

theorem Polynomial.signRight_pow {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (a : R) (n : ℕ) : (p ^ n).signRight a = p.signRight a ^ n

Powers raise the right-hand sign to the same power, with the convention 0^0 = 1.

@[simp]

theorem Polynomial.signLeft_pow {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (a : R) (n : ℕ) : (p ^ n).signLeft a = p.signLeft a ^ n

Powers raise the left-hand sign to the same power, with the convention 0^0 = 1.

theorem Polynomial.exists_signLeft_signRight {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (a : R) : ∃ (l : R) (u : R), l < a ∧ a < u ∧ (∀ x ∈ Set.Ioo l a, SignType.sign (eval x p) = p.signLeft a) ∧ ∀ x ∈ Set.Ioo a u, SignType.sign (eval x p) = p.signRight a

The algebraic one-sided signs are realized on intervals immediately to the left and right, including at multiple roots and for the zero polynomial.

theorem List.exists_signs_right {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (cs : List (Polynomial R)) (a : R) : ∃ (u : R), a < u ∧ ∀ p ∈ cs, ∀ x ∈ Set.Ioo a u, SignType.sign (Polynomial.eval x p) = p.signRight a

A uniform interval immediately to the right of a on which every polynomial of a list has its right-hand sign at a.

theorem List.exists_signs_left {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (cs : List (Polynomial R)) (a : R) : ∃ l < a, ∀ p ∈ cs, ∀ x ∈ Set.Ioo l a, SignType.sign (Polynomial.eval x p) = p.signLeft a

A uniform interval immediately to the left of a on which every polynomial of a list has its left-hand sign at a.