English
For a real polynomial p, the total number of real roots counted with multiplicity is at most the total number of real roots of its derivative counted with multiplicity, plus one.
Русский
Для действительного многочлена p общее число действительных корней с учетом кратностей не более суммарного количества корней производной p с кратностями, плюс один.
LaTeX
$$Multiset.card p.roots ≤ Multiset.card (derivative p).roots + 1$$
Lean4
/-- 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 card_roots_le_derivative (p : ℝ[X]) : Multiset.card p.roots ≤ Multiset.card (derivative p).roots + 1 :=
calc
Multiset.card p.roots = ∑ x ∈ p.roots.toFinset, p.roots.count x := (Multiset.toFinset_sum_count_eq _).symm
_ = ∑ x ∈ p.roots.toFinset, (p.roots.count x - 1 + 1) :=
(Eq.symm <|
Finset.sum_congr rfl fun _ hx =>
tsub_add_cancel_of_le <| Nat.succ_le_iff.2 <| Multiset.count_pos.2 <| Multiset.mem_toFinset.1 hx)
_ = (∑ x ∈ p.roots.toFinset, (p.rootMultiplicity x - 1)) + p.roots.toFinset.card := by
simp only [Finset.sum_add_distrib, Finset.card_eq_sum_ones, count_roots]
_ ≤
(∑ x ∈ p.roots.toFinset, p.derivative.rootMultiplicity x) +
((p.derivative.roots.toFinset \ p.roots.toFinset).card + 1) :=
(add_le_add (Finset.sum_le_sum fun _ _ => rootMultiplicity_sub_one_le_derivative_rootMultiplicity _ _)
p.card_roots_toFinset_le_card_roots_derivative_diff_roots_succ)
_ ≤
(∑ x ∈ p.roots.toFinset, p.derivative.roots.count x) +
((∑ x ∈ p.derivative.roots.toFinset \ p.roots.toFinset, p.derivative.roots.count x) + 1) :=
by
simp only [← count_roots]
refine add_le_add_left (add_le_add_right ((Finset.card_eq_sum_ones _).trans_le ?_) _) _
refine Finset.sum_le_sum fun x hx => Nat.succ_le_iff.2 <| ?_
rw [Multiset.count_pos, ← Multiset.mem_toFinset]
exact (Finset.mem_sdiff.1 hx).1
_ = Multiset.card (derivative p).roots + 1 :=
by
rw [← add_assoc, ← Finset.sum_union Finset.disjoint_sdiff, Finset.union_sdiff_self_eq_union, ←
Multiset.toFinset_sum_count_eq, ← Finset.sum_subset Finset.subset_union_right]
intro x _ hx₂
simpa only [Multiset.mem_toFinset, Multiset.count_eq_zero] using hx₂
