Yury G. Kudryashov (Feb 02 2022 at 05:09): Yury G. Kudryashov (Feb 02 2022 at 05:09):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?
Reynald Affeldt (Feb 02 2022 at 06:24):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/.
Yury G. Kudryashov (Feb 02 2022 at 07:28):Are they in this chat or I should email one of them?
Karl Palmskog (Feb 02 2022 at 07:30):might be safest to email, I don't think I've seen them on the Zulip
Reynald Affeldt (Feb 02 2022 at 07:30):I don't remember having seen them hanging around
Reynald Affeldt (Feb 02 2022 at 07:32):(oh, Sylvie is actually subscribing)
Last updated: Apr 20 2024 at 05:01 UTC