Convex hull of a product

Stream: maths

[Yaël Dillies]

Does anyone know how to prove that the convex hull of the product is the product of the convex hulls? Here's an excerpt of my draft over at branch#convex_hull_add:

import analysis.convex.hull

open set

variables {𝕜 E F : Type*} [ordered_semiring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E]
  [module 𝕜 F] {s : set E} {t : set F} {x : E} {y : F}

lemma mk_mem_convex_hull_prod (hx : x ∈ convex_hull 𝕜 s) (hy : y ∈ convex_hull 𝕜 t) :
  (x, y) ∈ convex_hull 𝕜 (s ×ˢ t) :=
sorry

@[simp] lemma convex_hull_prod (s : set E) (t : set F) :
  convex_hull 𝕜 (s ×ˢ t) = convex_hull 𝕜 s ×ˢ convex_hull 𝕜 t :=
subset.antisymm (convex_hull_min (prod_mono (subset_convex_hull _ _) $ subset_convex_hull _ _) $
  (convex_convex_hull _ _).prod $ convex_convex_hull _ _) $
    prod_subset_iff.2 $ λ x hx y, mk_mem_convex_hull_prod hx

[Yaël Dillies]

@Yury G. Kudryashov might have an opinion.

[Yaël Dillies]

It seems this is not simply a categorical fact coming from convex_hull being a closure operator and we do have to use something concrete about it.

[Yaël Dillies]

But I would be very glad to be proven wrong.

[Kevin Buzzard]

Is this a maths question? Is it known that this is true in this generality?

Can't the convex hull of a set s be defined as the elements which can be written in the form $\sum_i a_i s_i$ (a finite sum) with $s_i\in S$ and $0\leq a_i\in k$ with $\sum_i a_i=1$? Thinking about it this way, it seems that the first nontrivial obstruction is trying to write $(\lambda_1s_1+\mu_1s_2,\lambda_2t_1+\mu_2t_2)$ in this way, with $\lambda_i+\mu_i=1$. To do this you have to be able to solve the following equations: given $0\leq \lambda_1,\mu_1,\lambda_2,\mu_2$ with $\lambda_i+\mu_i=1$ you need to be able to find $0\leq a,b,c,d\in k$ with $a+b=\lambda_1$, $c+d=\mu_1$, $a+c=\lambda_2$ and $b+c=\mu_2$. So that's a completely concrete question which has nothing to do with convexity: can you do this? If you can do this you can probably do anything (by induction/optimism).

[Kevin Buzzard]

Aah, $a=\lambda_1\lambda_2$, $b=\lambda_1\mu_2$ etc. Ok so isn't that a proof?

[Kevin Buzzard]

Given $\sum_i a_is_i$ and $\sum_j b_jt_j$ you consider $\sum_{i,j}a_ib_j(s_i,t_j)=(\sum_i a_is_i,\sum_j b_jt_j)$.

[Yaël Dillies]

I don't know whether it is true in this generality, but it better be true in usual cases because it is equivalent to convex_hull 𝕜 (s + t) = convex_hull 𝕜 s + convex_hull 𝕜 t which Wikipedia claims to be true.

[Kevin Buzzard]

I don't know anything about this stuff, I had to fire up mathlib to read the definitions. Let me know if my proof is problematic.

[Yaël Dillies]

Your proof seems very fine :smile:

[Yaël Dillies]

But it probably means that `convex_hull 𝕜 (s.pi t) is not s.pi (λ i, convex_hull 𝕜 (t i)) in general.

[Kevin Buzzard]

Is s here a set (rather than a finset)? You're talking about arbitrary products? I mean, arbitrary products of open sets aren't open in the product topology in general (when you allow infinite products of top spaces) so maybe this is the same sort of thing?

[Yaël Dillies]

Yeah that's what I'm thinking too.

[Yaël Dillies]

docs#convex_hull_prod :face_palm:

[Yaël Dillies]

That's what you get for not putting stuff in the right place.

[Kevin Buzzard]

Infinite products: Yeah this sounds right. If you consider {0,1} as a subset of the reals, then for an infinite product of these, the convex hull will only contain points (a_i) where the a_i only take on finitely many values, right? Whereas in the product of the convex hulls you have far more stuff.

[Kevin Buzzard]

Yaël Dillies said:

docs#convex_hull_prod :face_palm:

[linear_ordered_field R] :-/

[Yaël Dillies]

Yeah this is because docs#finset.affine_combination is dumb and divides by the sum of the weights.

[Yaël Dillies]

I'm fixing it in #9268 but I never got around to reviving it.