Zulip Chat Archive

Stream: Is there code for X?

Topic: affine span is convex


Bhavik Mehta (Mar 06 2021 at 22:40):

I'm struggling to find any connection in mathlib between affine spans and convex sets, for instance, how do I show the following?

example {m : } (X : set (fin m  )) :
  convex (affine_span  X : set (fin m  )) :=
begin
end

Kenny Lau (Mar 06 2021 at 22:58):

import analysis.convex.basic
import linear_algebra.affine_space.affine_subspace

example {m : } (M : Type*) [add_comm_group M] [vector_space  M] (s : affine_subspace  M) :
  convex (s : set M) :=
λ x y hxs hys a b ha hb hab,
calc  a  x + b  y
    = (1 - b)  x + b  y : by rw eq_sub_of_add_eq hab
... = b  (y - x) + x :
  by rw [sub_smul, one_smul, sub_add_eq_add_sub, smul_sub, add_comm _ x, add_sub_assoc]
...  s : s.2 _ hys hxs hxs

Bhavik Mehta (Mar 06 2021 at 23:01):

Wow I didn't know calc allowed x = y ∈ s chains

Bhavik Mehta (Mar 06 2021 at 23:01):

Thanks!

Bhavik Mehta (Mar 06 2021 at 23:03):

golfed:

example (M : Type*) [add_comm_group M] [vector_space  M] (s : affine_subspace  M) :
  convex (s : set M) :=
λ x y hxs hys a b ha hb hab,
calc a  x + b  y = b  (y - x) + x : convex.combo_to_vadd hab
               ...  s : s.2 _ hys hxs hxs

Kenny Lau (Mar 06 2021 at 23:20):

golfed:

import analysis.convex.basic
import linear_algebra.affine_space.affine_subspace

example (M : Type*) [add_comm_group M] [vector_space  M] (s : affine_subspace  M) :
  convex (s : set M) :=
λ x y hx hy a b ha hb hab, (convex.combo_to_vadd hab : a  x + b  y = _).symm  s.2 _ hy hx hx

Last updated: Dec 20 2023 at 11:08 UTC