Isoperimetric Inequality

Stream: maths

[Yaël Dillies]

So I nerdsniped myself again. Now that Krein-Milman hit mathlib, I was reading more of Barry Simon, Convexity, and I thought that Brunn-Minkowski would be a very nice statement to formalize. Then I read that it implied the isoperimetric inequality (the sphere maximizes volume among shapes of fixed surface area) rather directly, which is one of the last three standing items on Freek's list! Hence I was wondering whether the isoperimetric inequality/Brunn-Minkowski was within reach from the mathlib measure theory side of things.

[Yaël Dillies]

What do our resident measure theorists think? @Yury G. Kudryashov, @Jason KY.

[Sebastien Gouezel]

I'm pretty sure we have everything that is needed for Brunn-Minkowski (and even Prekopa-Leindler). For the isoperimetric inequality, it depends how you want to phrase it (what is the "perimeter" in general?). I don't even know if the isoperimetric inequality holds when taking as the perimeter the n-1 Hausdorff measure of the boundary, but we have the Hausdorff measure.

[Kevin Buzzard]

One of those three missing theorems, the Fair Games theorem, has been done in Lean. Fermat's Last Theorem will be quite a challenge, but Freek has suggested that 99% would be a good enough reason to have a conference celebrating, so I would definitely encourage you to do the isoperimetric inequality!

[Yaël Dillies]

Guess I found my next project then!

[Yaël Dillies]

I haven't checked whether it is directly needed for Brunn-Minkowski, but I am now working on Minkowski-Carathéodory. This is like Carathéodory, except that we restrict to convex combinations of extreme points.

[Patrick Stevens]

If you'd like my Part III Probabilistic Combinatorics notes from 2016 (lectured by Bollobas), you're welcome to them - Prékopa-Leindler is Theorem 3 from them, and a number of isoperimetric inequalities (on the sphere and the Gaussian surface) and concentration of measure phenomena are deduced by Brunn-Minkowski and Prékopa-Leindler. But my notes are not the best, I barely understood the course material

[Yaël Dillies]

That would be greatly appreciated! It is funny to me that Probabilistic Combinatorics and Combinatorics both prove an isoperimetric inequality.

[Floris van Doorn]

I just saw that the Isoperimetric Theorem is formalized in HOL Light, at least for $n = 2$ (i.e. the relation between the length of a curve in the plane and the area it encloses). This is problem 43 on Freek's list, and was the last unsolved problem on the list besides Fermat's Last Theorem.

[Kevin Buzzard]

So what are we waiting for? ;-)

[Kevin Buzzard]

Oh yeah, the port

[Yaël Dillies]

In fact, we were very concretely waiting for docs#intrinsic_interior to become a thing, which it did a few days ago!

[Yaël Dillies]

I am now going through my old convexity branches to see what's ready for mathlib.

[Kevin Buzzard]

Oh no I mean FLT!

[Ruben Van de Velde]

Kevin's not so secret ten year plan?

[Eric Rodriguez]

Yaël Dillies said:

In fact, we were very concretely waiting for docs#intrinsic_interior to become a thing, which it did a few days ago!

(this 404s)

[Kevin Buzzard]

Are the docs not being updated? Yury also recently reported a broken doc link from a new PR

[Eric Rodriguez]

yeah, the doc-gen build seems to be from mathlib 4 days ago (https://github.com/leanprover-community/mathlib/tree/9003f28797c0664a49e4179487267c494477d853)

[Yaël Dillies]

Bleeding edge mathlib do be bleeding :frown:

[Henrik Böving]

Kevin Buzzard said:

Are the docs not being updated? Yury also recently reported a broken doc link from a new PR

Correct, as per usual the issue is that std4 is not mathlib4 master compatible and thus breaks the build since I have to run lake update during the automatic CI build which incidentally also pulls in std4 latest version

[Henrik Böving]

Oh

[Eric Rodriguez]

this is for docgen3 Henrik

[Henrik Böving]

The other doc-gen is being blamed fo once!

[Mario Carneiro]

@Henrik Böving can we maybe do something about that? Are we missing a lake feature or what?

[Henrik Böving]

Well if I could tell lake "only update doc-gen4 and its transitive deps" then it would not implicitly do the std4 and aesop update yeah.

[Eric Rodriguez]

Any updates on this? Seems that docgen is currently stuck..

[Yaël Dillies]

@Bryan Gin-ge Chen, do you think you could set doc-gen back on track?