Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Critical points of a complex p...


view this post on Zulip Email Gateway (Nov 21 2023 at 14:54):

From: Lawrence Paulson <lp15@cam.ac.uk>
And here is another contribution by the prolific Manuel Eberl:

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.

Online at https://www.isa-afp.org/entries/Polynomial_Crit_Geometry.html

Larry


Last updated: Apr 29 2024 at 01:08 UTC