English
If deg P > 0 and z is a root of P', then z is the center of mass of the roots of P with weights derivRootWeight z w.
Русский
Пусть deg P > 0 и z — корень P'; тогда z является центром массы корней P с весами derivRootWeight z w.
LaTeX
$$z = \\dfrac{\\sum_{w\\in P.roots} \\operatorname{derivRootWeight}(z,w) \\; w}{\\sum_{w\\in P.roots} \\operatorname{derivRootWeight}(z,w)}$$
Lean4
/-- *Gauss-Lucas Theorem*: if $P$ is a nonconstant polynomial with complex coefficients,
then all zeros of $P'$ belong to the convex hull of the set of zeros of $P$.
This version provides explicit formulas for the coefficients of the convex combination.
See also `rootSet_derivative_subset_convexHull_rootSet` below.
-/
theorem eq_centerMass_of_eval_derivative_eq_zero (hP : 0 < P.degree) (hz : P.derivative.eval z = 0) :
z = P.roots.toFinset.centerMass (P.derivRootWeight z) id :=
by
have hP₀ : P ≠ 0 := by rintro rfl; simp at hP
set weight : ℂ → ℝ := P.derivRootWeight z
set s := P.roots.toFinset
suffices ∑ x ∈ s, weight x • (z - x) = 0 by
calc
z = s.centerMass weight fun _ ↦ z :=
by
rw [Finset.centerMass, ← Finset.sum_smul, inv_smul_smul₀]
exact (sum_derivRootWeight_pos hP z).ne'
_ = s.centerMass weight (z - ·) + s.centerMass weight id := by
simp only [Finset.centerMass, ← smul_add, ← Finset.sum_add_distrib, id, sub_add_cancel]
_ = s.centerMass weight id := by simp only [add_eq_right, Finset.centerMass, this, smul_zero]
by_cases hzP : P.eval z = 0
· simp only [weight, derivRootWeight, if_pos hzP]
rw [Finset.sum_eq_single z] <;> simp_all
calc
∑ x ∈ s, weight x • (z - x) = conj (∑ x ∈ s, P.rootMultiplicity x • (1 / (z - x))) :=
by
simp only [map_sum, weight, derivRootWeight, if_neg hzP]
refine Finset.sum_congr rfl fun x hx ↦ ?_
have : z - x ≠ 0 := by
rw [sub_ne_zero]
rintro rfl
simp_all [s]
simp [← Complex.conj_mul', field]
_ = conj (P.roots.map fun x ↦ 1 / (z - x)).sum := by simp only [Finset.sum_multiset_map_count, P.count_roots, s]
_ = 0 := by
rw [← eval_derivative_div_eval_of_ne_zero_of_splits (IsAlgClosed.splits _) hzP]
simp [hz]
