[isabelle] Two new AFP entries by Wenda Li on complex analysis



Dear all,

it is my pleasure to announce two strongly related and interesting AFP entries 
on complex analysis by Wenda Li.


Evaluate winding numbers through Cauchy indices

  In complex analysis, the winding number measures the number of times a
  path (counterclockwise) winds around a point, while the Cauchy index
  can approximate how the path winds. This entry provides a
  formalisation of the Cauchy index, which is then shown to be related
  to the winding number. In addition, this entry also offers a tactic
  that enables users to evaluate the winding number by calculating
  Cauchy indices.



Count the Number of Complex Roots

  Based on evaluating Cauchy indices through remainder sequences, this
  entry provides an effective procedure to count the number of complex
  roots (with multiplicity) of a polynomial within a rectangle box or a
  half-plane. Potential applications of this entry include certified
  complex root isolation (of a polynomial) and testing the Routh-Hurwitz
  stability criterion (i.e., to check whether all the roots of some
  characteristic polynomial have negative real parts).


For more information, have a look at:

https://www.isa-afp.org/entries/Winding_Number_Eval.html
https://www.isa-afp.org/entries/Count_Complex_Roots.html

Cheers,
RenÃ


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.