A formal proof of Cauchy's residue theorem

DOI10.1007/978-3-319-43144-4_15MaRDI QIDQ2829261zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Wenda Li, Lawrence C. Paulson

Publication date 27 October 2016

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://www.repository.cam.ac.uk/handle/1810/262370

Mathematics Subject Classification ID

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

Recommendations

• Cauchy's residue sore thumb
• Formalizing an analytic proof of the prime number theorem
• A direct proof and a transcendental version of the fundamental theorem of algebra via Cauchy's theorem
• An Isabelle/HOL formalisation of Green's theorem
• An Isabelle/HOL formalisation of Green's theorem

Cites work

• scientific article; zbMATH DE number 1889799 (Why is no real title available?)
• A formally verified proof of the central limit theorem
• Algorithms in real algebraic geometry
• An Elementary Proof of the Stone-Weierstrass Theorem
• Complex Analysis
• Complex Analysis
• Coquelicot: a user-friendly library of real analysis for Coq
• Formalizing an analytic proof of the prime number theorem
• Mathematical Knowledge Management
• The HOL Light theory of Euclidean space

Cited in

(5)

• Non-constructive complex analysis in Coq
• Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
• An Isabelle/HOL formalisation of Green's theorem
• An Isabelle/HOL formalisation of Green's theorem
• Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL

Describes a project that uses

Uses Software

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

This page was built for publication: A formal proof of Cauchy's residue theorem

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829261)