English
For a real polynomial p, the number of distinct real roots is at most the number of distinct real roots of its derivative that are not roots of p, plus one.
Русский
Для действительного многочлена p число различных действительных корней не более числа различных корней производной p, которые не являются корнями p, плюс один.
LaTeX
$$$\left|p\text{.roots}_{\mathbb{R}}\right| \le \left|p'.\text{roots}_{\mathbb{R}} \setminus p.\text{roots}_{\mathbb{R}}\right| + 1$$$
Lean4
/-- 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 card_roots_toFinset_le_card_roots_derivative_diff_roots_succ (p : ℝ[X]) :
p.roots.toFinset.card ≤ (p.derivative.roots.toFinset \ p.roots.toFinset).card + 1 :=
by
rcases eq_or_ne (derivative p) 0 with hp' | hp'
· rw [eq_C_of_derivative_eq_zero hp', roots_C, Multiset.toFinset_zero, Finset.card_empty]
exact zero_le _
have hp : p ≠ 0 := ne_of_apply_ne derivative (by rwa [derivative_zero])
refine Finset.card_le_diff_of_interleaved fun x hx y hy hxy hxy' => ?_
rw [Multiset.mem_toFinset, mem_roots hp] at hx hy
obtain ⟨z, hz1, hz2⟩ := exists_deriv_eq_zero hxy p.continuousOn (hx.trans hy.symm)
refine ⟨z, ?_, hz1⟩
rwa [Multiset.mem_toFinset, mem_roots hp', IsRoot, ← p.deriv]
