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

I think that's definitely in reach.

The only two ones that are still missing are the "Fair Games Theorem"
and the Isoperimetric Theorem.

Not sure what "Fair Games" actually is, but my best guess is that it
refers to the Optional Stopping Theorem. We do have a big amount of
probability theory in Isabelle/HOL, and I think there is even some
martingale theory in some AFP entry. The proof looks fairly simple, as
long as the necessary background theory is there.

The Isoperimetric Theorem is a bit more tricky because to even state it,
one needs a way to talk about the perimeter of a set (or in higher
dimensions, the "surface area"), and there are a number of different
approaches, some of which are more general than others.

The best approach, I think, would be to define the Minkowski measure and
prove the Brunn–Minkowski inequality in R^n (all very doable with some
basic measure theory; I even have some material about these things lying
around somewhere already). The isoperimetric inequality for R^n in terms
of the Minkowski measure follows very easily then.

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 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).


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.