Zulip Chat Archive

Stream: new members

Topic: Shapley-Folkman lemma


Peter Hansen (Mar 29 2023 at 09:21):

It is suggested on the mathlib repo that a good first project could be to prove the Shapley-Folkman lemma

https://github.com/leanprover-community/mathlib/issues/18135

The proof is supposedly similar to that of Carathéodory's (convex hull) Theorem

Let ERlE \subset \mathbb{R}^l.
Let xconv(E)\mathrm{x} \in \operatorname{conv}(E), where conv(E)\operatorname{conv}(E) denotes the convex hull of EE.
Then x\mathbf{x} is a convex combination of affinely independent points of EE.
In particular, x\mathbf{x} is a convex combination of at most l+1l+1 points of EE.

The Lean version of the theorem assumes a general vector space as an instance of [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E]. The lack of any reference to the dimension of the vector space is a bit eerie to a novice like me. Since the Shapley-Folkman lemma assumes a finite dimensional vector space, I thought a good exercise could be to show the "In particular, ..." proposition

import analysis.convex.caratheodory

open_locale big_operators

universe u
variables {𝕜 : Type*} {E : Type u} {s : set E}
variables [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [finite_dimensional 𝕜 E]

open finite_dimensional

lemma affine_independent_and_dimensions (ι : Type*) (_ : fintype ι) (ai : ι  E)
  (af : affine_independent 𝕜 ai) : fintype.card ι  finrank 𝕜 E + 1 :=
begin
  have hfd : finrank 𝕜 (vector_span 𝕜 (set.range ai)) + 1  finrank 𝕜 E + 1,
  { apply add_le_add_right,
    exact submodule.finrank_le _ },
  apply le_trans' hfd,
  generalize h : fintype.card ι = n,
  cases n,
  { exact zero_le _ },
  { apply nat.succ_le_succ,
    exact (affine_independent_iff_le_finrank_vector_span 𝕜 ai h).mp af }
end

theorem particular_caratheodory {x : E} (hc : x  convex_hull 𝕜 s) :
   (ι : Sort (u+1)) (_ : fintype ι), by exactI  (z : ι  E) (w : ι  𝕜) (hss : set.range z  s)
  (hai : affine_independent 𝕜 z) (hfi : fintype.card ι  finrank 𝕜 E + 1)
  (hw :  i, 0 < w i),  i, w i = 1   i, w i  z i = x :=
begin
  obtain ι, hf, ai, li, hss, hai, hw, h₁ := eq_pos_convex_span_of_mem_convex_hull hc,
  exact ι, hf, ai, li, hss, hai, affine_independent_and_dimensions _ _ _ hai, hw, h₁
end
  1. Is the Lean statement correct? Does it correctly correctly state the "particular version" of Carathéodory's Theorem?
  2. Any comments on my code? This is first my attempt of doing real mathematics, so any critique would be appreciated.

Peter Hansen (Apr 01 2023 at 13:16):

I should probably have asked about specific issues I’m having with proving the lemma. I’ll try to be more concrete in the future. I have not made much progress with the lemma since the last post. I’m trying to prove the following:

import analysis.convex.caratheodory

open_locale big_operators pointwise

universe u
variables {𝕜 : Type*} {E : Sort (u+1)} {S : set E}
variables [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E]

lemma convex_n_add (n : ) (s : fin n  set E) :
  convex_hull 𝕜 ( x, s x) =  x, convex_hull 𝕜 (s x) :=
begin
  induction n with n ih,
  { exact convex_hull_singleton 0 },
  rw [fin.sum_univ_succ, fin.sum_univ_succ, convex_hull_add, ih (λ x, s x.succ)]
end

lemma step1 (m : ) (S_i : fin m  set E) (S : set E)
(h :  i, S_i i = S) (s : E) (hs : s  convex_hull 𝕜 S) :
 (y_i : fin m  E), (s =  i, y_i i)  ( i,
y_i i  convex_hull 𝕜 (S_i i)  ( (F : Sort (u+1)) [fintype F] (y_ij : F  E) (a_ij : F  𝕜),
by exactI ( j, 0 < a_ij j)  ( j, a_ij j = 1)  ( j, a_ij j  y_ij j = y_i i))) :=
begin
  rw [h, convex_n_add, set.mem_finset_sum] at hs,
  rcases hs with y_i, h₂, h₃⟩,
  refine y_i, eq_comm.mp h₃, _⟩,
  intro I,
  fconstructor,
  exact h₂ (finset.mem_univ I),
  specialize h₂ (finset.mem_univ I),
  obtain F, Fa, y_ij, a_ij, _, _, h₆, h₇, h₈ := eq_pos_convex_span_of_mem_convex_hull h₂,
  exact F, Fa, y_ij, a_ij, h₆, h₇, h₈
end

lemma step2 (m : ) (S_i : fin m  set E) (S : set E)
  (h :  i, S_i i = S) (s : E) (hs : s  convex_hull 𝕜 S)
  (he :  i, (S_i i).nonempty) :
   (m_i: fin m  Sort (u+1))
  (mf_i:   (i : fin m), fintype (m_i i))
  (y_ij :  (i : fin m), (m_i i)  E)
  (a_ij :  (i : fin m), (m_i i)  𝕜), by exactI
  ( i j, (a_ij i) j > 0) 
  ( i j, (y_ij i) j  (S_i i)) 
  ( i,  j, (a_ij i) j = 1) 
  (s =  i j, (a_ij i) j  (y_ij i) j) :=
begin
  rw [h, convex_n_add, set.mem_finset_sum] at hs,
  rcases hs with y_i, h₂, h₃⟩,
  sorry,
end

I believe I have shown in step 1 that there exists (yi)iI(y_i)_{i \in I} such that s=i=1myis=\sum_{i=1}^m y_i and that for all iIi\in I there exist (yi,j)jJ(y_{i,j})_{j\in J} and (ai,j)jJ(a_{i,j})_{j\in J} such that yi=j=1aijyijy_i=\sum_{j=1} a_{ij} y_{ij}. The problem in step 2 is that I don’t now how to reason about some arbitrary ii in S=i=1mSiS=\sum_{i=1}^m S_i. How do I do that?

Eric Wieser (Apr 01 2023 at 13:23):

convex_n_add should follow easily from docs#convex_hull_add using docs#map_sum

Yaël Dillies (Apr 01 2023 at 13:24):

Sorry, I meant to have a look at your code but I was on the move! I shall give some attention tonight.

Peter Hansen (Apr 01 2023 at 14:05):

That part I did manage to show :) I tried to use exactly those two theorems you mentioned, but I could not get map_sum to work.
Instead I resorted to induction over nn with convex_hull_add. I guess I should have included it in my post ... I'm a bit unsure what exactly a mwe is.

