在 Isabelle/HOL 中通过柯西指数计算卷绕数与复根计数
计算机科学中的逻辑
2019-08-06 v3
摘要
在复分析中，卷绕数度量一条路径(逆时针)绕某点缠绕的次数，而柯西指数可近似描述路径的缠绕方式。我们在 Isabelle 定理证明器中形式化了这一近似关系，并提供一种通过柯西指数计算卷绕数的策略。进一步将该近似与辐角原理结合，我们得以利用余式序列有效计数多项式在特定域(如矩形框与半平面)内的复根个数。
引用
@article{arxiv.1804.03922,
title = {Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle/HOL},
author = {Wenda Li and Lawrence C. Paulson},
journal= {arXiv preprint arXiv:1804.03922},
year = {2019}
}
备注
32 pages