DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2022.23

Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean

Authors: Yury Kudryashov

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{kudryashov:LIPIcs.ITP.2022.23,
  author =	{Kudryashov, Yury},
  title =	{{Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{23:1--23:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.23},
  URN =		{urn:nbn:de:0030-drops-167326},
  doi =		{10.4230/LIPIcs.ITP.2022.23},
  annote =	{Keywords: divergence theorem, Green’s theorem, Gauge integral, Cauchy integral formula, Cauchy-Goursat theorem, complex analysis}
}

Search Results

Documents authored by Kudryashov, Yury

Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean

Abstract

Cite as

Thanks for your feedback!

Could not send message