Stream: Mirror: Isabelle Users Mailing List

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


view this post on Zulip Email Gateway (Feb 24 2021 at 14:18):

From: Lawrence Paulson <lp15@cam.ac.uk>
I am happy to announce another entry from Manuel Eberl, who is one of our most prolific contributors:

Formal Puiseux series are generalisations of formal power series and formal Laurent series that also allow for fractional exponents. … This entry defines these series including their basic algebraic properties. Furthermore, it proves the Newton–Puiseux Theorem, namely that the Puiseux series over an algebraically closed field of characteristic 0 are also algebraically closed.

You will find it online at https://www.isa-afp.org/entries/Formal_Puiseux_Series.html

Many thanks, Manuel!

Larry

view this post on Zulip Email Gateway (Feb 24 2021 at 15:00):

From: Manuel Eberl <eberlm@in.tum.de>
Please do excuse the frivolous remark, but I cannot resist pointing out
that with this, we are now exactly one theorem behind HOL Light on Freek
Wiedijk's list.

https://www.cs.ru.nl/~freek/100/

Perhaps someone feels inspired to formalise some more things from there
so that we will finally pull ahead? Some geometry perhaps? Or port
something over from HOL Light?

:)

Manuel
smime.p7s

view this post on Zulip Email Gateway (Feb 24 2021 at 16:10):

From: Wenda Li <wl302@cam.ac.uk>
In fact, many of the ’newer’ theorems that appears at the bottom of Freek’s website but don’t count as the 100 theorems are also available in Isabelle. We may ask Freek for a longer list :-)

Wenda

view this post on Zulip Email Gateway (Feb 24 2021 at 16:15):

From: Manuel Eberl <eberlm@in.tum.de>
I know, I already compiled a list of those and intend to publish it soon
(as soon as I figure out how to properly do syntax highlighting).

Manuel
smime.p7s

view this post on Zulip Email Gateway (Feb 24 2021 at 16:39):

From: Freek Wiedijk <freek@cs.ru.nl>
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

view this post on Zulip Email Gateway (Feb 26 2021 at 15:43):

From: Manuel Eberl <eberlm@in.tum.de>
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).

Manuel
smime.p7s

view this post on Zulip Email Gateway (Feb 26 2021 at 15:52):

From: Manuel Eberl <eberlm@in.tum.de>
For the curious, here is a slightly updated version of Gerwin's "Top 100
in Isabelle" list that also includes the additional theorems mentioned
on Freek's web site:

https://pruvisto.github.io/100isabelle/

Note that this is just an experiment for now (I wanted to see if Github
pages can be used for this purpose – turns out it can't). It will be
moved somewhere else eventually once we've figured out the syntax
highlighting, and replace Gerwin's site.

Manuel
smime.p7s

view this post on Zulip Email Gateway (Feb 26 2021 at 16:06):

From: Mohammad Abdulaziz <mohammad.abdulaziz8@gmail.com>

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

view this post on Zulip Email Gateway (Feb 26 2021 at 16:16):

From: Manuel Eberl <eberlm@in.tum.de>
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
smime.p7s

view this post on Zulip Email Gateway (Feb 26 2021 at 16:27):

From: Manuel Eberl <eberlm@in.tum.de>
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
smime.p7s

view this post on Zulip Email Gateway (Feb 26 2021 at 16:27):

From: Mohammad Abdulaziz <mohammad.abdulaziz8@gmail.com>

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

You are right, we should probably ask him. A quick review of that page suggest they did not solve
the problem we are discussing though, i.e. defining integrals on such manifolds and using partition
of unities arguments to reason about them.

Mohammad

view this post on Zulip Email Gateway (Feb 26 2021 at 16:28):

From: Freek Wiedijk <freek@cs.ru.nl>
Hi Manuel,

Not sure what "Fair Games" actually is, but my best guess is that it
refers to the Optional Stopping Theorem.

Yes, that's my guess too. I never managed to reach the
people who drew up the original top 100 list, so I never
could ask.

Freek


Last updated: Jul 15 2022 at 23:21 UTC