search

leanprover-community / mathlib4

The math library of Lean 4
https://leanprover-community.github.io/mathlib4_docs
Apache License 2.0
1.18k stars 253 forks source link

The Shapley-Folkman lemma #14427

Open YaelDillies opened 3 days ago

YaelDillies commented 3 days ago

The Shapley-Folkman lemma is a convex analysis result standard in the economics literature. In contrast, it is basically unheard of in mathematics.

The proof is elementary, and very similar to the proofs of Carathéodory's and Radon's theorems, which should serve as inspiration.

This issue existed in mathlib3 as https://github.com/leanprover-community/mathlib/issues/18135.

ndcroos commented 3 days ago

Hi Yaël, can you assign this to me?