Stream: Miscellaneous

Topic: Green's theorem?

view this post on Zulip Yury G. Kudryashov (Jan 31 2022 at 20:38):

Hi, I'm writing a paper about my formalization of the divergence theorem for GP-integral (it seems that I've reinvented a wheel; I'm going to add proper references in a few days) and Bochner integral in Lean and applications to complex analysis.
Clearly, I want to reference any related work in Coq. Is there a version of the divergence theorem formalized in Coq (I'm only interested in rectangular boxes)? If yes, where can I find it? Which integral do you use? What are the assumptions on the function?

view this post on Zulip Karl Palmskog (Feb 01 2022 at 09:09):

Green's theorem is not known to have any Coq formalization:

The most active project doing analysis in Coq these days is probably #math-comp analysis - you could try asking in that stream about where they are w.r.t. integrals and their applications.

Last updated: Aug 19 2022 at 20:03 UTC