feat(analysis/convex/extreme): Extreme points of s ×ˢ t (#18171)

YaelDillies · eric-wieser · YaelDillies · commit c5773405394e · 2023-03-01T12:30:26.000Z
Characterise `segment`, `open_segment`, `extreme_points` in `prod` and `pi`.



Co-authored-by: Eric Wieser &lt;wieser.eric@gmail.com&gt;
diff --git a/src/analysis/convex/extreme.lean b/src/analysis/convex/extreme.lean
@@ -35,18 +35,18 @@ See chapter 8 of [Barry Simon, *Convexity*][simon2011]
 
 ## TODO
 
-Define intrinsic frontier and prove lemmas related to extreme sets and points.
+Prove lemmas relating extreme sets and points to the intrinsic frontier.
 
 More not-yet-PRed stuff is available on the branch `sperner_again`.
 -/
 
-open_locale classical affine
-open set
+open function set
+open_locale affine classical
 
-variables (𝕜 : Type*) {E : Type*}
+variables {𝕜 E F ι : Type*} {π : ι → Type*}
 
 section has_smul
-variables [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E]
+variables (𝕜) [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E]
 
 /-- A set `B` is an extreme subset of `A` if `B ⊆ A` and all points of `B` only belong to open
 segments whose ends are in `B`. -/
@@ -99,7 +99,7 @@ protected lemma is_extreme.mono (hAC : is_extreme 𝕜 A C) (hBA : B ⊆ A) (hCB
   is_extreme 𝕜 B C :=
 ⟨hCB, λ x₁ hx₁B x₂ hx₂B x hxC hx, hAC.2 (hBA hx₁B) (hBA hx₂B) hxC hx⟩
 
-lemma is_extreme_Inter {ι : Type*} [nonempty ι] {F : ι → set E}
+lemma is_extreme_Inter {ι : Sort*} [nonempty ι] {F : ι → set E}
   (hAF : ∀ i : ι, is_extreme 𝕜 A (F i)) :
   is_extreme 𝕜 A (⋂ i : ι, F i) :=
 begin
@@ -110,16 +110,9 @@ begin
   exact ⟨λ i, (h i).1, λ i, (h i).2⟩,
 end
 
-lemma is_extreme_bInter {F : set (set E)} (hF : F.nonempty)
-  (hAF : ∀ B ∈ F, is_extreme 𝕜 A B) :
+lemma is_extreme_bInter {F : set (set E)} (hF : F.nonempty) (hA : ∀ B ∈ F, is_extreme 𝕜 A B) :
   is_extreme 𝕜 A (⋂ B ∈ F, B) :=
-begin
-  obtain ⟨B, hB⟩ := hF,
-  refine ⟨(bInter_subset_of_mem hB).trans (hAF B hB).1, λ x₁ hx₁A x₂ hx₂A x hxF hx, _⟩,
-  simp_rw mem_Inter₂ at ⊢ hxF,
-  have h := λ B hB, (hAF B hB).2 hx₁A hx₂A (hxF B hB) hx,
-  exact ⟨λ B hB, (h B hB).1, λ B hB, (h B hB).2⟩,
-end
+by { haveI := hF.to_subtype, simpa only [Inter_subtype] using is_extreme_Inter (λ i : F, hA _ i.2) }
 
 lemma is_extreme_sInter {F : set (set E)} (hF : F.nonempty)
   (hAF : ∀ B ∈ F, is_extreme 𝕜 A B) :
@@ -132,7 +125,7 @@ begin
   exact ⟨λ B hB, (h B hB).1, λ B hB, (h B hB).2⟩,
 end
 
-lemma extreme_points_def :
+lemma mem_extreme_points :
   x ∈ A.extreme_points 𝕜 ↔ x ∈ A ∧ ∀ (x₁ x₂ ∈ A), x ∈ open_segment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x :=
 iff.rfl
 
@@ -175,13 +168,59 @@ subset.antisymm (λ x hx, ⟨hx.1, hAB.extreme_points_subset_extreme_points hx
 end has_smul
 
 section ordered_semiring
-variables {𝕜} [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] {A B : set E} {x : E}
+variables [ordered_semiring 𝕜] [add_comm_group E] [add_comm_group F] [Π i, add_comm_group (π i)]
+  [module 𝕜 E] [module 𝕜 F] [Π i, module 𝕜 (π i)] {A B : set E} {x : E}
 
 lemma is_extreme.convex_diff (hA : convex 𝕜 A) (hAB : is_extreme 𝕜 A B) :
   convex 𝕜 (A \ B) :=
 convex_iff_open_segment_subset.2 (λ x₁ ⟨hx₁A, hx₁B⟩ x₂ ⟨hx₂A, hx₂B⟩ x hx,
     ⟨hA.open_segment_subset hx₁A hx₂A hx, λ hxB, hx₁B (hAB.2 hx₁A hx₂A hxB hx).1⟩)
 
+@[simp] lemma extreme_points_prod (s : set E) (t : set F) :
+  (s ×ˢ t).extreme_points 𝕜 = s.extreme_points 𝕜 ×ˢ t.extreme_points 𝕜 :=
+begin
+  ext,
+  refine (and_congr_right $ λ hx, ⟨λ h, _, λ h, _⟩).trans (and_and_and_comm _ _ _ _),
+  split,
+  { rintro x₁ hx₁ x₂ hx₂ hx_fst,
+    refine (h (mk_mem_prod hx₁ hx.2) (mk_mem_prod hx₂ hx.2) _).imp
+      (congr_arg prod.fst) (congr_arg prod.fst),
+    rw ←prod.image_mk_open_segment_left,
+    exact ⟨_, hx_fst, prod.mk.eta⟩ },
+  { rintro x₁ hx₁ x₂ hx₂ hx_snd,
+    refine (h (mk_mem_prod hx.1 hx₁) (mk_mem_prod hx.1 hx₂) _).imp
+      (congr_arg prod.snd) (congr_arg prod.snd),
+    rw ←prod.image_mk_open_segment_right,
+    exact ⟨_, hx_snd, prod.mk.eta⟩ },
+  { rintro x₁ hx₁ x₂ hx₂ ⟨a, b, ha, hb, hab, hx'⟩,
+    simp_rw prod.ext_iff,
+    exact (and_and_and_comm _ _ _ _).1
+     ⟨h.1 hx₁.1 hx₂.1 ⟨a, b, ha, hb, hab, congr_arg prod.fst hx'⟩,
+      h.2 hx₁.2 hx₂.2 ⟨a, b, ha, hb, hab, congr_arg prod.snd hx'⟩⟩ }
+end
+
+@[simp] lemma extreme_points_pi (s : Π i, set (π i)) :
+  (univ.pi s).extreme_points 𝕜 = univ.pi (λ i, (s i).extreme_points 𝕜) :=
+begin
+  ext,
+  simp only [mem_extreme_points, mem_pi, mem_univ, true_implies_iff, @forall_and_distrib ι],
+  refine and_congr_right (λ hx, ⟨λ h i, _, λ h, _⟩),
+  { rintro x₁ hx₁ x₂ hx₂ hi,
+    refine (h (update x i x₁) _ (update x i x₂) _ _).imp (λ h₁, by rw [←h₁, update_same])
+      (λ h₂, by rw [←h₂, update_same]),
+    iterate 2
+    { rintro j,
+      obtain rfl | hji := eq_or_ne j i,
+      { rwa update_same },
+      { rw update_noteq hji,
+        exact hx _ } },
+    rw ←pi.image_update_open_segment,
+    exact ⟨_, hi, update_eq_self _ _⟩ },
+  { rintro x₁ hx₁ x₂ hx₂ ⟨a, b, ha, hb, hab, hx'⟩,
+    simp_rw [funext_iff, ←forall_and_distrib],
+    exact λ i, h _ _ (hx₁ _) _ (hx₂ _) ⟨a, b, ha, hb, hab, congr_fun hx' _⟩ }
+end
+
 end ordered_semiring
 
 section linear_ordered_ring
diff --git a/src/analysis/convex/segment.lean b/src/analysis/convex/segment.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Alexander Bentkamp. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Alexander Bentkamp, Yury Kudriashov, Yaël Dillies
+Authors: Alexander Bentkamp, Yury Kudryashov, Yaël Dillies
 -/
 import algebra.order.invertible
 import algebra.order.smul
@@ -29,9 +29,10 @@ Should we rename `segment` and `open_segment` to `convex.Icc` and `convex.Ioo`?
 define `clopen_segment`/`convex.Ico`/`convex.Ioc`?
 -/
 
-variables {𝕜 E F : Type*}
+variables {𝕜 E F G ι : Type*} {π : ι → Type*}
 
-open set
+open function set
+open_locale pointwise
 
 section ordered_semiring
 variables [ordered_semiring 𝕜] [add_comm_monoid E]
@@ -137,7 +138,8 @@ end ordered_semiring
 open_locale convex
 
 section ordered_ring
-variables (𝕜) [ordered_ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F]
+variables (𝕜) [ordered_ring 𝕜] [add_comm_group E] [add_comm_group F] [add_comm_group G] [module 𝕜 E]
+  [module 𝕜 F]
 
 section densely_ordered
 variables [nontrivial 𝕜] [densely_ordered 𝕜]
@@ -180,28 +182,29 @@ lemma open_segment_eq_image_line_map (x y : E) :
   open_segment 𝕜 x y = affine_map.line_map x y '' Ioo (0 : 𝕜) 1 :=
 by { convert open_segment_eq_image 𝕜 x y, ext, exact affine_map.line_map_apply_module _ _ _ }
 
-lemma segment_image (f : E →ₗ[𝕜] F) (a b : E) : f '' [a -[𝕜] b] = [f a -[𝕜] f b] :=
-set.ext (λ x, by simp_rw [segment_eq_image, mem_image, exists_exists_and_eq_and, map_add, map_smul])
+@[simp] lemma image_segment (f : E →ᵃ[𝕜] F) (a b : E) : f '' [a -[𝕜] b] = [f a -[𝕜] f b] :=
+set.ext $ λ x, by simp_rw [segment_eq_image_line_map, mem_image, exists_exists_and_eq_and,
+  affine_map.apply_line_map]
 
-@[simp] lemma open_segment_image (f : E →ₗ[𝕜] F) (a b : E) :
+@[simp] lemma image_open_segment (f : E →ᵃ[𝕜] F) (a b : E) :
   f '' open_segment 𝕜 a b = open_segment 𝕜 (f a) (f b) :=
-set.ext (λ x, by simp_rw [open_segment_eq_image, mem_image, exists_exists_and_eq_and, map_add,
-  map_smul])
+set.ext $ λ x, by simp_rw [open_segment_eq_image_line_map, mem_image, exists_exists_and_eq_and,
+  affine_map.apply_line_map]
 
-lemma mem_segment_translate (a : E) {x b c} : a + x ∈ [a + b -[𝕜] a + c] ↔ x ∈ [b -[𝕜] c] :=
-begin
-  rw [segment_eq_image', segment_eq_image'],
-  refine exists_congr (λ θ, and_congr iff.rfl _),
-  simp only [add_sub_add_left_eq_sub, add_assoc, add_right_inj],
-end
+@[simp] lemma vadd_segment [add_torsor G E] [vadd_comm_class G E E] (a : G) (b c : E) :
+  a +ᵥ [b -[𝕜] c] = [a +ᵥ b -[𝕜] a +ᵥ c] :=
+image_segment 𝕜 ⟨_, linear_map.id, λ _ _, vadd_comm _ _ _⟩ b c
+
+@[simp] lemma vadd_open_segment [add_torsor G E] [vadd_comm_class G E E] (a : G) (b c : E) :
+  a +ᵥ open_segment 𝕜 b c = open_segment 𝕜 (a +ᵥ b) (a +ᵥ c) :=
+image_open_segment 𝕜 ⟨_, linear_map.id, λ _ _, vadd_comm _ _ _⟩ b c
+
+@[simp] lemma mem_segment_translate (a : E) {x b c} : a + x ∈ [a + b -[𝕜] a + c] ↔ x ∈ [b -[𝕜] c] :=
+by simp_rw [←vadd_eq_add, ←vadd_segment, vadd_mem_vadd_set_iff]
 
 @[simp] lemma mem_open_segment_translate (a : E) {x b c : E} :
   a + x ∈ open_segment 𝕜 (a + b) (a + c) ↔ x ∈ open_segment 𝕜 b c :=
-begin
-  rw [open_segment_eq_image', open_segment_eq_image'],
-  refine exists_congr (λ θ, and_congr iff.rfl _),
-  simp only [add_sub_add_left_eq_sub, add_assoc, add_right_inj],
-end
+by simp_rw [←vadd_eq_add, ←vadd_open_segment, vadd_mem_vadd_set_iff]
 
 lemma segment_translate_preimage (a b c : E) : (λ x, a + x) ⁻¹' [a + b -[𝕜] a + c] = [b -[𝕜] c] :=
 set.ext $ λ x, mem_segment_translate 𝕜 a
@@ -492,3 +495,95 @@ begin
 end
 
 end linear_ordered_field
+
+namespace prod
+variables [ordered_semiring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F]
+
+lemma segment_subset (x y : E × F) : segment 𝕜 x y ⊆ segment 𝕜 x.1 y.1 ×ˢ segment 𝕜 x.2 y.2 :=
+begin
+  rintro z ⟨a, b, ha, hb, hab, hz⟩,
+  exact ⟨⟨a, b, ha, hb, hab, congr_arg prod.fst hz⟩, a, b, ha, hb, hab, congr_arg prod.snd hz⟩,
+end
+
+lemma open_segment_subset (x y : E × F) :
+  open_segment 𝕜 x y ⊆ open_segment 𝕜 x.1 y.1 ×ˢ open_segment 𝕜 x.2 y.2 :=
+begin
+  rintro z ⟨a, b, ha, hb, hab, hz⟩,
+  exact ⟨⟨a, b, ha, hb, hab, congr_arg prod.fst hz⟩, a, b, ha, hb, hab, congr_arg prod.snd hz⟩,
+end
+
+lemma image_mk_segment_left (x₁ x₂ : E) (y : F) :
+  (λ x, (x, y)) '' [x₁ -[𝕜] x₂] = [(x₁, y) -[𝕜] (x₂, y)] :=
+begin
+  ext ⟨x', y'⟩,
+  simp_rw [set.mem_image, segment, set.mem_set_of, prod.smul_mk, prod.mk_add_mk,
+    prod.mk.inj_iff, ←exists_and_distrib_right, @exists_comm E, exists_eq_left'],
+  refine exists₅_congr (λ a b ha hb hab, _),
+  rw convex.combo_self hab,
+end
+
+lemma image_mk_segment_right (x : E) (y₁ y₂ : F) :
+  (λ y, (x, y)) '' [y₁ -[𝕜] y₂] = [(x, y₁) -[𝕜] (x, y₂)] :=
+begin
+  ext ⟨x', y'⟩,
+  simp_rw [set.mem_image, segment, set.mem_set_of, prod.smul_mk, prod.mk_add_mk,
+    prod.mk.inj_iff, ←exists_and_distrib_right, @exists_comm F, exists_eq_left'],
+  refine exists₅_congr (λ a b ha hb hab, _),
+  rw convex.combo_self hab,
+end
+
+lemma image_mk_open_segment_left (x₁ x₂ : E) (y : F) :
+  (λ x, (x, y)) '' open_segment 𝕜 x₁ x₂ = open_segment 𝕜 (x₁, y) (x₂, y) :=
+begin
+  ext ⟨x', y'⟩,
+  simp_rw [set.mem_image, open_segment, set.mem_set_of, prod.smul_mk, prod.mk_add_mk,
+    prod.mk.inj_iff, ←exists_and_distrib_right, @exists_comm E, exists_eq_left'],
+  refine exists₅_congr (λ a b ha hb hab, _),
+  rw convex.combo_self hab,
+end
+
+@[simp] lemma image_mk_open_segment_right (x : E) (y₁ y₂ : F) :
+  (λ y, (x, y)) '' open_segment 𝕜 y₁ y₂ = open_segment 𝕜 (x, y₁) (x, y₂) :=
+begin
+  ext ⟨x', y'⟩,
+  simp_rw [set.mem_image, open_segment, set.mem_set_of, prod.smul_mk, prod.mk_add_mk,
+    prod.mk.inj_iff, ←exists_and_distrib_right, @exists_comm F, exists_eq_left'],
+  refine exists₅_congr (λ a b ha hb hab, _),
+  rw convex.combo_self hab,
+end
+
+end prod
+
+namespace pi
+variables [ordered_semiring 𝕜] [Π i, add_comm_monoid (π i)] [Π i, module 𝕜 (π i)] {s : set ι}
+
+lemma segment_subset (x y : Π i, π i) : segment 𝕜 x y ⊆ s.pi (λ i, segment 𝕜 (x i) (y i)) :=
+by { rintro z ⟨a, b, ha, hb, hab, hz⟩ i -, exact ⟨a, b, ha, hb, hab, congr_fun hz i⟩ }
+
+lemma open_segment_subset (x y : Π i, π i) :
+  open_segment 𝕜 x y ⊆ s.pi (λ i, open_segment 𝕜 (x i) (y i)) :=
+by { rintro z ⟨a, b, ha, hb, hab, hz⟩ i -, exact ⟨a, b, ha, hb, hab, congr_fun hz i⟩ }
+
+variables [decidable_eq ι]
+
+lemma image_update_segment (i : ι) (x₁ x₂ : π i) (y : Π i, π i) :
+  update y i '' [x₁ -[𝕜] x₂] = [update y i x₁ -[𝕜] update y i x₂] :=
+begin
+  ext z,
+  simp_rw [set.mem_image, segment, set.mem_set_of, ←update_smul, ←update_add, update_eq_iff,
+    ←exists_and_distrib_right, @exists_comm (π i), exists_eq_left'],
+  refine exists₅_congr (λ a b ha hb hab, _),
+  rw convex.combo_self hab,
+end
+
+lemma image_update_open_segment (i : ι) (x₁ x₂ : π i) (y : Π i, π i) :
+  update y i '' open_segment 𝕜 x₁ x₂ = open_segment 𝕜 (update y i x₁) (update y i x₂) :=
+begin
+  ext z,
+  simp_rw [set.mem_image, open_segment, set.mem_set_of, ←update_smul, ←update_add, update_eq_iff,
+    ←exists_and_distrib_right, @exists_comm (π i), exists_eq_left'],
+  refine exists₅_congr (λ a b ha hb hab, _),
+  rw convex.combo_self hab,
+end
+
+end pi
