Hi, I asked this question in #Miscellaneous but I was told that it's better to ask it in this stream.

I'm writing a paper about my formalization of the divergence theorem for GP-integral (first introduced here) 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, not in fancy domains like in Isabelle)? If yes, where can I find it? Which integral do you use? What are the assumptions on the function?

Not that I am aware of but I am not sure I did my homework properly; the MILC people may know better https://lipn.univ-paris13.fr/MILC/.

Are they in this chat or I should email one of them?

might be safest to email, I don't think I've seen them on the Zulip

I don't remember having seen them hanging around

(oh, Sylvie is actually subscribing)

Last updated: Feb 05 2023 at 08:28 UTC