Stream: General

Topic: Divergence thm and Cauchy-Goursat


view this post on Zulip Yury G. Kudryashov (Feb 02 2022 at 10:39):

Hi, I'm writing a paper about my formalization of the divergence theorem for the GP-integral (first introduced in 1981) and Bochner integral in Lean and applications to complex analysis.
Clearly, I want to reference any related work in Isabelle but I'm not fluent in Isabelle and I'm bad in searching Isabelle docs. I'm aware of the formalization of the Green's theorem, including the case of non-rectangular domains, in Isabelle. Could you please tell me what are the other relevant projects? Thank you!

view this post on Zulip Manuel Eberl (Feb 02 2022 at 10:56):

Not sure what you're looking for exactly. The Henstock–Kurzweil integral and the Bochner integral are all part of Isabelle's standard library (HOL-Analysis to be exact). I can dig you up a reference for that later if you want.

Not sure how Green's theorem is relevant to you – are you just interested in any result that includes integrals in its statement? Not sure how much more of that there is, other than Green. There are a lot of AFP entries and some things in the standard library that make extensive use of integrals, but don't actually have them in the final result. But that is perhaps too far away to still be related.

view this post on Zulip Manuel Eberl (Feb 02 2022 at 10:56):

Ah, right, Euler–MacLaurin in the AFP, that's another result that involves integrals.

view this post on Zulip Manuel Eberl (Feb 02 2022 at 10:58):

And the Laplace transform

view this post on Zulip Manuel Eberl (Feb 02 2022 at 10:59):

And the Akra–Bazzi theorem technically also has an integral in its statement, but there's nothing crazy going on there.

view this post on Zulip Manuel Eberl (Feb 02 2022 at 11:01):

The (analytic) proof that ζ(3) is irrational has a lot of manipulation of integrals, including double and triple integrals.

view this post on Zulip Manuel Eberl (Feb 02 2022 at 11:01):

And one result from the library that you may be interested in is the multivariate change of variables for the Lebesgue integral.

view this post on Zulip Manuel Eberl (Feb 02 2022 at 11:02):

Plus, there's also a lot of complex analysis in HOL-Complex_Analysis.

view this post on Zulip Yury G. Kudryashov (Feb 02 2022 at 11:08):

I formalized a version of the divergence theorem for a non-standard gauge integral that implies the Cauchy-Goursat theorem with standard assumptions (complex differentiability, not C1C^1). It's one of my first papers on formalization and I'm still not completely sure what I should or should not reference in a paper about this. Clearly, formalization of the Green's formula and complex analysis are relevant projects.


Last updated: Aug 15 2022 at 04:16 UTC