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?

Green's theorem is not known to have any Coq formalization: https://madiot.fr/coq100#21

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: Jun 05 2023 at 09:01 UTC