Stream: math-comp analysis

Topic: Green's theorem?


view this post on Zulip 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?

view this post on Zulip 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/.

view this post on Zulip Yury G. Kudryashov (Feb 02 2022 at 07:28):

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

view this post on Zulip Karl Palmskog (Feb 02 2022 at 07:30):

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

view this post on Zulip Reynald Affeldt (Feb 02 2022 at 07:30):

I don't remember having seen them hanging around

view this post on Zulip Reynald Affeldt (Feb 02 2022 at 07:32):

(oh, Sylvie is actually subscribing)


Last updated: Aug 11 2022 at 03:02 UTC