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

However, would this be enough to claim one has shown the Isoperimetric
Theorem? To me, that sounds dangerously like making the theorem true by
defining things the right way.

I agree that this would be very close to more or less assuming the theorem.

> I think that for a "proper" proof of it,
> one should also show that Minkowski coincides with other measures of
> "surface area", such as the length of a rectifiable curve in R^2, or the
> surface integral for manifolds in higher dimensions (the latter of which
> gets ugly as soon as you want to allow your objects to have sharp corners).

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?

For the length of a rectifiable curve, i.e. a curve whose length is well-defined, you can reuse the version of line integrals developed for Green's theorem, which is based on the HK integrals, for which some theory exists. Showing that this is equivalent to Minkowski's measure is nontrivial, nonetheless.


On 24/02/2021 17:39, Freek Wiedijk wrote:
Hi Wenda,

We may ask Freek for a longer list :-)

Let's finish the first one first :-)

That is: at least until we are at 99 theorems.  When that
happens, I would like to organise a workshop titled

   "I got 99 theorems, but Fermat ain't one"
where I'll ask the most prolific contributors to the top
100 list to present a talk.


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