Main Theorem of Polytope Theory

Stream: Is there code for X?

[Hyeokjun Kwon]

Hello, I am planning to do Lean as part of my Masters dissertation next year, hopefully something not already proved in Mathlib.
My future supervisor has suggested me to work on the Main Theorem of Polytope Theory which states:
Let 𝑋 be a closed convex subset of ℝ^𝑑. Then:
• 𝑋 is a 𝑉-polytope if it is the convex hull of a finite point set.
• 𝑋 is an 𝐻-polytope if it is the intersection of finitely many half spaces.

Theorem : Every 𝑉-polytope is an 𝐻-polytope, and every compact 𝐻-polytope is a 𝑉-polytope.

Is this theorem already part of the Mathlib? Thank you very much in advance.

[Johan Commelin]

Welcome! No, I don't think this is in mathlib yet. But let's ping @Yaël Dillies, our convexity expert.

[Yaël Dillies]

Ahah! I'm glad this denomination sticked around. I have the statement and part of the proof on a branch. I got stuck at finding the right way of defining polytopes, because I was lacking overview of the subject.

[Yaël Dillies]

I know more now, so probably I can get you the definitions right and leave you to complete the proof. What's your time frame?

[Kevin Buzzard]

One of the hardest parts of Lean is getting the definitions into a Lean-friendly state, so if Yael can do the definitions then perhaps Hyeokjun can take over from there?

[Hyeokjun Kwon]

Thank you. I will be writing my dissertation from September to April next year so there is some time before the start of it. My supervisor and I are currently at the brainstorming stage where we are still trying to decide which area/theorem to work on. (So probably I will be posting more questions here in the future) If we decides to go for this theorem, I would be very grateful to get help!

[Yaël Dillies]

Okay great! I most definitely can get the definitions right by then.

[Louis Theran]

Kevin Buzzard said:

One of the hardest parts of Lean is getting the definitions into a Lean-friendly state, so if Yael can do the definitions then perhaps Hyeokjun can take over from there?

Informally, the lean friendly definition is probably that a V-polytope is a compact convex set in a finite-dimensional Euclidean space that has finitely many extreme points and that an H-polytope is a compact intersection of finitely many half-spaces. Along the way, you'd also want the definition of the polar dual of a convex set. Is this in mathlib?

[Moritz Firsching]

I'm also interested in polytopes!

[Violeta Hernández]

Is there anything wrong with the more usual definition? Namely, a convex polytope is the convex hull of a finite set

[Violeta Hernández]

Is it not the correct generality? It so, what is it? Is there even a more general definition in use?

[Hyeokjun Kwon]

@Yaël Dillies , I wanted to share that I and my supervisor, @Louis Theran have decided the main theorem of polytope theory for my dissertation. If I can get the help with the definitions, I would be very happy :)

[Yaël Dillies]

Nice, @Hyeokjun Kwon! I'm at the beach until tomorrow, but expect the definitions some time next week.

[Hyeokjun Kwon]

I have managed to prove the theorem earlier than expected. Here is the github repo! : https://github.com/Jun2M/MasterDiss/

[Johan Commelin]

Congratulations!

[Kevin Buzzard]

So do you hand in the Masters dissertation now and take 6 months off? :-)

[Scott Morrison]

PRing to Mathlib may take the rest of the time. :-)