Zulip Chat Archive

Stream: maths

Topic: Convex hull of a product


Yaël Dillies (May 15 2022 at 11:11):

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 (May 15 2022 at 11:12):

@Yury G. Kudryashov might have an opinion.

Yaël Dillies (May 15 2022 at 11:14):

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 (May 15 2022 at 11:15):

But I would be very glad to be proven wrong.

Kevin Buzzard (May 15 2022 at 11:59):

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 iaisi\sum_i a_i s_i (a finite sum) with siSs_i\in S and 0aik0\leq a_i\in k with iai=1\sum_i a_i=1? Thinking about it this way, it seems that the first nontrivial obstruction is trying to write (λ1s1+μ1s2,λ2t1+μ2t2)(\lambda_1s_1+\mu_1s_2,\lambda_2t_1+\mu_2t_2) in this way, with λi+μi=1\lambda_i+\mu_i=1. To do this you have to be able to solve the following equations: given 0λ1,μ1,λ2,μ20\leq \lambda_1,\mu_1,\lambda_2,\mu_2 with λi+μi=1\lambda_i+\mu_i=1 you need to be able to find 0a,b,c,dk0\leq a,b,c,d\in k with a+b=λ1a+b=\lambda_1, c+d=μ1c+d=\mu_1, a+c=λ2a+c=\lambda_2 and b+c=μ2b+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 (May 15 2022 at 12:01):

Aah, a=λ1λ2a=\lambda_1\lambda_2, b=λ1μ2b=\lambda_1\mu_2 etc. Ok so isn't that a proof?

Kevin Buzzard (May 15 2022 at 12:02):

Given iaisi\sum_i a_is_i and jbjtj\sum_j b_jt_j you consider i,jaibj(si,tj)=(iaisi,jbjtj)\sum_{i,j}a_ib_j(s_i,t_j)=(\sum_i a_is_i,\sum_j b_jt_j).

Yaël Dillies (May 15 2022 at 12:02):

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 (May 15 2022 at 12:06):

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 (May 15 2022 at 12:07):

Your proof seems very fine :smile:

Yaël Dillies (May 15 2022 at 12:08):

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

Kevin Buzzard (May 15 2022 at 12:10):

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 (May 15 2022 at 12:10):

Yeah that's what I'm thinking too.

Yaël Dillies (May 15 2022 at 12:15):

docs#convex_hull_prod :face_palm:

Yaël Dillies (May 15 2022 at 12:16):

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

Kevin Buzzard (May 15 2022 at 12:18):

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 (May 15 2022 at 12:18):

Yaël Dillies said:

docs#convex_hull_prod :face_palm:

[linear_ordered_field R] :-/

Yaël Dillies (May 15 2022 at 12:18):

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

Yaël Dillies (May 15 2022 at 12:22):

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


Last updated: Dec 20 2023 at 11:08 UTC