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)