Descartes' Rule of Signs

We define the "sign changes" in the coefficients of a polynomial, and prove Descartes' Rule of Signs: a real polynomial has at most as many positive roots as there are sign changes. A sign change is when there is a positive coefficient followed by a negative coefficient, or vice versa, with any number of zero coefficients in between.

Main Definitions

• Polynomial.signVariations: The number of sign changes in a polynomial's coefficients, where 0 coefficients are ignored.

Main theorem

• Polynomial.roots_countP_pos_le_signVariations. States that P.roots.countP (0 < ·) ≤ P.signVariations, so that positive roots are counted with multiplicity. It's currently proved for any CommRing with IsStrictOrderedRing. There is likely some correct statement in terms of a (noncommutative) Ring, but Polynomial.roots is only defined for commutative rings.

Reference

Wikipedia: Descartes' Rule of Signs

def Polynomial.signVariations {R : Type u_1} [Semiring R] [LinearOrder R] (P : Polynomial R) : ℕ

Counts the number of times that the coefficients in a polynomial change sign, with the convention that 0 can count as either sign.

Equations

• P.signVariations = (List.destutter (fun (x1 x2 : SignType) => x1 ≠ x2) (List.filter (fun (x : SignType) => decide (x ≠ 0)) (List.map (⇑SignType.sign) P.coeffList))).length - 1

@[simp]

theorem Polynomial.signVariations_zero (R : Type u_1) [Semiring R] [LinearOrder R] : signVariations 0 = 0

@[simp]

theorem Polynomial.signVariations_monomial {R : Type u_1} [Semiring R] [LinearOrder R] (d : ℕ) (c : R) : ((monomial d) c).signVariations = 0

Sign variations of a monomial are always zero.

theorem Polynomial.signVariations_eraseLead {R : Type u_1} [Semiring R] [LinearOrder R] (P : Polynomial R) (h : SignType.sign P.leadingCoeff = SignType.sign P.nextCoeff) : P.eraseLead.signVariations = P.signVariations

If the first two signs are the same, then sign_variations is unchanged by eraseLead

theorem Polynomial.signVariations_eq_eraseLead_add_ite {R : Type u_1} [Semiring R] [LinearOrder R] {P : Polynomial R} (h : P ≠ 0) : P.signVariations = P.eraseLead.signVariations + if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0

If we drop the leading coefficient, the sign changes drop by 0 or 1 depending on whether the first two nonzero coeffients match.

theorem Polynomial.signVariations_eraseLead_le {R : Type u_1} [Semiring R] [LinearOrder R] (P : Polynomial R) : P.eraseLead.signVariations ≤ P.signVariations

We can only lose, not gain, sign changes if we drop the leading coefficient.

theorem Polynomial.signVariations_le_eraseLead_succ {R : Type u_1} [Semiring R] [LinearOrder R] (P : Polynomial R) : P.signVariations ≤ P.eraseLead.signVariations + 1

We can only lose at most one sign changes if we drop the leading coefficient.

@[simp]

theorem Polynomial.signVariations_neg {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] (P : Polynomial R) : (-P).signVariations = P.signVariations

The number of sign changes does not change if we negate.

@[simp]

theorem Polynomial.signVariations_C_mul {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {η : R} (P : Polynomial R) (hx : η ≠ 0) : (C η * P).signVariations = P.signVariations

The number of sign changes does not change if we multiply by any nonzero scalar.

theorem Polynomial.signVariations_eraseLead_mul_X_sub_C {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {P : Polynomial R} {η : R} (hη : 0 < η) (hP₀ : 0 < P.leadingCoeff) (hc : P.nextCoeff < 0) : ((X - C η) * P).eraseLead.signVariations = ((X - C η) * P.eraseLead).signVariations

If P's coefficients start with signs [+, -, ...], then multiplying by a binomial X - η commutes with eraseLead in the number of sign changes. This is because the product of P and X - η has the pattern [+, -, ...] as well, so then P.eraseLead starts with [-,...], and multiplying by X - η gives [-, ...] too.

theorem Polynomial.succ_signVariations_X_sub_C_mul_monomial {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {η : R} {d : ℕ} {c : R} (hc : c ≠ 0) (hη : 0 < η) : ((monomial d) c).signVariations + 1 ≤ ((X - C η) * (monomial d) c).signVariations

This lemma is really a specialization of succ_signVariations_le_sub_mul to monomials.

theorem Polynomial.signVariations_X_sub_C_mul_eraseLead_le {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {P : Polynomial R} {η : R} (h : 0 < P.leadingCoeff) (h₂ : 0 < P.nextCoeff) : ((X - C η) * P.eraseLead).signVariations ≤ ((X - C η) * P).signVariations

If a polynomial starts with two positive coefficients, then the sign changes in the product (X - η) * P is the same as (X - η) * P.eraseLead. This lemma lets us do induction on the degree of P when P starts with matching coefficient signs. Of course this is also true when the first two coefficients of P are negative, but we just prove the case where they're positive since it's cleaner and sufficient for the later use.

theorem Polynomial.succ_signVariations_le_X_sub_C_mul {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {P : Polynomial R} {η : R} (hη : 0 < η) (hP : P ≠ 0) : P.signVariations + 1 ≤ ((X - C η) * P).signVariations

Multiplying a polynomial by a linear term X - η adds at least one sign change. This is the basis for the induction in roots_countP_pos_le_signVariations.

theorem Polynomial.roots_countP_pos_le_signVariations {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (P : Polynomial R) : Multiset.countP (fun (x : R) => 0 < x) P.roots ≤ P.signVariations

Descartes' Rule of Signs: the number of positive roots is at most the number of sign variations.