Peter Hansen (Apr 01 2023 at 14:06):

Yaël Dillies said:

Sorry, I meant to have a look at your code but I was on the move! I shall give some attention tonight.

That would be greatly appreciated :) Thank you.

Peter Hansen (May 02 2023 at 18:29):

So I made some small progress with the Shapley-Folkman lemma, but I quickly ran into a major obstacle: Most of proofs of the lemma uses the notion of the conical hull of a set SRnS \subset \mathbb{R}^n, but I believe this does not yet exist in mathlib.
The hull is formed by intersecting all convex cones containing SS and appending 0 to it.
I tried defining it myself:

import analysis.convex.cone.basic

open set

variables {𝕜 E : Type*}
variables (𝕜) [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E]

def conical_hull : closure_operator (set E) :=
closure_operator.mk'
(λ s,  (t : convex_cone 𝕜 E) (hst : s  t) (hsa : convex_cone.pointed t), t)
(λ i b h, Inter_mono $ λ q, Inter₂_mono' $ λ d p, trans h d, p, rfl.subset⟩)
(λ g, subset_Inter $ λ l, subset_Inter₂ $ λ h s, h)
(λ x, Inter_mono $ λ h, Inter₂_mono' $ λ a p, λ z w, mem_Inter₂.mp w h a h (mem_range_self p),
Exists.intro p rfl.subset⟩)

Is this a reasonable definition? At the moment, conical_hull 𝕜 (s : set E) has type set E. I think it would be more natural if it had type convex_cone 𝕜 E. I use an auxiliary function, that turns a set into convex cone using the above hull. How would you go about defining the hull?

Eric Wieser (May 04 2023 at 13:36):

What goes wrong if you just replace set E with convex_cone k E?

Peter Hansen (May 04 2023 at 15:09):

Eric Wieser said:

What goes wrong if you just replace set E with convex_cone k E?

Thank you for taking your time to reply.
The closure operator is function f : α → α, so if I replace set E with convex_cone k E, it no longer takes an arbitrary set as input.

Eric Wieser (May 04 2023 at 15:11):

Perhaps I should have taken the time to look at docs#closure_operator first...

Eric Wieser (May 04 2023 at 15:13):

Does the following work?

def conical_hull (s : set E) : convex_cone 𝕜 E :=
 (t : convex_cone 𝕜 E) (hst : s  t) (hsa : convex_cone.pointed t), t

Eric Wieser (May 04 2023 at 15:14):

You then probably want to follow up with proving that this forms a docs#galois_insertion, like we do with docs#submodule.gi

Yaël Dillies (May 04 2023 at 16:03):

Yeah, don't bother with closure_operator

Peter Hansen (May 04 2023 at 18:06):

Eric Wieser said:

Does the following work?

def conical_hull (s : set E) : convex_cone 𝕜 E :=
 (t : convex_cone 𝕜 E) (hst : s  t) (hsa : convex_cone.pointed t), t

It works, thank you, but I thought it would be a good idea to get access to all the bells and whistles of the closure operator. But if you and Yaël Dillies believe it is not worth the trouble, I guess I will drop it.

Eric Wieser (May 04 2023 at 18:16):

I think the bells and whistles you want should be encapsulated by galois_insertion (assuming it's true!)

Yaël Dillies (May 04 2023 at 18:33):

closure_operator is something I helped shape when I was a very beginner in Lean two years ago and, in retrospect, it is quite bad. Use Galois insertions directly.

Eric Wieser (May 04 2023 at 20:16):

Eric Wieser said:

convex_n_add should follow easily from docs#convex_hull_add using docs#map_sum

I've PR'd this and many similar lemmas as #18943

Peter Hansen (May 07 2023 at 21:57):

I'm beginning to doubt it forms a galois_insertion and I'm not sure how to deal with it. If I remove the constraint that the conical hull includes 0 (and maybe just call it the 'minimal convex cone'), then everything nicely resembles the case of the span of a submodule.

def minimal_convex_cone (s : set E) : convex_cone 𝕜 E :=
 (t : convex_cone 𝕜 E) (hst : s  t), t

I could then append 0 to the result (which is still a convex cone) to form the conical hull. But this seems kinda awkward and I'm not sure how much of a utility the galois insertion will be. It also seems a bit odd that the conical hull of is 0 (also an issue in the original definition of 'conical_hull').

Any good ideas of what to do next?

Kevin Buzzard (May 07 2023 at 22:46):

The subgroup generated by the empty set is {1}, and there's still a Galois insertion there

Peter Hansen (May 08 2023 at 01:32):

When you say that there is Galois insertion, are you referring to Eric Wieser's definition of the conical hull

def conical_hull (s : set E) : convex_cone 𝕜 E :=
 (t : convex_cone 𝕜 E) (hst : s  t) (hsa : convex_cone.pointed t), t

or my definition of a minimal convex cone

def minimal_convex_cone (s : set E) : convex_cone 𝕜 E :=
 (t : convex_cone 𝕜 E) (hst : s  t), t

Because I have shown a Galois insertion in the latter case. I was just wondering how useful it is to say anything about the actual conical hull.

Kevin Buzzard (May 08 2023 at 07:54):

Oh I'm not following closely, my comment was just that a functor sending an empty thing to a nonempty thing should neither be thought of as strange nor as a blocker for it being an adjoint (because all of this is just a special case of adjoint functors)

Nick Decroos (Jul 10 2024 at 10:15):

Hi all, I am working on the Shapley-Folkman lemma as a first project. I need some help in the statement of the lemma.

There are different statements of the lemma in the literature (aside: one version is for compact sets, which could also be formalized; like Analysis/Convex/Radon.lean also has different versions of Helly's thorem). The version of the SF lemma that I've choosen to formalize is the one in https://en.wikipedia.org/wiki/Shapley%E2%80%93Folkman_lemma, below "The lemma may be stated succinctly as". I've choosen this version, because it seemed easier to formalize.

The SF lemma is supposed to be proven in a similar way as Caratheodory's theorem and Radon's theorem, according to the description of the issue on Mathlib4. I'm not sure if this version would be proven in a similar way. So I am not sure if this is the right path to prove this lemma.

So my problem with this code is that in the line convexHull 𝕜 (Σ i ∈ Finset.range N Q i)... I get unexpected token '∈'; expected ','

import Mathlib.Data.Finset.Basic
import Mathlib.Data.Set.Finite
import Mathlib.Analysis.Convex.Basic
import Mathlib.Analysis.Convex.Combination
import Mathlib.Data.Set.Card
import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
import Mathlib.Topology.Separation

namespace Convex

open Fintype Finset Set

universe u

-- Assume that we have a field 𝕜, a vector space E over 𝕜, and a finite index type
variable {𝕜 E ι : Type*} [Fintype ι] [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E]

variable {s : Set E} {x : E}{hx : x  convexHull 𝕜 s}

lemma shapley_folkman{D : }{N : }{Q : ι  Set E}
(hD : D  Fintype.card ι) :
convexHull 𝕜 (Σ i  Finset.range N Q i)   (I : Finset ι) (hI: I.card = D), (Σ i, convexHull 𝕜 (Q i)) + (Σ i, Q i) := sorry

I've also worked on another formulation of the SF lemma (this one is also incomplete). But I started working on the version above, because it seemed easier to state in Lean. This one is supposed to be the statement of the SF lemma here, inside the box.

lemma shapley_folkman {N : }{Q : ι  Set E} {s : Finset ι}
  (x : E)
  (h_convex :  i  s, Convex 𝕜 (Q i))
  (h_finite :  i  s, Finite (Q i))
  (h_mem : x  convexHull 𝕜 ( i in s, Q i)) :
   (q : ι  E), ( i in (finset.range N).to_finset, q i = x) ^
   i, q i  convexHull 𝕜 (Q i) := sorry

EDIT: I see Peter Hansen's messages on the SF lemma now. I think I should verify whether he is still working on this, before continuing.

Daniel Weber (Jul 10 2024 at 12:36):

You need to open BigOperators to use the notation

Yaël Dillies (Jul 10 2024 at 13:27):

No, you don't anymore (as of two months ago)

Yaël Dillies (Jul 10 2024 at 13:28):

You are just missing a comma between N and Q i

Nick Decroos (Jul 10 2024 at 16:21):

Thanks for the feedback, I have this error at the moment:

lemma shapley_folkman{D : }{N : }{Q : ι  Set E}
(hD : D  Fintype.card ι) :
convexHull 𝕜 (Σ i  range N, Q i)
unexpected token '∈'; expected ','

I am trying all sorts of things with

i  range N

to see what works
(i in range N, i \in Finset.range N,...)

Kevin Buzzard (Jul 10 2024 at 19:13):

If you're trying to do a finite sum, You have the wrong Σ. You want , which you can get with \sum.

Nick Decroos (Jul 11 2024 at 19:30):

Kevin Buzzard
Great catch, that was the error. Thanks!

Nick Decroos (Jul 17 2024 at 12:29):

I struggle with the indices and the sets over which to take the indices, in this statement here:
shapley-folkman.png
I want to state this in Lean4, from the wiki article.

This is my code at the moment:

import Mathlib.Data.Finset.Basic
import Mathlib.Data.Set.Basic
import Mathlib.Data.Set.Card
import Mathlib.Data.Set.Finite
import Mathlib.Analysis.Convex.Basic
import Mathlib.Analysis.Convex.Hull
import Mathlib.Analysis.Convex.Combination
import Mathlib.Algebra.Module.Basic

namespace Convex

open Fintype Finset Set Pointwise

-- Assume that we have a field 𝕜, a vector space E over 𝕜, and a finite index type
variable {𝕜 E ι : Type*} [Fintype ι] [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E]

/-!
# The Shapley-Folkman lemma

The Shapley-Folkman lemma is a result in convex analysis that states that the Minkowski sum of a finite number of sets is close to the Minkowski sum of their convex hulls.
The intuitive understand is that the lemma implies that even if individual sets are non-convex, their sum behaves almost as if it were convex, when the number of sets is large compared to the dimension of the space.
The sum of a large number of nonconvex sets is approximately convex (though still noncnvex).
The lemma is used in mathematical economics, in particular in general equilibrium theory.

## Tags

convex hull, shapley-folkman, convex analysis, mathematical economics

-/

/-- **Shapley-Folkman's lemma**

-/
lemma shapley_folkman {ι}{D N : } (Q : ι  Set E) :
  convexHull 𝕜 ( n  Finset.range N, Q n)   (I : Finset N) (hI : I.card = D),
  ( n  Finset.range I, convexHull 𝕜 (Q n)) + ( n  Finset N \ I, Q n) := sorry

end Convex

Yves Jäckle (Jul 18 2024 at 07:47):

There's

#check Finset.powersetCard
#check Finset.slice

Last updated: May 02 2025 at 03:31 UTC