Repository logo
 

Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL

Published version
Peer-reviewed

Change log

Abstract

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

Article, Interactive theorem proving, Isabelle/HOL, Computer algebra, Cauchy index, Winding number, Root counting, The Routh–Hurwitz stability criterion

Journal Title

Journal of Automated Reasoning

Conference Name

Journal ISSN

0168-7433
1573-0670

Volume Title

64

Publisher

Springer Netherlands
Sponsorship
European Research Council (742178)