A formal proof of Cauchy’s residue theorem. (English) Zbl 1478.68440

Li, Wenda; Paulson, Lawrence C.

Blanchette, Jasmin Christian (ed.) et al., Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22–25, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9807, 235-251 (2016).

Summary: We present a formalization of Cauchy’s residue theorem and two of its corollaries: the argument principle and Rouché’s theorem. These results have applications to verify algorithms in computer algebra and demonstrate Isabelle/HOL’s complex analysis library.
For the entire collection see [Zbl 1343.68004].

MSC:

68V20	Formalization of mathematics in connection with theorem provers
03B35	Mechanization of proofs and logical operations
30E20	Integration, integrals of Cauchy type, integral representations of analytic functions in the complex plane

Software:

Coquelicot; Isabelle/HOL; Isabelle; kepler98; HOL; C-CoRN

References:

[1]	Ahlfors, L.V.: Complex Analysis: An Introduction to the Theory of Analytic Funtions of One Complex Variable. McGraw-Hill, New York (1966)
[2]	Avigad, J., Hölzl, J., Serafin, L.: A formally verified proof of the central limit theorem. CoRR abs/1405.7012 (2014) · Zbl 1425.68369
[3]	Bak, J., Newman, D.: Complex Analysis. Springer, New York (2010) · Zbl 1205.30001
[4]	Basu, S., Pollack, R., Roy, M.F.: Algorithms in Real Algebraic Geometry, vol. 10. Springer, Heidelberg (2006) · Zbl 1102.14041
[5]	Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41–62 (2014) · Zbl 1322.68176
[6]	Brunel, A.: Non-constructive complex analysis in Coq. In: 18th International Workshop on Types for Proofs and Programs, TYPES 2011, Bergen, Norway, pp. 1–15, 8–11 September 2011
[7]	Bruno Brosowski, F.D.: An elementary proof of the Stone-Weierstrass theorem. Proc. Am. Math. Soc. 81(1), 89–92 (1981) · Zbl 0482.46014
[8]	Caviness, B., Johnson, J.: Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer, New York (2012)
[9]	Conway, J.B.: Functions of One Complex Variable, vol. 11, 2nd edn. Springer, New York (1978)
[10]	Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-CoRN, the constructive Coq repository at Nijmegen. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 88–103. Springer, Heidelberg (2004) · Zbl 1108.68586
[11]	Hales, T.C., Adams, M., Bauer, G., Dang, D.T., Harrison, J., Hoang, T.L., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T.T., Nguyen, T.Q., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, A.H.T., Tran, T.N., Trieu, D.T., Urban, J., Vu, K.K., Zumkeller, R.: A formal proof of the Kepler conjecture. arXiv:1501.02155 (2015)
[12]	Harrison, J.: Formalizing basic complex analysis. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, vol. 10(23), pp. 151–165. University of Białystok (2007)
[13]	Harrison, J.: Formalizing an analytic proof of the Prime Number Theorem (dedicated to Mike Gordon on the occasion of his 60th birthday). J. Autom. Reasoning 43, 243–261 (2009) · Zbl 1185.68624
[14]	Harrison, J.: The HOL light theory of Euclidean space. J. Autom. Reasoning 50, 173–190 (2013) · Zbl 1260.68373
[15]	Lang, S.: Complex Analysis. Springer, New York (1993) · Zbl 0819.30001
[16]	Stein, E.M., Shakarchi, R.: Complex Analysis, vol. 2. Princeton University Press, Princeton (2010) · Zbl 1020.30001