2026-07-23T18:07:46Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16732 2024-03-06T10:58:10Z ddc:004 open_access

Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean Kudryashov, Yury divergence theorem Green’s theorem Gauge integral Cauchy integral formula Cauchy-Goursat theorem complex analysis 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Yury Kudryashov 2022 Is Part Of LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2022.23 urn:nbn:de:0030-drops-167326 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.23 eng https://creativecommons.org/licenses/by/4.0/legalcode