Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL.
Published version
Peer-reviewed
Repository URI
Repository DOI
Type
Article
Change log
Authors
Li, Wenda
Paulson, Lawrence C
Abstract
In complex analysis, the winding number measures the number of times a path (counter-clockwise) winds around a point, while the Cauchy index can approximate how the path winds. We formalise this approximation in the Isabelle theorem prover, and provide a tactic to evaluate winding numbers through Cauchy indices. By further combining this approximation with the argument principle, we are able to make use of remainder sequences to effectively count the number of complex roots of a polynomial within some domains, such as a rectangular box and a half-plane.
Description
Keywords
Cauchy index, Computer algebra, Interactive theorem proving, Isabelle/HOL, Root counting, The Routh–Hurwitz stability criterion, Winding number
Journal Title
J. Autom. Reasoning
Conference Name
Journal ISSN
0168-7433
1573-0670
1573-0670
Volume Title
64
Publisher
Springer Science and Business Media LLC
Publisher DOI
Sponsorship
The first author was funded by the China Scholarship Council, via the CSC Cambridge
Scholarship programme. This development is also supported by the European Research Council
Advanced Grant ALEXANDRIA (Project 742178).