Two theorems about the geometry of the critical points of a complex polynomial

Manuel Eberl
Archive of Formal Proofs 2023.

pdf AFP entry

Abstract

This entry formalises two well-known results about the geometric relation between the roots of a complex polynomial and its critical points, i.e. the roots of its derivative. The first of these is the Gauß–Lucas Theorem: The critical points of a complex polynomial lie inside the convex hull of its roots. The second one is Jensen’s Theorem: Every non-real critical point of a real polynomial lies inside a disc between two conjugate roots. These discs are called the Jensen discs: the Jensen disc of a pair of conjugate roots a ± bi is the smallest disc that contains both of them, i.e. the disc with centre a and radius b.

BibTex

@article{Polynomial_Crit_Geometry-AFP,
author = {Manuel Eberl},
title = {Two theorems about the geometry of the critical points of a complex polynomial},
journal = {Archive of Formal Proofs},
month = {November},
year = {2023},
note = {\url{https://isa-afp.org/entries/Polynomial_Crit_Geometry.html},
Formal proof development},
ISSN = {2150-914x},
}