Rolle's Theorem for polynomials

In this file we use Rolle's Theorem to relate the number of real roots of a real polynomial and its derivative. Namely, we prove the following facts.

• Polynomial.card_roots_toFinset_le_card_roots_derivative_diff_roots_succ: the number of roots of a real polynomial p is at most the number of roots of its derivative that are not roots of p plus one.
• Polynomial.card_roots_toFinset_le_derivative, Polynomial.card_rootSet_le_derivative: the number of roots of a real polynomial is at most the number of roots of its derivative plus one.
• Polynomial.card_roots_le_derivative: same, but the roots are counted with multiplicities.

Keywords

polynomial, Rolle's Theorem, root

theorem Polynomial.card_roots_toFinset_le_card_roots_derivative_diff_roots_succ (p : Polynomial ℝ) : (Multiset.toFinset (Polynomial.roots p)).card ≤ (Multiset.toFinset (Polynomial.roots (Polynomial.derivative p)) \ Multiset.toFinset (Polynomial.roots p)).card + 1

The number of roots of a real polynomial p is at most the number of roots of its derivative that are not roots of p plus one.

theorem Polynomial.card_roots_toFinset_le_derivative (p : Polynomial ℝ) : (Multiset.toFinset (Polynomial.roots p)).card ≤ (Multiset.toFinset (Polynomial.roots (Polynomial.derivative p))).card + 1

The number of roots of a real polynomial is at most the number of roots of its derivative plus one.

theorem Polynomial.card_roots_le_derivative (p : Polynomial ℝ) : Multiset.card (Polynomial.roots p) ≤ Multiset.card (Polynomial.roots (Polynomial.derivative p)) + 1

The number of roots of a real polynomial (counted with multiplicities) is at most the number of roots of its derivative (counted with multiplicities) plus one.

theorem Polynomial.card_rootSet_le_derivative {F : Type u_1} [CommRing F] [Algebra F ℝ] (p : Polynomial F) : Fintype.card ↑(Polynomial.rootSet p ℝ) ≤ Fintype.card ↑(Polynomial.rootSet (Polynomial.derivative p) ℝ) + 1

The number of real roots of a polynomial is at most the number of roots of its derivative plus one.