Gauss-Lucas Theorem

In this file we prove Gauss-Lucas Theorem: the roots of the derivative of a nonconstant complex polynomial are included in the convex hull of the roots of the polynomial.

noncomputable def Polynomial.derivRootWeight (P : Polynomial ℂ) (z w : ℂ) : ℝ

Given a polynomial P of positive degree and a root z of its derivative, derivRootWeight P z w gives the weight of a root w of P in a convex combination that is equal to z.

Equations

• P.derivRootWeight z w = if Polynomial.eval z P = 0 then Pi.single z 1 w else ↑(Polynomial.rootMultiplicity w P) / ‖z - w‖ ^ 2

theorem Polynomial.derivRootWeight_nonneg (P : Polynomial ℂ) (z w : ℂ) : 0 ≤ P.derivRootWeight z w

theorem Polynomial.sum_derivRootWeight_pos {P : Polynomial ℂ} (hP : 0 < P.degree) (z : ℂ) : 0 < ∑ w ∈ P.roots.toFinset, P.derivRootWeight z w

The sum of the weights derivRootWeight P z w of all the roots w of P is positive, provided that P is not a constant polynomial.

theorem Polynomial.eq_centerMass_of_eval_derivative_eq_zero {P : Polynomial ℂ} {z : ℂ} (hP : 0 < P.degree) (hz : eval z (derivative P) = 0) : z = P.roots.toFinset.centerMass (P.derivRootWeight z) id

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 Polynomial.rootSet_derivative_subset_convexHull_rootSet {P : Polynomial ℂ} (h₀ : 0 < P.degree) : (derivative P).rootSet ℂ ⊆ (convexHull ℝ) (P.rootSet ℂ)

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$.

See also eq_centerMass_of_eval_derivative_eq_zero for a version that provides explicit coefficients of the convex combination.