LIPIcs.ITP.2022.23.pdf
- Filesize: 0.77 MB
- 19 pages
Document
Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean
Author
Yury Kudryashov 
-
Part of:
Volume:
13th International Conference on Interactive Theorem Proving (ITP 2022)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2022-08-03
File
Document Identifiers
Author Details
Acknowledgements
I want to thank Patrick Massot for bringing up an idea of formalizing a sufficiently general version of the divergence theorem, Sébastien Gouëzel for fruitful discussions and peer review of most of the code, and my wife Nataliya Goncharuk for constant support. I also want to thank Anne Baanen, Johan Commelin, Nataliya Goncharuk, and Robert Y. Lewis for valuable comments on the draft versions of this paper and I thank my son Konstantin for finding lots of typos. I am also grateful to the anonymous referees for their valuable comments.
Cite AsGet BibTex
Yury Kudryashov. Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ITP.2022.23
https://doi.org/10.4230/LIPIcs.ITP.2022.23
Abstract
I formalize a version of the divergence theorem for a function on a rectangular box that does not assume regularity of individual partial derivatives, only Fréchet differentiability of the vector field and integrability of its divergence. Then I use this theorem to prove the Cauchy-Goursat theorem (for some simple domains) and bootstrap complex analysis in the Lean mathematical library. The main tool is the GP-integral, a version of the Henstock-Kurzweil integral introduced by J. Mawhin in 1981. The divergence theorem for this integral does not require integrability of the divergence.
Subject Classification
ACM Subject Classification
- Security and privacy → Logic and verification
- Mathematics of computing → Integral calculus
Keywords
- divergence theorem
- Green’s theorem
- Gauge integral
- Cauchy integral formula
- Cauchy-Goursat theorem
- complex analysis
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Mohammad Abdulaziz and Lawrence Paulson. An Isabelle/HOL formalisation of green’s theorem. J Autom Reasoning, 63:763-786, 2019. URL: https://doi.org/10.1007/s10817-018-9495-z.
- Felipe Acker. The missing link. The Mathematical Intelligencer, 18(3):4-9, June 1996. URL: https://doi.org/10.1007/BF03024304.
- Jeremy Avigad, Johannes Hölzl, and Luke Serafin. A formally verified proof of the central limit theorem. Journal of Automated Reasoning, 59(4):389-423, 2017. URL: https://doi.org/10.1007/s10817-017-9404-x.
-
Salomon Bochner. Integration von Funktionen, deren Werte die Elemente eines Vektorraumes sind. Fundamenta Mathematicae, 20, 1933.
- Sylvie Boldo, François Clément, and Louise Leclerc. A Coq formalization of the Bochner integral, 2022. URL: http://arxiv.org/abs/2201.03242.
- Benedetto Bongiorno. The Henstock-Kurzweil integral. In E. PAP, editor, Handbook of Measure Theory, chapter 13, pages 587-615. North-Holland, Amsterdam, 2002. URL: https://doi.org/10.1016/B978-044450263-6/50014-2.
-
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25, pages 378-388, Cham, 2015. Springer International Publishing.
-
Russel A. Gordon. The integrals of Lebesgue, Denjoy, Perron, and Henstock, volume 4 of Graduate Studies in Mathematics. American Mathematical Society, Providence, R.I, 1955.
- John Harrison. Formalizing basic complex analysis. In R. Matuszewski and A. Zalewska, editors, From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, volume 10(23) of Studies in Logic, Grammar and Rhetoric, pages 151-165. University of Białystok, 2007. URL: http://mizar.org/trybulec65/.
- John Harrison. Formalizing an analytic proof of the prime number theorem. Journal of Automated Reasoning, 43(3):243-261, 2009. URL: https://doi.org/10.1007/s10817-009-9145-6.
- The mathlib community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 367-381, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373824.
-
Jean Mawhin. Generalized multiple Perron integrals and the Green-Goursat theorem for differentiable vector fields. Czechoslovak Math. J., 31(106)(4):614-632, 1981.
-
Washek F. Pfeffer. The Riemann approach to integration, volume 109 of Cambridge Tracts in Mathematics. Cambridge University Press, Cambridge, 1993. Local geometric theory.
- Floris van Doorn. Formalized Haar Measure. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving (ITP 2021), volume 193 of Leibniz International Proceedings in Informatics (LIPIcs), pages 18:1-18:17, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.18.