Zulip Chat Archive

Stream: maths

Topic: Brunn-Minkowski Inequality + Theory

Jineon Baek (Jan 20 2025 at 02:19):

Me @Jineon Baek and @Hyojae Lim, @Jihoon Hyun are now working slowly on Brunn-Minkowski Inequality. A consequence of this would be the Isoperimetric Inequality, which is one of the still-missing theorems in Wiedijk's 100-theorem list. Another motivation comes from formalizing the resolution of the moving sofa problem discussed here.

Anyone interested in joining the effort? Right now, we have a private GitHub repository. We could coordinate what each of us would do through this thread. For your information,

  • @Hyojae Lim is now working on 1-D version of BM inequality that is needed in the induction step, following a sketch by Tao.
  • @Jineon Baek is now working on the Prékopa-Leindler inequality that generalizes BM inequality, following the same sketch as above.
  • @Jihoon Hyun is now working on using Jordan curve theorem + rectifiable curves to calculate the area trapped inside a rectifiable curve using Green's theorem.

If you join, you could start by defining the support function, mixed volume, surface area measure of a convex body K, and show their multi-linearity with Mikowski sum etc.

Michael Rothgang (Jan 20 2025 at 10:39):

Just a comment from the peanut gallery: you are assuming the Jordan curve theorem, right? (Proving that on its own would be a great addition, but I believe is also a project that could take many months.)

Jineon Baek (Jan 20 2025 at 11:16):

Michael Rothgang Thanks, this is good to know. We didn't know that Jordan curve theorem did not exist. We are still on a very early stage and needs research on what is already done in mathlib and not.

Jihoon Hyun (Jan 20 2025 at 11:19):

Actually, there is no good definition of curves yet, if I looked correctly.

Michael Rothgang (Jan 20 2025 at 14:45):

(I believe Mario Carneiro made some Mizar export work: generating a crazy ball of Lean code from the Mizar proof that was not ... well readable, but worked. For such a project, stating the Jordan Curve theorem as a sorry and moving on feels fair. Nobody doubts the result is true.)

Jaemin Choi (Jan 20 2025 at 14:45):

Hi! I just saw @Jineon Baek's invitation and would love to join.

Jihoon Hyun (Jan 22 2025 at 13:56):

Jihoon Hyun 말함:

Actually, there is no good definition of curves yet, if I looked correctly.

There is no 'curve', but there is a docs#Path . I should've searched a bit more.

Last updated: May 02 2025 at 03:31 UTC