Shapley-Folkman lemma

Stream: new members

[Peter Hansen]

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 $E \subset \mathbb{R}^l$.
Let $\mathrm{x} \in \operatorname{conv}(E)$, where $\operatorname{conv}(E)$ denotes the convex hull of $E$.
Then $\mathbf{x}$ is a convex combination of affinely independent points of $E$.
In particular, $\mathbf{x}$ is a convex combination of at most $l+1$ points of $E$.

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]

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 $(y_i)_{i \in I}$ such that $s=\sum_{i=1}^m y_i$ and that for all $i\in I$ there exist $(y_{i,j})_{j\in J}$ and $(a_{i,j})_{j\in J}$ such that $y_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 $i$ in $S=\sum_{i=1}^m S_i$. How do I do that?

[Eric Wieser]

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

[Yaël Dillies]

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

[Peter Hansen]

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 $n$ 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]

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]

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 $S \subset \mathbb{R}^n$, but I believe this does not yet exist in mathlib.
The hull is formed by intersecting all convex cones containing $S$ 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]

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

[Peter Hansen]

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]

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

[Eric Wieser]

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]

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]

Yeah, don't bother with closure_operator

[Peter Hansen]

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]

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

[Yaël Dillies]

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]

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]

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]

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

[Peter Hansen]

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]

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]

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]

You need to open BigOperators to use the notation

[Yaël Dillies]

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

[Yaël Dillies]

You are just missing a comma between N and Q i

[Nick Decroos]

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]

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

[Nick Decroos]

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

[Nick Decroos]

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]

There's

#check Finset.powersetCard
#check Finset.slice