1 Search Results for "Kudryashov, Yury"

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-dev.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}
}
  • Refine by Author
  • 1 Kudryashov, Yury

  • Refine by Classification
  • 1 Mathematics of computing → Integral calculus
  • 1 Security and privacy → Logic and verification

  • Refine by Keyword
  • 1 Cauchy integral formula
  • 1 Cauchy-Goursat theorem
  • 1 Gauge integral
  • 1 Green’s theorem
  • 1 complex analysis
  • Show More...

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact