Yury G. Kudryashov (Jan 31 2022 at 20:38): 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?
Karl Palmskog (Feb 01 2022 at 09:09):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: Apr 19 2024 at 10:02 UTC