Yury G. Kudryashov (Feb 02 2022 at 10:39): 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!
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.
Manuel Eberl (Feb 02 2022 at 10:56):Ah, right, Euler–MacLaurin in the AFP, that's another result that involves integrals.
Manuel Eberl (Feb 02 2022 at 10:58):And the Laplace transform
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.
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.
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.
Manuel Eberl (Feb 02 2022 at 11:02):Plus, there's also a lot of complex analysis in HOL-Complex_Analysis.
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 ). 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: Apr 16 2024 at 16:19 UTC