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



Relatedly, I think it would be great to have some geometric measure
theory in Isabelle, e.g. the Minkowski and Hausdorff measures.

Minkowski and Hausdorff coincide for reasonably nice sets, and for
curves, Haussdorff is just the length of rectifiable curves and can be
shown to coincide with the integral for smooth curves fairly easily (I
think).

The situation in higher dimensions is probably complicated though…

Manuel


On 26/02/2021 17:06, Mohammad Abdulaziz wrote:
> 
>> 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.
> 
> Mohammad
> 
>>
>> 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.
>>>
>>> Freek
>>>
>>
> 

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



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