Minkowski-Weyl theorem and convexity

Stream: mathlib4

[Stephan Maier]

Hi
I was looking at the various files in Analysis dealing with convexity hunting for the elementary theorems in convenxity such as the Minkowski-Weyl theorem, Radon's and Helly's theorem and Carathéodory's. I only found the latter, and there is no trace of a PI that suggests Minkowski-Weyl is going to b eimplemented. Do you have any idea if these basic convexity theorems are somewhere in the making?
Note: I need this only in passing for PL-topology, so just wondering.
Thanks, Stephan

[Johan Commelin]

I'm not aware of current work in this direction. cc @Yaël Dillies who knows the convexity library.

[Bhavik Mehta]

Yaël and I actually talked about some of these yesterday! They're currently working on conical hulls, but none of the others are being actively working on, as far as I know.

[Bhavik Mehta]

Actually, there's also this: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Convex/Radon.html

[Yaël Dillies]

Weyl-Minkowski was proved a few months back. Look for "fundamental theorem of polytope theory" on Zulip

[Yaël Dillies]

@Hyeokjun Kwon, are you still working on PRing this to mathlib? I am happy to take over if you don't have time anymore

[Stephan Maier]

Yaël Dillies said:

Hyeokjun Kwon, are you still working on PRing this to mathlib? I am happy to take over if you don't have time anymore

Hi
Thanks, I found it at https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Main.20Theorem.20of.20Polytope.20Theory/near/394635860.
May need a little rwriting as things are done over the real numbers, and inner prduct spaces, but I suspsect that is not necessary.
Let me know what is doing, or if I could do anything. Thanks!
Stephan

[Hyeokjun Kwon]

Yaël Dillies said:

Hyeokjun Kwon, are you still working on PRing this to mathlib? I am happy to take over if you don't have time anymore

I would be happy and grateful for you to take over to PR it to the Mathlib. I feel like I have dragged this way too long, I am sorry.

[Yaël Dillies]

No problem :smile: I will take over it

[Stephan Maier]

Bhavik Mehta said:

Actually, there's also this: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Convex/Radon.html

Thanks, overlooked it!