Re: [isabelle] New in the AFP: Formal Puiseux Series



On 26/02/2021 17:06, Mohammad Abdulaziz wrote:
> I recall that back in Logrono you claimed to know how you can generalise
> the approach of partitions of unity to handle integrals defined on
> manifolds with corners, when you were suggesting improvements to the
> formalisation of Green's theorem. I disagreed as this sounded too
> complicated for me. Did you actually try to do that and find it is too
> complicated or why did you change your mind?

I vaguely recall that that was how I was taught it, but I don't know for
sure. It might be more complicated though. (Intuitively, of course, it
seems obvious: just deform the corners by some epsilon to make them
smooth; if the epsilon goes to 0 the change vanishes – but that's
probably hardly the most elegant way to do it)

In any case, I am probably not a good person to ask such things because
I know very little about… whatever branch of mathematics this is.

Lean does seem to have "manifolds with corners":
https://leanprover-community.github.io/mathlib_docs/geometry/manifold/smooth_manifold_with_corners.html

Perhaps you could ask Sébastien Gouëzel (who did it) on his perspective
on this. I hear he also has a soft spot for Isabelle. :)

Manuel



Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.