feat(analysis/convex/combination): The convex hull of s + t (#14160)

`convex_hull` distributes over pointwise addition of sets and commutes with pointwise scalar multiplication. Also delete `linear_map.image_convex_hull` because it duplicates `linear_map.convex_hull_image`.

Author: YaelDillies

src/analysis/convex/combination.lean

@@ -24,7 +24,7 @@ lemmas unconditional on the sum of the weights being `1`.
 -/
 
 open set
-open_locale big_operators classical
+open_locale big_operators classical pointwise
 
 universes u u'
 variables {R E F ι ι' : Type*} [linear_ordered_field R] [add_comm_group E] [add_comm_group F]
@@ -325,13 +325,10 @@ begin
   { exact Union_subset (λ i, Union_subset convex_hull_mono), },
 end
 
-lemma convex_hull_prod (s : set E) (t : set F) :
-  convex_hull R (s ×ˢ t) = convex_hull R s ×ˢ convex_hull R t :=
+lemma mk_mem_convex_hull_prod {t : set F} {x : E} {y : F} (hx : x ∈ convex_hull R s)
+  (hy : y ∈ convex_hull R t) :
+  (x, y) ∈ convex_hull R (s ×ˢ t) :=
 begin
-  refine set.subset.antisymm _ _,
-  { exact convex_hull_min (set.prod_mono (subset_convex_hull _ _) $ subset_convex_hull _ _)
-    ((convex_convex_hull _ _).prod $ convex_convex_hull _ _) },
-  rintro ⟨x, y⟩ ⟨hx, hy⟩,
   rw convex_hull_eq at ⊢ hx hy,
   obtain ⟨ι, a, w, S, hw, hw', hS, hSp⟩ := hx,
   obtain ⟨κ, b, v, T, hv, hv', hT, hTp⟩ := hy,
@@ -367,6 +364,19 @@ begin
     rw [←finset.sum_smul, hw', one_smul] }
 end
 
+@[simp] lemma convex_hull_prod (s : set E) (t : set F) :
+  convex_hull R (s ×ˢ t) = convex_hull R s ×ˢ convex_hull R 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
+
+lemma convex_hull_add (s t : set E) : convex_hull R (s + t) = convex_hull R s + convex_hull R t :=
+by simp_rw [←image2_add, ←image_prod, is_linear_map.is_linear_map_add.convex_hull_image,
+  convex_hull_prod]
+
+lemma convex_hull_sub (s t : set E) : convex_hull R (s - t) = convex_hull R s - convex_hull R t :=
+by simp_rw [sub_eq_add_neg, convex_hull_add, convex_hull_neg]
+
 /-! ### `std_simplex` -/
 
 variables (ι) [fintype ι] {f : ι → R}

src/analysis/convex/hull.lean

@@ -20,6 +20,7 @@ while the impact on writing code is minimal as `convex_hull 𝕜 s` is automatic
 -/
 
 open set
+open_locale pointwise
 
 variables {𝕜 E F : Type*}
 
@@ -46,15 +47,24 @@ lemma subset_convex_hull : s ⊆ convex_hull 𝕜 s := (convex_hull 𝕜).le_clo
 
 lemma convex_convex_hull : convex 𝕜 (convex_hull 𝕜 s) := closure_operator.closure_mem_mk₃ s
 
-variables {𝕜 s} {t : set E}
+lemma convex_hull_eq_Inter : convex_hull 𝕜 s = ⋂ (t : set E) (hst : s ⊆ t) (ht : convex 𝕜 t), t :=
+rfl
+
+variables {𝕜 s} {t : set E} {x : E}
+
+lemma mem_convex_hull_iff : x ∈ convex_hull 𝕜 s ↔ ∀ t, s ⊆ t → convex 𝕜 t → x ∈ t :=
+by simp_rw [convex_hull_eq_Inter, mem_Inter]
 
 lemma convex_hull_min (hst : s ⊆ t) (ht : convex 𝕜 t) : convex_hull 𝕜 s ⊆ t :=
 closure_operator.closure_le_mk₃_iff (show s ≤ t, from hst) ht
 
+lemma convex.convex_hull_subset_iff (ht : convex 𝕜 t) : convex_hull 𝕜 s ⊆ t ↔ s ⊆ t :=
+⟨(subset_convex_hull _ _).trans, λ h, convex_hull_min h ht⟩
+
 @[mono] lemma convex_hull_mono (hst : s ⊆ t) : convex_hull 𝕜 s ⊆ convex_hull 𝕜 t :=
 (convex_hull 𝕜).monotone hst
 
-lemma convex.convex_hull_eq {s : set E} (hs : convex 𝕜 s) : convex_hull 𝕜 s = s :=
+lemma convex.convex_hull_eq (hs : convex 𝕜 s) : convex_hull 𝕜 s = s :=
 closure_operator.mem_mk₃_closed hs
 
 @[simp] lemma convex_hull_univ : convex_hull 𝕜 (univ : set E) = univ :=
@@ -78,6 +88,10 @@ begin
   exact not_congr convex_hull_empty_iff,
 end
 
+alias convex_hull_nonempty_iff ↔ _ set.nonempty.convex_hull
+
+attribute [protected] set.nonempty.convex_hull
+
 @[simp]
 lemma convex_hull_singleton {x : E} : convex_hull 𝕜 ({x} : set E) = {x} :=
 (convex_singleton x).convex_hull_eq
@@ -95,21 +109,6 @@ begin
     by { rintro (rfl : y = x), exact hx hy }⟩),
 end
 
-lemma is_linear_map.image_convex_hull {f : E → F} (hf : is_linear_map 𝕜 f) :
-  f '' (convex_hull 𝕜 s) = convex_hull 𝕜 (f '' s) :=
-begin
-  apply set.subset.antisymm ,
-  { rw set.image_subset_iff,
-    exact convex_hull_min (set.image_subset_iff.1 $ subset_convex_hull 𝕜 $ f '' s)
-      ((convex_convex_hull 𝕜 (f '' s)).is_linear_preimage hf) },
-  { exact convex_hull_min (set.image_subset _ $ subset_convex_hull 𝕜 s)
-     ((convex_convex_hull 𝕜 s).is_linear_image hf) }
-end
-
-lemma linear_map.image_convex_hull (f : E →ₗ[𝕜] F) :
-  f '' (convex_hull 𝕜 s) = convex_hull 𝕜 (f '' s) :=
-f.is_linear.image_convex_hull
-
 lemma is_linear_map.convex_hull_image {f : E → F} (hf : is_linear_map 𝕜 f) (s : set E) :
   convex_hull 𝕜 (f '' s) = f '' convex_hull 𝕜 s :=
 set.subset.antisymm (convex_hull_min (image_subset _ (subset_convex_hull 𝕜 s)) $
@@ -125,14 +124,22 @@ f.is_linear.convex_hull_image s
 end add_comm_monoid
 end ordered_semiring
 
+section ordered_comm_semiring
+variables [ordered_comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E]
+
+lemma convex_hull_smul (a : 𝕜) (s : set E) : convex_hull 𝕜 (a • s) = a • convex_hull 𝕜 s :=
+(linear_map.lsmul _ _ a).convex_hull_image _
+
+end ordered_comm_semiring
+
 section ordered_ring
 variables [ordered_ring 𝕜]
 
 section add_comm_group
 variables [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] (s : set E)
 
 lemma affine_map.image_convex_hull (f : E →ᵃ[𝕜] F) :
-  f '' (convex_hull 𝕜 s) = convex_hull 𝕜 (f '' s) :=
+  f '' convex_hull 𝕜 s = convex_hull 𝕜 (f '' s) :=
 begin
   apply set.subset.antisymm,
   { rw set.image_subset_iff,
@@ -153,6 +160,9 @@ begin
   exact convex_hull_subset_affine_span s,
 end
 
+lemma convex_hull_neg (s : set E) : convex_hull 𝕜 (-s) = -convex_hull 𝕜 s :=
+by { simp_rw ←image_neg, exact (affine_map.image_convex_hull _ $ -1).symm }
+
 end add_comm_group
 end ordered_ring
 end convex_hull