Zulip Chat Archive

Stream: Is there code for X?

Topic: Convexity and products


view this post on Zulip Heather Macbeth (Oct 25 2020 at 20:41):

I couldn't find these in the library, do they exist?

import analysis.convex.basic

open_locale big_operators
open set

variables {E : Type*} {F : Type*}
  [add_comm_group E] [vector_space  E] [add_comm_group F] [vector_space  F]

lemma prod_convex {s : set E} {t : set F} (hs : convex s) (ht : convex t) :
  convex (s.prod t) :=
sorry

lemma prod_convex_hull (s : set E) (t : set F) :
  convex_hull (s.prod t) = (convex_hull s).prod (convex_hull t) :=
sorry

view this post on Zulip Heather Macbeth (Oct 25 2020 at 20:42):

I have proofs of both (the latter rather terrible), will clean up and PR if missing.

view this post on Zulip Patrick Massot (Oct 25 2020 at 20:43):

Beware that @Yury G. Kudryashov is working on refactoring convexity.

view this post on Zulip Patrick Massot (Oct 25 2020 at 20:43):

So maybe you shouldn't invest too much time on this lemma right now.

view this post on Zulip Heather Macbeth (Oct 25 2020 at 22:28):

@Yury G. Kudryashov, how will your refactor interact with goals like this? I can post my proof if it would help you assess whether it's the kind of thing that would change a lot after the refactor.

view this post on Zulip Yury G. Kudryashov (Oct 25 2020 at 22:41):

Let me open a WIP PR tonight.

view this post on Zulip Heather Macbeth (Oct 25 2020 at 22:41):

Thanks!


Last updated: May 19 2021 at 00:40 UTC