From faaa873ad82a61da3e6511235f671b0990c0cf74 Mon Sep 17 00:00:00 2001
From: YaelDillies <yael.dillies@gmail.com>
Date: Sun, 28 Nov 2021 00:05:16 +0000
Subject: [PATCH 1/8] initial commit

---
 src/analysis/convex/strict.lean | 660 ++++++++++++++++++++++++++++++++
 1 file changed, 660 insertions(+)
 create mode 100644 src/analysis/convex/strict.lean

diff --git a/src/analysis/convex/strict.lean b/src/analysis/convex/strict.lean
new file mode 100644
index 0000000000000..ffd5f1d23760e
--- /dev/null
+++ b/src/analysis/convex/strict.lean
@@ -0,0 +1,660 @@
+/-
+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
+-/
+import analysis.convex.basic
+import topology.algebra.monoid
+
+/-!
+# Strictly strict_convex sets
+-/
+
+variables {𝕜 E F β : Type*}
+
+open set
+open_locale pointwise
+
+/-!
+### Strict convexity of sets
+
+This file defines strictly convex sets.
+
+-/
+
+section ordered_semiring
+variables [ordered_semiring 𝕜]
+
+section add_comm_monoid
+variables [add_comm_monoid E] [topological_space E] [add_comm_monoid F] [topological_space F]
+
+section has_scalar
+variables (𝕜) [has_scalar 𝕜 E] [has_scalar 𝕜 F] (s : set E)
+
+/-- Convexity of sets. -/
+def strict_convex : Prop :=
+s.pairwise (λ x y, ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior s)
+
+variables {𝕜 s}
+
+lemma strict_convex_iff_open_segment_subset :
+  strict_convex 𝕜 s ↔ ∀ ⦃x y⦄, x ∈ s → y ∈ s → open_segment 𝕜 x y ⊆ interior s :=
+begin
+  split,
+  { rintro h x y hx hy z ⟨a, b, ha, hb, hab, rfl⟩,
+    exact h hx hy ha hb hab },
+  { rintro h x y hx hy a b ha hb hab,
+    exact h hx hy ⟨a, b, ha, hb, hab, rfl⟩ }
+end
+
+lemma strict_convex.segment_subset (h : strict_convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
+  [x -[𝕜] y] ⊆ s :=
+convex_iff_segment_subset.1 h hx hy
+
+lemma strict_convex.open_segment_subset (h : strict_convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
+  open_segment 𝕜 x y ⊆ s :=
+(open_segment_subset_segment 𝕜 x y).trans (h.segment_subset hx hy)
+
+/-- Alternative definition of set strict_convexity, in terms of pointwise set operations. -/
+lemma strict_convex_iff_pointwise_add_subset :
+  strict_convex 𝕜 s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s :=
+iff.intro
+  begin
+    rintro hA a b ha hb hab w ⟨au, bv, ⟨u, hu, rfl⟩, ⟨v, hv, rfl⟩, rfl⟩,
+    exact hA hu hv ha hb hab
+  end
+  (λ h x y hx hy a b ha hb hab,
+    (h ha hb hab) (set.add_mem_add ⟨_, hx, rfl⟩ ⟨_, hy, rfl⟩))
+
+lemma strict_convex_empty : strict_convex 𝕜 (∅ : set E) := by finish
+
+lemma strict_convex_univ : strict_convex 𝕜 (set.univ : set E) := λ _ _ _ _ _ _ _ _ _, trivial
+
+lemma strict_convex.inter {t : set E} (hs : strict_convex 𝕜 s) (ht : strict_convex 𝕜 t) : strict_convex 𝕜 (s ∩ t) :=
+λ x y (hx : x ∈ s ∩ t) (hy : y ∈ s ∩ t) a b (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1),
+  ⟨hs hx.left hy.left ha hb hab, ht hx.right hy.right ha hb hab⟩
+
+lemma strict_convex_sInter {S : set (set E)} (h : ∀ s ∈ S, strict_convex 𝕜 s) : strict_convex 𝕜 (⋂₀ S) :=
+assume x y hx hy a b ha hb hab s hs,
+h s hs (hx s hs) (hy s hs) ha hb hab
+
+lemma strict_convex_Inter {ι : Sort*} {s : ι → set E} (h : ∀ i : ι, strict_convex 𝕜 (s i)) :
+  strict_convex 𝕜 (⋂ i, s i) :=
+(sInter_range s) ▸ strict_convex_sInter $ forall_range_iff.2 h
+
+lemma strict_convex.prod {s : set E} {t : set F} (hs : strict_convex 𝕜 s) (ht : strict_convex 𝕜 t) :
+  strict_convex 𝕜 (s.prod t) :=
+begin
+  intros x y hx hy a b ha hb hab,
+  apply mem_prod.2,
+  exact ⟨hs (mem_prod.1 hx).1 (mem_prod.1 hy).1 ha hb hab,
+        ht (mem_prod.1 hx).2 (mem_prod.1 hy).2 ha hb hab⟩
+end
+
+lemma strict_convex_pi {ι : Type*} {E : ι → Type*} [Π i, add_comm_monoid (E i)]
+  [Π i, has_scalar 𝕜 (E i)] {s : set ι} {t : Π i, set (E i)} (ht : ∀ i, strict_convex 𝕜 (t i)) :
+  strict_convex 𝕜 (s.pi t) :=
+λ x y hx hy a b ha hb hab i hi, ht i (hx i hi) (hy i hi) ha hb hab
+
+lemma directed.strict_convex_Union {ι : Sort*} {s : ι → set E} (hdir : directed (⊆) s)
+  (hc : ∀ ⦃i : ι⦄, strict_convex 𝕜 (s i)) :
+  strict_convex 𝕜 (⋃ i, s i) :=
+begin
+  rintro x y hx hy a b ha hb hab,
+  rw mem_Union at ⊢ hx hy,
+  obtain ⟨i, hx⟩ := hx,
+  obtain ⟨j, hy⟩ := hy,
+  obtain ⟨k, hik, hjk⟩ := hdir i j,
+  exact ⟨k, hc (hik hx) (hjk hy) ha hb hab⟩,
+end
+
+lemma directed_on.strict_convex_sUnion {c : set (set E)} (hdir : directed_on (⊆) c)
+  (hc : ∀ ⦃A : set E⦄, A ∈ c → strict_convex 𝕜 A) :
+  strict_convex 𝕜 (⋃₀c) :=
+begin
+  rw sUnion_eq_Union,
+  exact (directed_on_iff_directed.1 hdir).strict_convex_Union (λ A, hc A.2),
+end
+
+end has_scalar
+
+section module
+variables [module 𝕜 E] [module 𝕜 F] {s : set E}
+
+lemma strict_convex.convex (hs : strict_convex 𝕜 s) : convex 𝕜 s :=
+convex_iff_forall_pos.2 $ λ x y hx hy a b ha hb hab, interior_subset $ hs hx hy ha hb hab
+
+lemma convex.strict_convex (h : is_open s) (hs : convex 𝕜 s) : strict_convex 𝕜 s :=
+λ x y hx hy a b ha hb hab, h.interior_eq.symm ▸ hs hx hy ha hb hab
+
+lemma is_open.strict_convex_iff (h : is_open s) : strict_convex 𝕜 s ↔ convex 𝕜 s :=
+⟨strict_convex.convex, convex.strict_convex h⟩
+
+lemma strict_convex_iff_forall_pos :
+  strict_convex 𝕜 s ↔ ∀ ⦃x y⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1
+  → a • x + b • y ∈ s :=
+begin
+  refine ⟨λ h x y hx hy a b ha hb hab, h hx hy ha.le hb.le hab, _⟩,
+  intros h x y hx hy a b ha hb hab,
+  cases ha.eq_or_lt with ha ha,
+  { subst a, rw [zero_add] at hab, simp [hab, hy] },
+  cases hb.eq_or_lt with hb hb,
+  { subst b, rw [add_zero] at hab, simp [hab, hx] },
+  exact h hx hy ha hb hab
+end
+
+lemma strict_convex_iff_pairwise_pos :
+  strict_convex 𝕜 s ↔ s.pairwise (λ x y, ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s) :=
+begin
+  refine ⟨λ h x hx y hy _ a b ha hb hab, h hx hy ha.le hb.le hab, _⟩,
+  intros h x y hx hy a b ha hb hab,
+  obtain rfl | ha' := ha.eq_or_lt,
+  { rw [zero_add] at hab, rwa [hab, zero_smul, one_smul, zero_add] },
+  obtain rfl | hb' := hb.eq_or_lt,
+  { rw [add_zero] at hab, rwa [hab, zero_smul, one_smul, add_zero] },
+  obtain rfl | hxy := eq_or_ne x y,
+  { rwa strict_convex.combo_self hab },
+  exact h _ hx _ hy hxy ha' hb' hab,
+end
+
+lemma strict_convex_iff_open_segment_subset :
+  strict_convex 𝕜 s ↔ ∀ ⦃x y⦄, x ∈ s → y ∈ s → open_segment 𝕜 x y ⊆ s :=
+begin
+  rw strict_convex_iff_segment_subset,
+  exact forall₂_congr (λ x y, forall₂_congr $ λ hx hy,
+    (open_segment_subset_iff_segment_subset hx hy).symm),
+end
+
+lemma strict_convex_singleton (c : E) : strict_convex 𝕜 ({c} : set E) :=
+begin
+  intros x y hx hy a b ha hb hab,
+  rw [set.eq_of_mem_singleton hx, set.eq_of_mem_singleton hy, ←add_smul, hab, one_smul],
+  exact mem_singleton c
+end
+
+lemma strict_convex.linear_image (hs : strict_convex 𝕜 s) (f : E →ₗ[𝕜] F) : strict_convex 𝕜 (s.image f) :=
+begin
+  intros x y hx hy a b ha hb hab,
+  obtain ⟨x', hx', rfl⟩ := mem_image_iff_bex.1 hx,
+  obtain ⟨y', hy', rfl⟩ := mem_image_iff_bex.1 hy,
+  exact ⟨a • x' + b • y', hs hx' hy' ha hb hab, by rw [f.map_add, f.map_smul, f.map_smul]⟩,
+end
+
+lemma strict_convex.is_linear_image (hs : strict_convex 𝕜 s) {f : E → F} (hf : is_linear_map 𝕜 f) :
+  strict_convex 𝕜 (f '' s) :=
+hs.linear_image $ hf.mk' f
+
+lemma strict_convex.linear_preimage {s : set F} (hs : strict_convex 𝕜 s) (f : E →ₗ[𝕜] F) :
+  strict_convex 𝕜 (s.preimage f) :=
+begin
+  intros x y hx hy a b ha hb hab,
+  rw [mem_preimage, f.map_add, f.map_smul, f.map_smul],
+  exact hs hx hy ha hb hab,
+end
+
+lemma strict_convex.is_linear_preimage {s : set F} (hs : strict_convex 𝕜 s) {f : E → F} (hf : is_linear_map 𝕜 f) :
+  strict_convex 𝕜 (preimage f s) :=
+hs.linear_preimage $ hf.mk' f
+
+lemma strict_convex.add {t : set E} (hs : strict_convex 𝕜 s) (ht : strict_convex 𝕜 t) : strict_convex 𝕜 (s + t) :=
+by { rw ← add_image_prod, exact (hs.prod ht).is_linear_image is_linear_map.is_linear_map_add }
+
+lemma strict_convex.translate (hs : strict_convex 𝕜 s) (z : E) : strict_convex 𝕜 ((λ x, z + x) '' s) :=
+begin
+  intros x y hx hy a b ha hb hab,
+  obtain ⟨x', hx', rfl⟩ := mem_image_iff_bex.1 hx,
+  obtain ⟨y', hy', rfl⟩ := mem_image_iff_bex.1 hy,
+  refine ⟨a • x' + b • y', hs hx' hy' ha hb hab, _⟩,
+  rw [smul_add, smul_add, add_add_add_comm, ←add_smul, hab, one_smul],
+end
+
+/-- The translation of a strict_convex set is also strict_convex. -/
+lemma strict_convex.translate_preimage_right (hs : strict_convex 𝕜 s) (z : E) : strict_convex 𝕜 ((λ x, z + x) ⁻¹' s) :=
+begin
+  intros x y hx hy a b ha hb hab,
+  have h := hs hx hy ha hb hab,
+  rwa [smul_add, smul_add, add_add_add_comm, ←add_smul, hab, one_smul] at h,
+end
+
+/-- The translation of a strict_convex set is also strict_convex. -/
+lemma strict_convex.translate_preimage_left (hs : strict_convex 𝕜 s) (z : E) : strict_convex 𝕜 ((λ x, x + z) ⁻¹' s) :=
+by simpa only [add_comm] using hs.translate_preimage_right z
+
+section ordered_add_comm_monoid
+variables [ordered_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β]
+
+lemma strict_convex_Iic (r : β) : strict_convex 𝕜 (Iic r) :=
+λ x y hx hy a b ha hb hab,
+calc
+  a • x + b • y
+      ≤ a • r + b • r
+      : add_le_add (smul_le_smul_of_nonneg hx ha) (smul_le_smul_of_nonneg hy hb)
+  ... = r : strict_convex.combo_self hab _
+
+lemma strict_convex_Ici (r : β) : strict_convex 𝕜 (Ici r) :=
+@convex_Iic 𝕜 (order_dual β) _ _ _ _ r
+
+lemma strict_convex_Icc (r s : β) : strict_convex 𝕜 (Icc r s) :=
+Ici_inter_Iic.subst ((convex_Ici r).inter $ strict_convex_Iic s)
+
+lemma strict_convex_halfspace_le {f : E → β} (h : is_linear_map 𝕜 f) (r : β) :
+  strict_convex 𝕜 {w | f w ≤ r} :=
+(convex_Iic r).is_linear_preimage h
+
+lemma strict_convex_halfspace_ge {f : E → β} (h : is_linear_map 𝕜 f) (r : β) :
+  strict_convex 𝕜 {w | r ≤ f w} :=
+(convex_Ici r).is_linear_preimage h
+
+lemma strict_convex_hyperplane {f : E → β} (h : is_linear_map 𝕜 f) (r : β) :
+  strict_convex 𝕜 {w | f w = r} :=
+begin
+  simp_rw le_antisymm_iff,
+  exact (convex_halfspace_le h r).inter (convex_halfspace_ge h r),
+end
+
+end ordered_add_comm_monoid
+
+section ordered_cancel_add_comm_monoid
+variables [ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β]
+
+lemma strict_convex_Iio (r : β) : strict_convex 𝕜 (Iio r) :=
+begin
+  intros x y hx hy a b ha hb hab,
+  obtain rfl | ha' := ha.eq_or_lt,
+  { rw zero_add at hab,
+    rwa [zero_smul, zero_add, hab, one_smul] },
+  rw mem_Iio at hx hy,
+  calc
+    a • x + b • y
+        < a • r + b • r
+        : add_lt_add_of_lt_of_le (smul_lt_smul_of_pos hx ha') (smul_le_smul_of_nonneg hy.le hb)
+    ... = r : strict_convex.combo_self hab _
+end
+
+lemma strict_convex_Ioi (r : β) : strict_convex 𝕜 (Ioi r) :=
+@convex_Iio 𝕜 (order_dual β) _ _ _ _ r
+
+lemma strict_convex_Ioo (r s : β) : strict_convex 𝕜 (Ioo r s) :=
+Ioi_inter_Iio.subst ((convex_Ioi r).inter $ strict_convex_Iio s)
+
+lemma strict_convex_Ico (r s : β) : strict_convex 𝕜 (Ico r s) :=
+Ici_inter_Iio.subst ((convex_Ici r).inter $ strict_convex_Iio s)
+
+lemma strict_convex_Ioc (r s : β) : strict_convex 𝕜 (Ioc r s) :=
+Ioi_inter_Iic.subst ((convex_Ioi r).inter $ strict_convex_Iic s)
+
+lemma strict_convex_halfspace_lt {f : E → β} (h : is_linear_map 𝕜 f) (r : β) :
+  strict_convex 𝕜 {w | f w < r} :=
+(convex_Iio r).is_linear_preimage h
+
+lemma strict_convex_halfspace_gt {f : E → β} (h : is_linear_map 𝕜 f) (r : β) :
+  strict_convex 𝕜 {w | r < f w} :=
+(convex_Ioi r).is_linear_preimage h
+
+end ordered_cancel_add_comm_monoid
+
+section linear_ordered_add_comm_monoid
+variables [linear_ordered_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β]
+
+lemma strict_convex_interval (r s : β) : strict_convex 𝕜 (interval r s) :=
+convex_Icc _ _
+
+end linear_ordered_add_comm_monoid
+end module
+end add_comm_monoid
+
+section linear_ordered_add_comm_monoid
+variables [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E]
+  [ordered_smul 𝕜 E] {s : set E} {f : E → β}
+
+lemma monotone_on.strict_convex_le (hf : monotone_on f s) (hs : strict_convex 𝕜 s) (r : β) :
+  strict_convex 𝕜 {x ∈ s | f x ≤ r} :=
+λ x y hx hy a b ha hb hab, ⟨hs hx.1 hy.1 ha hb hab,
+  (hf (hs hx.1 hy.1 ha hb hab) (max_rec' s hx.1 hy.1) (convex.combo_le_max x y ha hb hab)).trans
+    (max_rec' _ hx.2 hy.2)⟩
+
+lemma monotone_on.strict_convex_lt (hf : monotone_on f s) (hs : strict_convex 𝕜 s) (r : β) :
+  strict_convex 𝕜 {x ∈ s | f x < r} :=
+λ x y hx hy a b ha hb hab, ⟨hs hx.1 hy.1 ha hb hab,
+  (hf (hs hx.1 hy.1 ha hb hab) (max_rec' s hx.1 hy.1) (convex.combo_le_max x y ha hb hab)).trans_lt
+    (max_rec' _ hx.2 hy.2)⟩
+
+lemma monotone_on.strict_convex_ge (hf : monotone_on f s) (hs : strict_convex 𝕜 s) (r : β) :
+  strict_convex 𝕜 {x ∈ s | r ≤ f x} :=
+@monotone_on.strict_convex_le 𝕜 (order_dual E) (order_dual β) _ _ _ _ _ _ _ hf.dual hs r
+
+lemma monotone_on.strict_convex_gt (hf : monotone_on f s) (hs : strict_convex 𝕜 s) (r : β) :
+  strict_convex 𝕜 {x ∈ s | r < f x} :=
+@monotone_on.strict_convex_lt 𝕜 (order_dual E) (order_dual β) _ _ _ _ _ _ _ hf.dual hs r
+
+lemma antitone_on.strict_convex_le (hf : antitone_on f s) (hs : strict_convex 𝕜 s) (r : β) :
+  strict_convex 𝕜 {x ∈ s | f x ≤ r} :=
+@monotone_on.strict_convex_ge 𝕜 E (order_dual β) _ _ _ _ _ _ _ hf hs r
+
+lemma antitone_on.strict_convex_lt (hf : antitone_on f s) (hs : strict_convex 𝕜 s) (r : β) :
+  strict_convex 𝕜 {x ∈ s | f x < r} :=
+@monotone_on.strict_convex_gt 𝕜 E (order_dual β) _ _ _ _ _ _ _ hf hs r
+
+lemma antitone_on.strict_convex_ge (hf : antitone_on f s) (hs : strict_convex 𝕜 s) (r : β) :
+  strict_convex 𝕜 {x ∈ s | r ≤ f x} :=
+@monotone_on.strict_convex_le 𝕜 E (order_dual β) _ _ _ _ _ _ _ hf hs r
+
+lemma antitone_on.strict_convex_gt (hf : antitone_on f s) (hs : strict_convex 𝕜 s) (r : β) :
+  strict_convex 𝕜 {x ∈ s | r < f x} :=
+@monotone_on.strict_convex_lt 𝕜 E (order_dual β) _ _ _ _ _ _ _ hf hs r
+
+lemma monotone.strict_convex_le (hf : monotone f) (r : β) :
+  strict_convex 𝕜 {x | f x ≤ r} :=
+set.sep_univ.subst ((hf.monotone_on univ).strict_convex_le strict_convex_univ r)
+
+lemma monotone.strict_convex_lt (hf : monotone f) (r : β) :
+  strict_convex 𝕜 {x | f x ≤ r} :=
+set.sep_univ.subst ((hf.monotone_on univ).strict_convex_le strict_convex_univ r)
+
+lemma monotone.strict_convex_ge (hf : monotone f ) (r : β) :
+  strict_convex 𝕜 {x | r ≤ f x} :=
+set.sep_univ.subst ((hf.monotone_on univ).strict_convex_ge strict_convex_univ r)
+
+lemma monotone.strict_convex_gt (hf : monotone f) (r : β) :
+  strict_convex 𝕜 {x | f x ≤ r} :=
+set.sep_univ.subst ((hf.monotone_on univ).strict_convex_le strict_convex_univ r)
+
+lemma antitone.strict_convex_le (hf : antitone f) (r : β) :
+  strict_convex 𝕜 {x | f x ≤ r} :=
+set.sep_univ.subst ((hf.antitone_on univ).strict_convex_le strict_convex_univ r)
+
+lemma antitone.strict_convex_lt (hf : antitone f) (r : β) :
+  strict_convex 𝕜 {x | f x < r} :=
+set.sep_univ.subst ((hf.antitone_on univ).strict_convex_lt strict_convex_univ r)
+
+lemma antitone.strict_convex_ge (hf : antitone f) (r : β) :
+  strict_convex 𝕜 {x | r ≤ f x} :=
+set.sep_univ.subst ((hf.antitone_on univ).strict_convex_ge strict_convex_univ r)
+
+lemma antitone.strict_convex_gt (hf : antitone f) (r : β) :
+  strict_convex 𝕜 {x | r < f x} :=
+set.sep_univ.subst ((hf.antitone_on univ).strict_convex_gt strict_convex_univ r)
+
+end linear_ordered_add_comm_monoid
+
+section add_comm_group
+variables [add_comm_group E] [module 𝕜 E] {s t : set E}
+
+lemma strict_convex.combo_eq_vadd {a b : 𝕜} {x y : E} (h : a + b = 1) :
+  a • x + b • y = b • (y - x) + x :=
+calc
+  a • x + b • y = (b • y - b • x) + (a • x + b • x) : by abel
+            ... = b • (y - x) + x                   : by rw [smul_sub, strict_convex.combo_self h]
+
+lemma strict_convex.sub (hs : strict_convex 𝕜 s) (ht : strict_convex 𝕜 t) :
+  strict_convex 𝕜 ((λ x : E × E, x.1 - x.2) '' (s.prod t)) :=
+(hs.prod ht).is_linear_image is_linear_map.is_linear_map_sub
+
+lemma strict_convex_segment (x y : E) : strict_convex 𝕜 [x -[𝕜] y] :=
+begin
+  rintro p q ⟨ap, bp, hap, hbp, habp, rfl⟩ ⟨aq, bq, haq, hbq, habq, rfl⟩ a b ha hb hab,
+  refine ⟨a * ap + b * aq, a * bp + b * bq,
+    add_nonneg (mul_nonneg ha hap) (mul_nonneg hb haq),
+    add_nonneg (mul_nonneg ha hbp) (mul_nonneg hb hbq), _, _⟩,
+  { rw [add_add_add_comm, ←mul_add, ←mul_add, habp, habq, mul_one, mul_one, hab] },
+  { simp_rw [add_smul, mul_smul, smul_add],
+    exact add_add_add_comm _ _ _ _ }
+end
+
+lemma strict_convex_open_segment (a b : E) : strict_convex 𝕜 (open_segment 𝕜 a b) :=
+begin
+  rw strict_convex_iff_open_segment_subset,
+  rintro p q ⟨ap, bp, hap, hbp, habp, rfl⟩ ⟨aq, bq, haq, hbq, habq, rfl⟩ z ⟨a, b, ha, hb, hab, rfl⟩,
+  refine ⟨a * ap + b * aq, a * bp + b * bq,
+    add_pos (mul_pos ha hap) (mul_pos hb haq),
+    add_pos (mul_pos ha hbp) (mul_pos hb hbq), _, _⟩,
+  { rw [add_add_add_comm, ←mul_add, ←mul_add, habp, habq, mul_one, mul_one, hab] },
+  { simp_rw [add_smul, mul_smul, smul_add],
+    exact add_add_add_comm _ _ _ _ }
+end
+
+end add_comm_group
+end ordered_semiring
+
+section ordered_comm_semiring
+variables [ordered_comm_semiring 𝕜]
+
+section add_comm_monoid
+variables [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] {s : set E}
+
+lemma strict_convex.smul (hs : strict_convex 𝕜 s) (c : 𝕜) : strict_convex 𝕜 (c • s) :=
+hs.linear_image (linear_map.lsmul _ _ c)
+
+lemma strict_convex.smul_preimage (hs : strict_convex 𝕜 s) (c : 𝕜) : strict_convex 𝕜 ((λ z, c • z) ⁻¹' s) :=
+hs.linear_preimage (linear_map.lsmul _ _ c)
+
+lemma strict_convex.affinity (hs : strict_convex 𝕜 s) (z : E) (c : 𝕜) : strict_convex 𝕜 ((λ x, z + c • x) '' s) :=
+begin
+  have h := (hs.smul c).translate z,
+  rwa [←image_smul, image_image] at h,
+end
+
+end add_comm_monoid
+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 strict_convex.add_smul_mem (hs : strict_convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : x + y ∈ s)
+  {t : 𝕜} (ht : t ∈ Icc (0 : 𝕜) 1) : x + t • y ∈ s :=
+begin
+  have h : x + t • y = (1 - t) • x + t • (x + y),
+  { rw [smul_add, ←add_assoc, ←add_smul, sub_add_cancel, one_smul] },
+  rw h,
+  exact hs hx hy (sub_nonneg_of_le ht.2) ht.1 (sub_add_cancel _ _),
+end
+
+lemma strict_convex.smul_mem_of_zero_mem (hs : strict_convex 𝕜 s) {x : E} (zero_mem : (0 : E) ∈ s) (hx : x ∈ s)
+  {t : 𝕜} (ht : t ∈ Icc (0 : 𝕜) 1) : t • x ∈ s :=
+by simpa using hs.add_smul_mem zero_mem (by simpa using hx) ht
+
+lemma strict_convex.add_smul_sub_mem (h : strict_convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s)
+  {t : 𝕜} (ht : t ∈ Icc (0 : 𝕜) 1) : x + t • (y - x) ∈ s :=
+begin
+  apply h.segment_subset hx hy,
+  rw segment_eq_image',
+  exact mem_image_of_mem _ ht,
+end
+
+/-- Affine subspaces are strict_convex. -/
+lemma affine_subspace.strict_convex (Q : affine_subspace 𝕜 E) : strict_convex 𝕜 (Q : set E) :=
+begin
+  intros x y hx hy a b ha hb hab,
+  rw [eq_sub_of_add_eq hab, ← affine_map.line_map_apply_module],
+  exact affine_map.line_map_mem b hx hy,
+end
+
+/--
+Applying an affine map to an affine combination of two points yields
+an affine combination of the images.
+-/
+lemma strict_convex.combo_affine_apply {a b : 𝕜} {x y : E} {f : E →ᵃ[𝕜] F} (h : a + b = 1) :
+  f (a • x + b • y) = a • f x + b • f y :=
+begin
+  simp only [convex.combo_eq_vadd h, ← vsub_eq_sub],
+  exact f.apply_line_map _ _ _,
+end
+
+/-- The preimage of a strict_convex set under an affine map is strict_convex. -/
+lemma strict_convex.affine_preimage (f : E →ᵃ[𝕜] F) {s : set F} (hs : strict_convex 𝕜 s) :
+  strict_convex 𝕜 (f ⁻¹' s) :=
+begin
+  intros x y xs ys a b ha hb hab,
+  rw [mem_preimage, strict_convex.combo_affine_apply hab],
+  exact hs xs ys ha hb hab,
+end
+
+/-- The image of a strict_convex set under an affine map is strict_convex. -/
+lemma strict_convex.affine_image (f : E →ᵃ[𝕜] F) {s : set E} (hs : strict_convex 𝕜 s) :
+  strict_convex 𝕜 (f '' s) :=
+begin
+  rintro x y ⟨x', ⟨hx', hx'f⟩⟩ ⟨y', ⟨hy', hy'f⟩⟩ a b ha hb hab,
+  refine ⟨a • x' + b • y', ⟨hs hx' hy' ha hb hab, _⟩⟩,
+  rw [convex.combo_affine_apply hab, hx'f, hy'f]
+end
+
+lemma strict_convex.neg (hs : strict_convex 𝕜 s) : strict_convex 𝕜 ((λ z, -z) '' s) :=
+hs.is_linear_image is_linear_map.is_linear_map_neg
+
+lemma strict_convex.neg_preimage (hs : strict_convex 𝕜 s) : strict_convex 𝕜 ((λ z, -z) ⁻¹' s) :=
+hs.is_linear_preimage is_linear_map.is_linear_map_neg
+
+end add_comm_group
+end ordered_ring
+
+section linear_ordered_field
+variables [linear_ordered_field 𝕜]
+
+section add_comm_group
+variables [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] {s : set E}
+
+/-- Alternative definition of set strict_convexity, using division. -/
+lemma strict_convex_iff_div :
+  strict_convex 𝕜 s ↔ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄,
+    0 ≤ a → 0 ≤ b → 0 < a + b → (a/(a+b)) • x + (b/(a+b)) • y ∈ s :=
+⟨λ h x y hx hy a b ha hb hab, begin
+  apply h hx hy,
+  { have ha', from mul_le_mul_of_nonneg_left ha (inv_pos.2 hab).le,
+    rwa [mul_zero, ←div_eq_inv_mul] at ha' },
+  { have hb', from mul_le_mul_of_nonneg_left hb (inv_pos.2 hab).le,
+    rwa [mul_zero, ←div_eq_inv_mul] at hb' },
+  { rw ←add_div,
+    exact div_self hab.ne' }
+end, λ h x y hx hy a b ha hb hab,
+begin
+  have h', from h hx hy ha hb,
+  rw [hab, div_one, div_one] at h',
+  exact h' zero_lt_one
+end⟩
+
+lemma strict_convex.mem_smul_of_zero_mem (h : strict_convex 𝕜 s) {x : E} (zero_mem : (0 : E) ∈ s)
+  (hx : x ∈ s) {t : 𝕜} (ht : 1 ≤ t) :
+  x ∈ t • s :=
+begin
+  rw mem_smul_set_iff_inv_smul_mem₀ (zero_lt_one.trans_le ht).ne',
+  exact h.smul_mem_of_zero_mem zero_mem hx ⟨inv_nonneg.2 (zero_le_one.trans ht), inv_le_one ht⟩,
+end
+
+lemma strict_convex.add_smul (h_conv : strict_convex 𝕜 s) {p q : 𝕜} (hp : 0 ≤ p) (hq : 0 ≤ q) :
+  (p + q) • s = p • s + q • s :=
+begin
+  obtain rfl | hs := s.eq_empty_or_nonempty,
+  { simp_rw [smul_set_empty, add_empty] },
+  obtain rfl | hp' := hp.eq_or_lt,
+  { rw [zero_add, zero_smul_set hs, zero_add] },
+  obtain rfl | hq' := hq.eq_or_lt,
+  { rw [add_zero, zero_smul_set hs, add_zero] },
+  ext,
+  split,
+  { rintro ⟨v, hv, rfl⟩,
+    exact ⟨p • v, q • v, smul_mem_smul_set hv, smul_mem_smul_set hv, (add_smul _ _ _).symm⟩ },
+  { rintro ⟨v₁, v₂, ⟨v₁₁, h₁₂, rfl⟩, ⟨v₂₁, h₂₂, rfl⟩, rfl⟩,
+    have hpq := add_pos hp' hq',
+    exact mem_smul_set.2 ⟨_, h_conv h₁₂ h₂₂ (div_pos hp' hpq).le (div_pos hq' hpq).le
+      (by rw [←div_self hpq.ne', add_div] : p / (p + q) + q / (p + q) = 1),
+      by simp only [← mul_smul, smul_add, mul_div_cancel' _ hpq.ne']⟩ }
+end
+
+end add_comm_group
+end linear_ordered_field
+
+/-!
+#### Convex sets in an ordered space
+Relates `convex` and `ord_connected`.
+-/
+
+section
+
+lemma set.ord_connected.strict_convex_of_chain [ordered_semiring 𝕜] [ordered_add_comm_monoid E]
+  [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} (hs : s.ord_connected) (h : zorn.chain (≤) s) :
+  strict_convex 𝕜 s :=
+begin
+  intros x y hx hy a b ha hb hab,
+  obtain hxy | hyx := h.total_of_refl hx hy,
+  { refine hs.out hx hy (mem_Icc.2 ⟨_, _⟩),
+    calc
+      x   = a • x + b • x : (convex.combo_self hab _).symm
+      ... ≤ a • x + b • y : add_le_add_left (smul_le_smul_of_nonneg hxy hb) _,
+    calc
+      a • x + b • y
+          ≤ a • y + b • y : add_le_add_right (smul_le_smul_of_nonneg hxy ha) _
+      ... = y : strict_convex.combo_self hab _ },
+  { refine hs.out hy hx (mem_Icc.2 ⟨_, _⟩),
+    calc
+      y   = a • y + b • y : (convex.combo_self hab _).symm
+      ... ≤ a • x + b • y : add_le_add_right (smul_le_smul_of_nonneg hyx ha) _,
+    calc
+      a • x + b • y
+          ≤ a • x + b • x : add_le_add_left (smul_le_smul_of_nonneg hyx hb) _
+      ... = x : strict_convex.combo_self hab _ }
+end
+
+lemma set.ord_connected.strict_convex [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [module 𝕜 E]
+  [ordered_smul 𝕜 E] {s : set E} (hs : s.ord_connected) :
+  strict_convex 𝕜 s :=
+hs.strict_convex_of_chain (zorn.chain_of_trichotomous s)
+
+lemma strict_convex_iff_ord_connected [linear_ordered_field 𝕜] {s : set 𝕜} :
+  strict_convex 𝕜 s ↔ s.ord_connected :=
+begin
+  simp_rw [convex_iff_segment_subset, segment_eq_interval, ord_connected_iff_interval_subset],
+  exact forall_congr (λ x, forall_swap)
+end
+
+alias strict_convex_iff_ord_connected ↔ strict_convex.ord_connected _
+
+end
+
+/-! #### Convexity of submodules/subspaces -/
+
+section submodule
+open submodule
+
+lemma submodule.strict_convex [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (K : submodule 𝕜 E) :
+  strict_convex 𝕜 (↑K : set E) :=
+by { repeat {intro}, refine add_mem _ (smul_mem _ _ _) (smul_mem _ _ _); assumption }
+
+lemma subspace.strict_convex [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] (K : subspace 𝕜 E) :
+  strict_convex 𝕜 (↑K : set E) :=
+K.strict_convex
+
+end submodule
+
+/-! ### Simplex -/
+
+section simplex
+
+variables (𝕜) (ι : Type*) [ordered_semiring 𝕜] [fintype ι]
+
+/-- The standard simplex in the space of functions `ι → 𝕜` is the set of vectors with non-negative
+coordinates with total sum `1`. This is the free object in the category of strict_convex spaces. -/
+def std_simplex : set (ι → 𝕜) :=
+{f | (∀ x, 0 ≤ f x) ∧ ∑ x, f x = 1}
+
+lemma std_simplex_eq_inter :
+  std_simplex 𝕜 ι = (⋂ x, {f | 0 ≤ f x}) ∩ {f | ∑ x, f x = 1} :=
+by { ext f, simp only [std_simplex, set.mem_inter_eq, set.mem_Inter, set.mem_set_of_eq] }
+
+lemma strict_convex_std_simplex : strict_convex 𝕜 (std_simplex 𝕜 ι) :=
+begin
+  refine λ f g hf hg a b ha hb hab, ⟨λ x, _, _⟩,
+  { apply_rules [add_nonneg, mul_nonneg, hf.1, hg.1] },
+  { erw [finset.sum_add_distrib, ← finset.smul_sum, ← finset.smul_sum, hf.2, hg.2,
+      smul_eq_mul, smul_eq_mul, mul_one, mul_one],
+    exact hab }
+end
+
+variable {ι}
+
+lemma ite_eq_mem_std_simplex (i : ι) : (λ j, ite (i = j) (1:𝕜) 0) ∈ std_simplex 𝕜 ι :=
+⟨λ j, by simp only; split_ifs; norm_num, by rw [finset.sum_ite_eq, if_pos (finset.mem_univ _)]⟩
+
+end simplex

From c193a0a914f9714a8e57591dfe94c50d92a55c36 Mon Sep 17 00:00:00 2001
From: YaelDillies <yael.dillies@gmail.com>
Date: Sun, 28 Nov 2021 22:02:07 +0000
Subject: [PATCH 2/8] some more

---
 src/analysis/convex/strict.lean         | 675 ++++++++----------------
 src/topology/algebra/ordered/basic.lean |  15 +
 2 files changed, 243 insertions(+), 447 deletions(-)

diff --git a/src/analysis/convex/strict.lean b/src/analysis/convex/strict.lean
index ffd5f1d23760e..60a2308668b13 100644
--- a/src/analysis/convex/strict.lean
+++ b/src/analysis/convex/strict.lean
@@ -3,8 +3,9 @@ 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
 -/
-import analysis.convex.basic
-import topology.algebra.monoid
+import analysis.convex.function
+import topology.algebra.module
+import topology.algebra.ordered.basic
 
 /-!
 # Strictly strict_convex sets
@@ -22,11 +23,14 @@ This file defines strictly convex sets.
 
 -/
 
+open function set
+open_locale convex
+
 section ordered_semiring
-variables [ordered_semiring 𝕜]
+variables [ordered_semiring 𝕜] [topological_space E] [topological_space F]
 
 section add_comm_monoid
-variables [add_comm_monoid E] [topological_space E] [add_comm_monoid F] [topological_space F]
+variables [add_comm_monoid E] [add_comm_monoid F]
 
 section has_scalar
 variables (𝕜) [has_scalar 𝕜 E] [has_scalar 𝕜 F] (s : set E)
@@ -35,85 +39,58 @@ variables (𝕜) [has_scalar 𝕜 E] [has_scalar 𝕜 F] (s : set E)
 def strict_convex : Prop :=
 s.pairwise (λ x y, ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior s)
 
-variables {𝕜 s}
+variables {𝕜 s} {x y : E}
 
 lemma strict_convex_iff_open_segment_subset :
-  strict_convex 𝕜 s ↔ ∀ ⦃x y⦄, x ∈ s → y ∈ s → open_segment 𝕜 x y ⊆ interior s :=
+  strict_convex 𝕜 s ↔ s.pairwise (λ x y, open_segment 𝕜 x y ⊆ interior s) :=
 begin
   split,
-  { rintro h x y hx hy z ⟨a, b, ha, hb, hab, rfl⟩,
-    exact h hx hy ha hb hab },
-  { rintro h x y hx hy a b ha hb hab,
-    exact h hx hy ⟨a, b, ha, hb, hab, rfl⟩ }
+  { rintro h x hx y hy hxy z ⟨a, b, ha, hb, hab, rfl⟩,
+    exact h x hx y hy hxy ha hb hab },
+  { rintro h x hx y hy hxy a b ha hb hab,
+    exact h x hx y hy hxy ⟨a, b, ha, hb, hab, rfl⟩ }
 end
 
-lemma strict_convex.segment_subset (h : strict_convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
-  [x -[𝕜] y] ⊆ s :=
-convex_iff_segment_subset.1 h hx hy
-
-lemma strict_convex.open_segment_subset (h : strict_convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
-  open_segment 𝕜 x y ⊆ s :=
-(open_segment_subset_segment 𝕜 x y).trans (h.segment_subset hx hy)
-
-/-- Alternative definition of set strict_convexity, in terms of pointwise set operations. -/
-lemma strict_convex_iff_pointwise_add_subset :
-  strict_convex 𝕜 s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s :=
-iff.intro
-  begin
-    rintro hA a b ha hb hab w ⟨au, bv, ⟨u, hu, rfl⟩, ⟨v, hv, rfl⟩, rfl⟩,
-    exact hA hu hv ha hb hab
-  end
-  (λ h x y hx hy a b ha hb hab,
-    (h ha hb hab) (set.add_mem_add ⟨_, hx, rfl⟩ ⟨_, hy, rfl⟩))
-
-lemma strict_convex_empty : strict_convex 𝕜 (∅ : set E) := by finish
-
-lemma strict_convex_univ : strict_convex 𝕜 (set.univ : set E) := λ _ _ _ _ _ _ _ _ _, trivial
-
-lemma strict_convex.inter {t : set E} (hs : strict_convex 𝕜 s) (ht : strict_convex 𝕜 t) : strict_convex 𝕜 (s ∩ t) :=
-λ x y (hx : x ∈ s ∩ t) (hy : y ∈ s ∩ t) a b (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1),
-  ⟨hs hx.left hy.left ha hb hab, ht hx.right hy.right ha hb hab⟩
-
-lemma strict_convex_sInter {S : set (set E)} (h : ∀ s ∈ S, strict_convex 𝕜 s) : strict_convex 𝕜 (⋂₀ S) :=
-assume x y hx hy a b ha hb hab s hs,
-h s hs (hx s hs) (hy s hs) ha hb hab
+lemma strict_convex.open_segment_subset (hs : strict_convex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s)
+  (h : x ≠ y) :
+  open_segment 𝕜 x y ⊆ interior s :=
+strict_convex_iff_open_segment_subset.1 hs _ hx _ hy h
 
-lemma strict_convex_Inter {ι : Sort*} {s : ι → set E} (h : ∀ i : ι, strict_convex 𝕜 (s i)) :
-  strict_convex 𝕜 (⋂ i, s i) :=
-(sInter_range s) ▸ strict_convex_sInter $ forall_range_iff.2 h
+lemma strict_convex_empty : strict_convex 𝕜 (∅ : set E) := pairwise_empty _
 
-lemma strict_convex.prod {s : set E} {t : set F} (hs : strict_convex 𝕜 s) (ht : strict_convex 𝕜 t) :
-  strict_convex 𝕜 (s.prod t) :=
+lemma strict_convex_univ : strict_convex 𝕜 (univ : set E) :=
 begin
-  intros x y hx hy a b ha hb hab,
-  apply mem_prod.2,
-  exact ⟨hs (mem_prod.1 hx).1 (mem_prod.1 hy).1 ha hb hab,
-        ht (mem_prod.1 hx).2 (mem_prod.1 hy).2 ha hb hab⟩
+  intros x hx y hy hxy a b ha hb hab,
+  rw interior_univ,
+  exact mem_univ _,
 end
 
-lemma strict_convex_pi {ι : Type*} {E : ι → Type*} [Π i, add_comm_monoid (E i)]
-  [Π i, has_scalar 𝕜 (E i)] {s : set ι} {t : Π i, set (E i)} (ht : ∀ i, strict_convex 𝕜 (t i)) :
-  strict_convex 𝕜 (s.pi t) :=
-λ x y hx hy a b ha hb hab i hi, ht i (hx i hi) (hy i hi) ha hb hab
+lemma strict_convex.inter {t : set E} (hs : strict_convex 𝕜 s) (ht : strict_convex 𝕜 t) :
+  strict_convex 𝕜 (s ∩ t) :=
+begin
+  intros x hx y hy hxy a b ha hb hab,
+  rw interior_inter,
+  exact ⟨hs x hx.1 y hy.1 hxy ha hb hab, ht x hx.2 y hy.2 hxy ha hb hab⟩,
+end
 
 lemma directed.strict_convex_Union {ι : Sort*} {s : ι → set E} (hdir : directed (⊆) s)
-  (hc : ∀ ⦃i : ι⦄, strict_convex 𝕜 (s i)) :
+  (hs : ∀ ⦃i : ι⦄, strict_convex 𝕜 (s i)) :
   strict_convex 𝕜 (⋃ i, s i) :=
 begin
-  rintro x y hx hy a b ha hb hab,
-  rw mem_Union at ⊢ hx hy,
+  rintro x hx y hy hxy a b ha hb hab,
+  rw mem_Union at hx hy,
   obtain ⟨i, hx⟩ := hx,
   obtain ⟨j, hy⟩ := hy,
   obtain ⟨k, hik, hjk⟩ := hdir i j,
-  exact ⟨k, hc (hik hx) (hjk hy) ha hb hab⟩,
+  exact interior_mono (subset_Union s k) (hs _ (hik hx) _ (hjk hy) hxy ha hb hab),
 end
 
-lemma directed_on.strict_convex_sUnion {c : set (set E)} (hdir : directed_on (⊆) c)
-  (hc : ∀ ⦃A : set E⦄, A ∈ c → strict_convex 𝕜 A) :
-  strict_convex 𝕜 (⋃₀c) :=
+lemma directed_on.strict_convex_sUnion {S : set (set E)} (hdir : directed_on (⊆) S)
+  (hS : ∀ s ∈ S, strict_convex 𝕜 s) :
+  strict_convex 𝕜 (⋃₀ S) :=
 begin
   rw sUnion_eq_Union,
-  exact (directed_on_iff_directed.1 hdir).strict_convex_Union (λ A, hc A.2),
+  exact (directed_on_iff_directed.1 hdir).strict_convex_Union (λ s, hS _ s.2),
 end
 
 end has_scalar
@@ -122,387 +99,233 @@ section module
 variables [module 𝕜 E] [module 𝕜 F] {s : set E}
 
 lemma strict_convex.convex (hs : strict_convex 𝕜 s) : convex 𝕜 s :=
-convex_iff_forall_pos.2 $ λ x y hx hy a b ha hb hab, interior_subset $ hs hx hy ha hb hab
+convex_iff_pairwise_pos.2 $ λ x hx y hy hxy a b ha hb hab,
+  interior_subset $ hs x hx y hy hxy ha hb hab
 
 lemma convex.strict_convex (h : is_open s) (hs : convex 𝕜 s) : strict_convex 𝕜 s :=
-λ x y hx hy a b ha hb hab, h.interior_eq.symm ▸ hs hx hy ha hb hab
+λ x hx y hy _ a b ha hb hab, h.interior_eq.symm ▸ hs hx hy ha.le hb.le hab
 
 lemma is_open.strict_convex_iff (h : is_open s) : strict_convex 𝕜 s ↔ convex 𝕜 s :=
 ⟨strict_convex.convex, convex.strict_convex h⟩
 
-lemma strict_convex_iff_forall_pos :
-  strict_convex 𝕜 s ↔ ∀ ⦃x y⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1
-  → a • x + b • y ∈ s :=
-begin
-  refine ⟨λ h x y hx hy a b ha hb hab, h hx hy ha.le hb.le hab, _⟩,
-  intros h x y hx hy a b ha hb hab,
-  cases ha.eq_or_lt with ha ha,
-  { subst a, rw [zero_add] at hab, simp [hab, hy] },
-  cases hb.eq_or_lt with hb hb,
-  { subst b, rw [add_zero] at hab, simp [hab, hx] },
-  exact h hx hy ha hb hab
-end
-
-lemma strict_convex_iff_pairwise_pos :
-  strict_convex 𝕜 s ↔ s.pairwise (λ x y, ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s) :=
-begin
-  refine ⟨λ h x hx y hy _ a b ha hb hab, h hx hy ha.le hb.le hab, _⟩,
-  intros h x y hx hy a b ha hb hab,
-  obtain rfl | ha' := ha.eq_or_lt,
-  { rw [zero_add] at hab, rwa [hab, zero_smul, one_smul, zero_add] },
-  obtain rfl | hb' := hb.eq_or_lt,
-  { rw [add_zero] at hab, rwa [hab, zero_smul, one_smul, add_zero] },
-  obtain rfl | hxy := eq_or_ne x y,
-  { rwa strict_convex.combo_self hab },
-  exact h _ hx _ hy hxy ha' hb' hab,
-end
-
-lemma strict_convex_iff_open_segment_subset :
-  strict_convex 𝕜 s ↔ ∀ ⦃x y⦄, x ∈ s → y ∈ s → open_segment 𝕜 x y ⊆ s :=
-begin
-  rw strict_convex_iff_segment_subset,
-  exact forall₂_congr (λ x y, forall₂_congr $ λ hx hy,
-    (open_segment_subset_iff_segment_subset hx hy).symm),
-end
+lemma strict_convex_singleton (c : E) : strict_convex 𝕜 ({c} : set E) := pairwise_singleton _ _
 
-lemma strict_convex_singleton (c : E) : strict_convex 𝕜 ({c} : set E) :=
-begin
-  intros x y hx hy a b ha hb hab,
-  rw [set.eq_of_mem_singleton hx, set.eq_of_mem_singleton hy, ←add_smul, hab, one_smul],
-  exact mem_singleton c
-end
+lemma set.subsingleton.strict_convex (hs : s.subsingleton) : strict_convex 𝕜 s := hs.pairwise _
 
-lemma strict_convex.linear_image (hs : strict_convex 𝕜 s) (f : E →ₗ[𝕜] F) : strict_convex 𝕜 (s.image f) :=
+lemma strict_convex.linear_image (hs : strict_convex 𝕜 s) (f : E →ₗ[𝕜] F) (hf : is_open_map f) :
+  strict_convex 𝕜 (s.image f) :=
 begin
-  intros x y hx hy a b ha hb hab,
-  obtain ⟨x', hx', rfl⟩ := mem_image_iff_bex.1 hx,
-  obtain ⟨y', hy', rfl⟩ := mem_image_iff_bex.1 hy,
-  exact ⟨a • x' + b • y', hs hx' hy' ha hb hab, by rw [f.map_add, f.map_smul, f.map_smul]⟩,
+  rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ hxy a b ha hb hab,
+  exact hf.image_interior_subset _
+    ⟨a • x + b • y, hs _ hx _ hy (ne_of_apply_ne _ hxy) ha hb hab,
+    by rw [f.map_add, f.map_smul, f.map_smul]⟩,
 end
 
-lemma strict_convex.is_linear_image (hs : strict_convex 𝕜 s) {f : E → F} (hf : is_linear_map 𝕜 f) :
+lemma strict_convex.is_linear_image (hs : strict_convex 𝕜 s) {f : E → F} (h : is_linear_map 𝕜 f)
+  (hf : is_open_map f) :
   strict_convex 𝕜 (f '' s) :=
-hs.linear_image $ hf.mk' f
+hs.linear_image (h.mk' f) hf
 
-lemma strict_convex.linear_preimage {s : set F} (hs : strict_convex 𝕜 s) (f : E →ₗ[𝕜] F) :
+lemma strict_convex.linear_preimage {s : set F} (hs : strict_convex 𝕜 s) (f : E →ₗ[𝕜] F)
+  (hf : continuous f) (hfinj : injective f) :
   strict_convex 𝕜 (s.preimage f) :=
 begin
-  intros x y hx hy a b ha hb hab,
+  intros x hx y hy hxy a b ha hb hab,
+  refine preimage_interior_subset_interior_preimage hf _,
   rw [mem_preimage, f.map_add, f.map_smul, f.map_smul],
-  exact hs hx hy ha hb hab,
+  exact hs _ hx _ hy (hfinj.ne hxy) ha hb hab,
 end
 
-lemma strict_convex.is_linear_preimage {s : set F} (hs : strict_convex 𝕜 s) {f : E → F} (hf : is_linear_map 𝕜 f) :
-  strict_convex 𝕜 (preimage f s) :=
-hs.linear_preimage $ hf.mk' f
-
-lemma strict_convex.add {t : set E} (hs : strict_convex 𝕜 s) (ht : strict_convex 𝕜 t) : strict_convex 𝕜 (s + t) :=
-by { rw ← add_image_prod, exact (hs.prod ht).is_linear_image is_linear_map.is_linear_map_add }
+section linear_ordered_cancel_add_comm_monoid
+variables [topological_space β] [linear_ordered_cancel_add_comm_monoid β] [order_topology β]
+  [module 𝕜 β] [ordered_smul 𝕜 β]
 
-lemma strict_convex.translate (hs : strict_convex 𝕜 s) (z : E) : strict_convex 𝕜 ((λ x, z + x) '' s) :=
+lemma strict_convex_Iic [no_top_order β] (r : β) : strict_convex 𝕜 (Iic r) :=
 begin
-  intros x y hx hy a b ha hb hab,
-  obtain ⟨x', hx', rfl⟩ := mem_image_iff_bex.1 hx,
-  obtain ⟨y', hy', rfl⟩ := mem_image_iff_bex.1 hy,
-  refine ⟨a • x' + b • y', hs hx' hy' ha hb hab, _⟩,
-  rw [smul_add, smul_add, add_add_add_comm, ←add_smul, hab, one_smul],
+  rintro x (hx : x ≤ r) y (hy : y ≤ r) hxy a b ha hb hab,
+  refine (subset_interior_iff_subset_of_open is_open_Iio).2 Iio_subset_Iic_self _,
+  rw ←convex.combo_self hab r,
+  obtain rfl | hx := hx.eq_or_lt,
+  { exact add_lt_add_left (smul_lt_smul_of_pos (hy.lt_of_ne hxy.symm) hb) _ },
+  obtain rfl | hy := hy.eq_or_lt,
+  { exact add_lt_add_right (smul_lt_smul_of_pos hx ha) _ },
+  { exact add_lt_add (smul_lt_smul_of_pos hx ha) (smul_lt_smul_of_pos hy hb) }
 end
 
-/-- The translation of a strict_convex set is also strict_convex. -/
-lemma strict_convex.translate_preimage_right (hs : strict_convex 𝕜 s) (z : E) : strict_convex 𝕜 ((λ x, z + x) ⁻¹' s) :=
-begin
-  intros x y hx hy a b ha hb hab,
-  have h := hs hx hy ha hb hab,
-  rwa [smul_add, smul_add, add_add_add_comm, ←add_smul, hab, one_smul] at h,
-end
-
-/-- The translation of a strict_convex set is also strict_convex. -/
-lemma strict_convex.translate_preimage_left (hs : strict_convex 𝕜 s) (z : E) : strict_convex 𝕜 ((λ x, x + z) ⁻¹' s) :=
-by simpa only [add_comm] using hs.translate_preimage_right z
+lemma strict_convex_Ici [no_bot_order β] (r : β) : strict_convex 𝕜 (Ici r) :=
+@strict_convex_Iic 𝕜 (order_dual β) _ _ _ _ _ _ _ r
 
-section ordered_add_comm_monoid
-variables [ordered_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β]
-
-lemma strict_convex_Iic (r : β) : strict_convex 𝕜 (Iic r) :=
-λ x y hx hy a b ha hb hab,
-calc
-  a • x + b • y
-      ≤ a • r + b • r
-      : add_le_add (smul_le_smul_of_nonneg hx ha) (smul_le_smul_of_nonneg hy hb)
-  ... = r : strict_convex.combo_self hab _
-
-lemma strict_convex_Ici (r : β) : strict_convex 𝕜 (Ici r) :=
-@convex_Iic 𝕜 (order_dual β) _ _ _ _ r
-
-lemma strict_convex_Icc (r s : β) : strict_convex 𝕜 (Icc r s) :=
-Ici_inter_Iic.subst ((convex_Ici r).inter $ strict_convex_Iic s)
-
-lemma strict_convex_halfspace_le {f : E → β} (h : is_linear_map 𝕜 f) (r : β) :
-  strict_convex 𝕜 {w | f w ≤ r} :=
-(convex_Iic r).is_linear_preimage h
-
-lemma strict_convex_halfspace_ge {f : E → β} (h : is_linear_map 𝕜 f) (r : β) :
-  strict_convex 𝕜 {w | r ≤ f w} :=
-(convex_Ici r).is_linear_preimage h
-
-lemma strict_convex_hyperplane {f : E → β} (h : is_linear_map 𝕜 f) (r : β) :
-  strict_convex 𝕜 {w | f w = r} :=
-begin
-  simp_rw le_antisymm_iff,
-  exact (convex_halfspace_le h r).inter (convex_halfspace_ge h r),
-end
-
-end ordered_add_comm_monoid
-
-section ordered_cancel_add_comm_monoid
-variables [ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β]
+lemma strict_convex_Icc [no_top_order β] [no_bot_order β] (r s : β) : strict_convex 𝕜 (Icc r s) :=
+(strict_convex_Ici r).inter $ strict_convex_Iic s
 
 lemma strict_convex_Iio (r : β) : strict_convex 𝕜 (Iio r) :=
-begin
-  intros x y hx hy a b ha hb hab,
-  obtain rfl | ha' := ha.eq_or_lt,
-  { rw zero_add at hab,
-    rwa [zero_smul, zero_add, hab, one_smul] },
-  rw mem_Iio at hx hy,
-  calc
-    a • x + b • y
-        < a • r + b • r
-        : add_lt_add_of_lt_of_le (smul_lt_smul_of_pos hx ha') (smul_le_smul_of_nonneg hy.le hb)
-    ... = r : strict_convex.combo_self hab _
-end
+(convex_Iio r).strict_convex is_open_Iio
 
 lemma strict_convex_Ioi (r : β) : strict_convex 𝕜 (Ioi r) :=
-@convex_Iio 𝕜 (order_dual β) _ _ _ _ r
+(convex_Ioi r).strict_convex is_open_Ioi
 
 lemma strict_convex_Ioo (r s : β) : strict_convex 𝕜 (Ioo r s) :=
-Ioi_inter_Iio.subst ((convex_Ioi r).inter $ strict_convex_Iio s)
-
-lemma strict_convex_Ico (r s : β) : strict_convex 𝕜 (Ico r s) :=
-Ici_inter_Iio.subst ((convex_Ici r).inter $ strict_convex_Iio s)
-
-lemma strict_convex_Ioc (r s : β) : strict_convex 𝕜 (Ioc r s) :=
-Ioi_inter_Iic.subst ((convex_Ioi r).inter $ strict_convex_Iic s)
+(strict_convex_Ioi r).inter $ strict_convex_Iio s
 
-lemma strict_convex_halfspace_lt {f : E → β} (h : is_linear_map 𝕜 f) (r : β) :
-  strict_convex 𝕜 {w | f w < r} :=
-(convex_Iio r).is_linear_preimage h
+lemma strict_convex_Ico [no_bot_order β] (r s : β) : strict_convex 𝕜 (Ico r s) :=
+(strict_convex_Ici r).inter $ strict_convex_Iio s
 
-lemma strict_convex_halfspace_gt {f : E → β} (h : is_linear_map 𝕜 f) (r : β) :
-  strict_convex 𝕜 {w | r < f w} :=
-(convex_Ioi r).is_linear_preimage h
+lemma strict_convex_Ioc [no_top_order β] (r s : β) : strict_convex 𝕜 (Ioc r s) :=
+(strict_convex_Ioi r).inter $ strict_convex_Iic s
 
-end ordered_cancel_add_comm_monoid
+lemma strict_convex_interval [no_top_order β] [no_bot_order β] (r s : β) :
+  strict_convex 𝕜 (interval r s) :=
+strict_convex_Icc _ _
 
-section linear_ordered_add_comm_monoid
-variables [linear_ordered_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β]
-
-lemma strict_convex_interval (r s : β) : strict_convex 𝕜 (interval r s) :=
-convex_Icc _ _
-
-end linear_ordered_add_comm_monoid
+end linear_ordered_cancel_add_comm_monoid
 end module
 end add_comm_monoid
 
-section linear_ordered_add_comm_monoid
-variables [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E]
-  [ordered_smul 𝕜 E] {s : set E} {f : E → β}
-
-lemma monotone_on.strict_convex_le (hf : monotone_on f s) (hs : strict_convex 𝕜 s) (r : β) :
-  strict_convex 𝕜 {x ∈ s | f x ≤ r} :=
-λ x y hx hy a b ha hb hab, ⟨hs hx.1 hy.1 ha hb hab,
-  (hf (hs hx.1 hy.1 ha hb hab) (max_rec' s hx.1 hy.1) (convex.combo_le_max x y ha hb hab)).trans
-    (max_rec' _ hx.2 hy.2)⟩
-
-lemma monotone_on.strict_convex_lt (hf : monotone_on f s) (hs : strict_convex 𝕜 s) (r : β) :
-  strict_convex 𝕜 {x ∈ s | f x < r} :=
-λ x y hx hy a b ha hb hab, ⟨hs hx.1 hy.1 ha hb hab,
-  (hf (hs hx.1 hy.1 ha hb hab) (max_rec' s hx.1 hy.1) (convex.combo_le_max x y ha hb hab)).trans_lt
-    (max_rec' _ hx.2 hy.2)⟩
-
-lemma monotone_on.strict_convex_ge (hf : monotone_on f s) (hs : strict_convex 𝕜 s) (r : β) :
-  strict_convex 𝕜 {x ∈ s | r ≤ f x} :=
-@monotone_on.strict_convex_le 𝕜 (order_dual E) (order_dual β) _ _ _ _ _ _ _ hf.dual hs r
-
-lemma monotone_on.strict_convex_gt (hf : monotone_on f s) (hs : strict_convex 𝕜 s) (r : β) :
-  strict_convex 𝕜 {x ∈ s | r < f x} :=
-@monotone_on.strict_convex_lt 𝕜 (order_dual E) (order_dual β) _ _ _ _ _ _ _ hf.dual hs r
-
-lemma antitone_on.strict_convex_le (hf : antitone_on f s) (hs : strict_convex 𝕜 s) (r : β) :
-  strict_convex 𝕜 {x ∈ s | f x ≤ r} :=
-@monotone_on.strict_convex_ge 𝕜 E (order_dual β) _ _ _ _ _ _ _ hf hs r
-
-lemma antitone_on.strict_convex_lt (hf : antitone_on f s) (hs : strict_convex 𝕜 s) (r : β) :
-  strict_convex 𝕜 {x ∈ s | f x < r} :=
-@monotone_on.strict_convex_gt 𝕜 E (order_dual β) _ _ _ _ _ _ _ hf hs r
-
-lemma antitone_on.strict_convex_ge (hf : antitone_on f s) (hs : strict_convex 𝕜 s) (r : β) :
-  strict_convex 𝕜 {x ∈ s | r ≤ f x} :=
-@monotone_on.strict_convex_le 𝕜 E (order_dual β) _ _ _ _ _ _ _ hf hs r
-
-lemma antitone_on.strict_convex_gt (hf : antitone_on f s) (hs : strict_convex 𝕜 s) (r : β) :
-  strict_convex 𝕜 {x ∈ s | r < f x} :=
-@monotone_on.strict_convex_lt 𝕜 E (order_dual β) _ _ _ _ _ _ _ hf hs r
-
-lemma monotone.strict_convex_le (hf : monotone f) (r : β) :
-  strict_convex 𝕜 {x | f x ≤ r} :=
-set.sep_univ.subst ((hf.monotone_on univ).strict_convex_le strict_convex_univ r)
-
-lemma monotone.strict_convex_lt (hf : monotone f) (r : β) :
-  strict_convex 𝕜 {x | f x ≤ r} :=
-set.sep_univ.subst ((hf.monotone_on univ).strict_convex_le strict_convex_univ r)
-
-lemma monotone.strict_convex_ge (hf : monotone f ) (r : β) :
-  strict_convex 𝕜 {x | r ≤ f x} :=
-set.sep_univ.subst ((hf.monotone_on univ).strict_convex_ge strict_convex_univ r)
+section add_cancel_comm_monoid
+variables [add_cancel_comm_monoid E] [has_continuous_add E] [module 𝕜 E] {s : set E}
 
-lemma monotone.strict_convex_gt (hf : monotone f) (r : β) :
-  strict_convex 𝕜 {x | f x ≤ r} :=
-set.sep_univ.subst ((hf.monotone_on univ).strict_convex_le strict_convex_univ r)
-
-lemma antitone.strict_convex_le (hf : antitone f) (r : β) :
-  strict_convex 𝕜 {x | f x ≤ r} :=
-set.sep_univ.subst ((hf.antitone_on univ).strict_convex_le strict_convex_univ r)
-
-lemma antitone.strict_convex_lt (hf : antitone f) (r : β) :
-  strict_convex 𝕜 {x | f x < r} :=
-set.sep_univ.subst ((hf.antitone_on univ).strict_convex_lt strict_convex_univ r)
-
-lemma antitone.strict_convex_ge (hf : antitone f) (r : β) :
-  strict_convex 𝕜 {x | r ≤ f x} :=
-set.sep_univ.subst ((hf.antitone_on univ).strict_convex_ge strict_convex_univ r)
+/-- The translation of a strict_convex set is also strict_convex. -/
+lemma strict_convex.preimage_add_right (hs : strict_convex 𝕜 s) (z : E) :
+  strict_convex 𝕜 ((λ x, z + x) ⁻¹' s) :=
+begin
+  intros x hx y hy hxy a b ha hb hab,
+  refine preimage_interior_subset_interior_preimage (continuous_add_left _) _,
+  have h := hs _ hx _ hy ((add_right_injective _).ne hxy) ha hb hab,
+  rwa [smul_add, smul_add, add_add_add_comm, ←add_smul, hab, one_smul] at h,
+end
 
-lemma antitone.strict_convex_gt (hf : antitone f) (r : β) :
-  strict_convex 𝕜 {x | r < f x} :=
-set.sep_univ.subst ((hf.antitone_on univ).strict_convex_gt strict_convex_univ r)
+/-- The translation of a strict_convex set is also strict_convex. -/
+lemma strict_convex.preimage_add_left (hs : strict_convex 𝕜 s) (z : E) :
+  strict_convex 𝕜 ((λ x, x + z) ⁻¹' s) :=
+by simpa only [add_comm] using hs.preimage_add_right z
 
-end linear_ordered_add_comm_monoid
+end add_cancel_comm_monoid
 
 section add_comm_group
 variables [add_comm_group E] [module 𝕜 E] {s t : set E}
 
-lemma strict_convex.combo_eq_vadd {a b : 𝕜} {x y : E} (h : a + b = 1) :
-  a • x + b • y = b • (y - x) + x :=
-calc
-  a • x + b • y = (b • y - b • x) + (a • x + b • x) : by abel
-            ... = b • (y - x) + x                   : by rw [smul_sub, strict_convex.combo_self h]
+lemma strict_convex.add_left [has_continuous_add E] (hs : strict_convex 𝕜 s) (z : E) :
+  strict_convex 𝕜 ((λ x, z + x) '' s) :=
+begin
+  rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ hxy a b ha hb hab,
+  refine (is_open_map_add_left _).image_interior_subset _ _,
+  refine ⟨a • x + b • y, hs _ hx _ hy (ne_of_apply_ne _ hxy) ha hb hab, _⟩,
+  rw [smul_add, smul_add, add_add_add_comm, ←add_smul, hab, one_smul],
+end
 
-lemma strict_convex.sub (hs : strict_convex 𝕜 s) (ht : strict_convex 𝕜 t) :
-  strict_convex 𝕜 ((λ x : E × E, x.1 - x.2) '' (s.prod t)) :=
-(hs.prod ht).is_linear_image is_linear_map.is_linear_map_sub
+lemma strict_convex.add_right [has_continuous_add E] (hs : strict_convex 𝕜 s) (z : E) :
+  strict_convex 𝕜 ((λ x, x + z) '' s) :=
+by simpa only [add_comm] using hs.add_left z
 
-lemma strict_convex_segment (x y : E) : strict_convex 𝕜 [x -[𝕜] y] :=
+lemma strict_convex.add [has_continuous_add E] {t : set E} (hs : strict_convex 𝕜 s)
+  (ht : strict_convex 𝕜 t) :
+  strict_convex 𝕜 (s + t) :=
 begin
-  rintro p q ⟨ap, bp, hap, hbp, habp, rfl⟩ ⟨aq, bq, haq, hbq, habq, rfl⟩ a b ha hb hab,
-  refine ⟨a * ap + b * aq, a * bp + b * bq,
-    add_nonneg (mul_nonneg ha hap) (mul_nonneg hb haq),
-    add_nonneg (mul_nonneg ha hbp) (mul_nonneg hb hbq), _, _⟩,
-  { rw [add_add_add_comm, ←mul_add, ←mul_add, habp, habq, mul_one, mul_one, hab] },
-  { simp_rw [add_smul, mul_smul, smul_add],
-    exact add_add_add_comm _ _ _ _ }
+  rintro _ ⟨v, w, hv, hw, rfl⟩ _ ⟨x, y, hx, hy, rfl⟩ h a b ha hb hab,
+  rw [smul_add, smul_add, add_add_add_comm],
+  obtain rfl | hvx := eq_or_ne v x,
+  { rw convex.combo_self hab,
+    suffices : v + (a • w + b • y) ∈ interior ({v} + t),
+    { exact interior_mono (add_subset_add (singleton_subset_iff.2 hv) (subset.refl _)) this },
+    rw singleton_add,
+    exact (is_open_map_add_left _).image_interior_subset _
+      (mem_image_of_mem _ $ ht _ hw _ hy (ne_of_apply_ne _ h) ha hb hab) },
+  obtain rfl | hvx := eq_or_ne w y,
+  { rw convex.combo_self hab,
+    suffices : a • v + b • x + w ∈ interior (s + {w}),
+    { exact interior_mono (add_subset_add (subset.refl _) (singleton_subset_iff.2 hw)) this },
+    rw add_singleton,
+    exact (is_open_map_add_right _).image_interior_subset _
+      (mem_image_of_mem _ $ hs _ hv _ hx hvx ha hb hab) },
+  sorry
 end
 
-lemma strict_convex_open_segment (a b : E) : strict_convex 𝕜 (open_segment 𝕜 a b) :=
-begin
-  rw strict_convex_iff_open_segment_subset,
-  rintro p q ⟨ap, bp, hap, hbp, habp, rfl⟩ ⟨aq, bq, haq, hbq, habq, rfl⟩ z ⟨a, b, ha, hb, hab, rfl⟩,
-  refine ⟨a * ap + b * aq, a * bp + b * bq,
-    add_pos (mul_pos ha hap) (mul_pos hb haq),
-    add_pos (mul_pos ha hbp) (mul_pos hb hbq), _, _⟩,
-  { rw [add_add_add_comm, ←mul_add, ←mul_add, habp, habq, mul_one, mul_one, hab] },
-  { simp_rw [add_smul, mul_smul, smul_add],
-    exact add_add_add_comm _ _ _ _ }
+lemma strict_convex.sub {s : set (E × E)} (hs : strict_convex 𝕜 s) :
+  strict_convex 𝕜 ((λ x : E × E, x.1 - x.2) '' s) :=
+hs.is_linear_image is_linear_map.is_linear_map_sub begin
+  sorry
 end
 
 end add_comm_group
 end ordered_semiring
 
 section ordered_comm_semiring
-variables [ordered_comm_semiring 𝕜]
-
-section add_comm_monoid
-variables [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] {s : set E}
+variables [ordered_comm_semiring 𝕜] [topological_space E]
 
-lemma strict_convex.smul (hs : strict_convex 𝕜 s) (c : 𝕜) : strict_convex 𝕜 (c • s) :=
-hs.linear_image (linear_map.lsmul _ _ c)
-
-lemma strict_convex.smul_preimage (hs : strict_convex 𝕜 s) (c : 𝕜) : strict_convex 𝕜 ((λ z, c • z) ⁻¹' s) :=
-hs.linear_preimage (linear_map.lsmul _ _ c)
+section add_comm_group
+variables [add_comm_group E] [module 𝕜 E] [no_zero_smul_divisors 𝕜 E] {s : set E}
 
-lemma strict_convex.affinity (hs : strict_convex 𝕜 s) (z : E) (c : 𝕜) : strict_convex 𝕜 ((λ x, z + c • x) '' s) :=
+lemma strict_convex.preimage_smul (hs : strict_convex 𝕜 s) (c : 𝕜) :
+  strict_convex 𝕜 ((λ z, c • z) ⁻¹' s) :=
 begin
-  have h := (hs.smul c).translate z,
-  rwa [←image_smul, image_image] at h,
+  classical,
+  obtain rfl | hc := eq_or_ne c 0,
+  { simp_rw [zero_smul, preimage_const],
+    split_ifs,
+    { exact strict_convex_univ },
+    { exact strict_convex_empty } },
+  refine hs.linear_preimage (linear_map.lsmul _ _ c) _ (smul_right_injective E hc),
+  sorry
 end
 
-end add_comm_monoid
+end add_comm_group
 end ordered_comm_semiring
 
 section ordered_ring
-variables [ordered_ring 𝕜]
+variables [ordered_ring 𝕜] [topological_space E] [topological_space F]
 
 section add_comm_group
-variables [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] {s : set E}
+variables [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] {s : set E} {x y : E}
 
-lemma strict_convex.add_smul_mem (hs : strict_convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : x + y ∈ s)
-  {t : 𝕜} (ht : t ∈ Icc (0 : 𝕜) 1) : x + t • y ∈ s :=
+lemma strict_convex.add_smul_mem (hs : strict_convex 𝕜 s) (hx : x ∈ s) (hxy : x + y ∈ s)
+  (hy : y ≠ 0) {t : 𝕜} (ht₀ : 0 < t) (ht₁ : t < 1) :
+  x + t • y ∈ interior s :=
 begin
   have h : x + t • y = (1 - t) • x + t • (x + y),
   { rw [smul_add, ←add_assoc, ←add_smul, sub_add_cancel, one_smul] },
   rw h,
-  exact hs hx hy (sub_nonneg_of_le ht.2) ht.1 (sub_add_cancel _ _),
+  refine hs _ hx _ hxy (λ h, hy $ add_left_cancel _) (sub_pos_of_lt ht₁) ht₀ (sub_add_cancel _ _),
+  exact x,
+  rw [←h, add_zero],
 end
 
-lemma strict_convex.smul_mem_of_zero_mem (hs : strict_convex 𝕜 s) {x : E} (zero_mem : (0 : E) ∈ s) (hx : x ∈ s)
-  {t : 𝕜} (ht : t ∈ Icc (0 : 𝕜) 1) : t • x ∈ s :=
-by simpa using hs.add_smul_mem zero_mem (by simpa using hx) ht
+lemma strict_convex.smul_mem_of_zero_mem (hs : strict_convex 𝕜 s) (zero_mem : (0 : E) ∈ s)
+  (hx : x ∈ s) (hx₀ : x ≠ 0) {t : 𝕜} (ht₀ : 0 < t) (ht₁ : t < 1) :
+  t • x ∈ interior s :=
+by simpa using hs.add_smul_mem zero_mem (by simpa using hx) hx₀ ht₀ ht₁
 
-lemma strict_convex.add_smul_sub_mem (h : strict_convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s)
-  {t : 𝕜} (ht : t ∈ Icc (0 : 𝕜) 1) : x + t • (y - x) ∈ s :=
+lemma strict_convex.add_smul_sub_mem (h : strict_convex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y)
+  {t : 𝕜} (ht₀ : 0 < t) (ht₁ : t < 1) : x + t • (y - x) ∈ interior s :=
 begin
-  apply h.segment_subset hx hy,
-  rw segment_eq_image',
-  exact mem_image_of_mem _ ht,
-end
-
-/-- Affine subspaces are strict_convex. -/
-lemma affine_subspace.strict_convex (Q : affine_subspace 𝕜 E) : strict_convex 𝕜 (Q : set E) :=
-begin
-  intros x y hx hy a b ha hb hab,
-  rw [eq_sub_of_add_eq hab, ← affine_map.line_map_apply_module],
-  exact affine_map.line_map_mem b hx hy,
-end
-
-/--
-Applying an affine map to an affine combination of two points yields
-an affine combination of the images.
--/
-lemma strict_convex.combo_affine_apply {a b : 𝕜} {x y : E} {f : E →ᵃ[𝕜] F} (h : a + b = 1) :
-  f (a • x + b • y) = a • f x + b • f y :=
-begin
-  simp only [convex.combo_eq_vadd h, ← vsub_eq_sub],
-  exact f.apply_line_map _ _ _,
+  apply h.open_segment_subset hx hy hxy,
+  rw open_segment_eq_image',
+  exact mem_image_of_mem _ ⟨ht₀, ht₁⟩,
 end
 
 /-- The preimage of a strict_convex set under an affine map is strict_convex. -/
-lemma strict_convex.affine_preimage (f : E →ᵃ[𝕜] F) {s : set F} (hs : strict_convex 𝕜 s) :
+lemma strict_convex.affine_preimage {s : set F} (hs : strict_convex 𝕜 s) {f : E →ᵃ[𝕜] F}
+  (hf : continuous f) (hfinj : injective f) :
   strict_convex 𝕜 (f ⁻¹' s) :=
 begin
-  intros x y xs ys a b ha hb hab,
-  rw [mem_preimage, strict_convex.combo_affine_apply hab],
-  exact hs xs ys ha hb hab,
+  intros x hx y hy hxy a b ha hb hab,
+  refine preimage_interior_subset_interior_preimage hf _,
+  rw [mem_preimage, convex.combo_affine_apply hab],
+  exact hs _ hx _ hy (hfinj.ne hxy) ha hb hab,
 end
 
 /-- The image of a strict_convex set under an affine map is strict_convex. -/
-lemma strict_convex.affine_image (f : E →ᵃ[𝕜] F) {s : set E} (hs : strict_convex 𝕜 s) :
+lemma strict_convex.affine_image (hs : strict_convex 𝕜 s) {f : E →ᵃ[𝕜] F} (hf : is_open_map f) :
   strict_convex 𝕜 (f '' s) :=
 begin
-  rintro x y ⟨x', ⟨hx', hx'f⟩⟩ ⟨y', ⟨hy', hy'f⟩⟩ a b ha hb hab,
-  refine ⟨a • x' + b • y', ⟨hs hx' hy' ha hb hab, _⟩⟩,
-  rw [convex.combo_affine_apply hab, hx'f, hy'f]
+  rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ hxy a b ha hb hab,
+  exact hf.image_interior_subset _ ⟨a • x + b • y, ⟨hs _ hx _ hy (ne_of_apply_ne _ hxy) ha hb hab,
+    convex.combo_affine_apply hab⟩⟩,
 end
 
 lemma strict_convex.neg (hs : strict_convex 𝕜 s) : strict_convex 𝕜 ((λ z, -z) '' s) :=
-hs.is_linear_image is_linear_map.is_linear_map_neg
+hs.is_linear_image is_linear_map.is_linear_map_neg begin
+  sorry
+end
 
 lemma strict_convex.neg_preimage (hs : strict_convex 𝕜 s) : strict_convex 𝕜 ((λ z, -z) ⁻¹' s) :=
 hs.is_linear_preimage is_linear_map.is_linear_map_neg
@@ -511,56 +334,43 @@ end add_comm_group
 end ordered_ring
 
 section linear_ordered_field
-variables [linear_ordered_field 𝕜]
+variables [linear_ordered_field 𝕜] [topological_space E]
 
 section add_comm_group
-variables [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] {s : set E}
+variables [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] {s : set E} {x : E}
 
-/-- Alternative definition of set strict_convexity, using division. -/
-lemma strict_convex_iff_div :
-  strict_convex 𝕜 s ↔ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄,
-    0 ≤ a → 0 ≤ b → 0 < a + b → (a/(a+b)) • x + (b/(a+b)) • y ∈ s :=
-⟨λ h x y hx hy a b ha hb hab, begin
-  apply h hx hy,
-  { have ha', from mul_le_mul_of_nonneg_left ha (inv_pos.2 hab).le,
-    rwa [mul_zero, ←div_eq_inv_mul] at ha' },
-  { have hb', from mul_le_mul_of_nonneg_left hb (inv_pos.2 hab).le,
-    rwa [mul_zero, ←div_eq_inv_mul] at hb' },
-  { rw ←add_div,
-    exact div_self hab.ne' }
-end, λ h x y hx hy a b ha hb hab,
+lemma strict_convex.smul [topological_space 𝕜] [has_continuous_smul 𝕜 E] (hs : strict_convex 𝕜 s)
+  (c : 𝕜) :
+  strict_convex 𝕜 (c • s) :=
 begin
-  have h', from h hx hy ha hb,
-  rw [hab, div_one, div_one] at h',
-  exact h' zero_lt_one
-end⟩
-
-lemma strict_convex.mem_smul_of_zero_mem (h : strict_convex 𝕜 s) {x : E} (zero_mem : (0 : E) ∈ s)
-  (hx : x ∈ s) {t : 𝕜} (ht : 1 ≤ t) :
-  x ∈ t • s :=
+  obtain rfl | hc := eq_or_ne c 0,
+  { exact (subsingleton_zero_smul_set _).strict_convex },
+  { exact hs.linear_image (linear_map.lsmul _ _ c) (is_open_map_smul₀ hc) }
+end
+
+lemma strict_convex.affinity [has_continuous_add E] (hs : strict_convex 𝕜 s) (z : E) (c : 𝕜) :
+  strict_convex 𝕜 ((λ x, z + c • x) '' s) :=
 begin
-  rw mem_smul_set_iff_inv_smul_mem₀ (zero_lt_one.trans_le ht).ne',
-  exact h.smul_mem_of_zero_mem zero_mem hx ⟨inv_nonneg.2 (zero_le_one.trans ht), inv_le_one ht⟩,
+  have h := (hs.smul c).add_right z,
+  rwa [←image_smul, image_image] at h,
 end
 
-lemma strict_convex.add_smul (h_conv : strict_convex 𝕜 s) {p q : 𝕜} (hp : 0 ≤ p) (hq : 0 ≤ q) :
-  (p + q) • s = p • s + q • s :=
+/-- Alternative definition of set strict_convexity, using division. -/
+lemma strict_convex_iff_div :
+  strict_convex 𝕜 s ↔ s.pairwise
+    (λ x y, ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s) :=
+⟨λ h x hx y hy hxy a b ha hb, begin
+  apply h _ hx _ hy hxy (div_pos ha $ add_pos ha hb) (div_pos hb $ add_pos ha hb),
+  rw ←add_div,
+  exact div_self (add_pos ha hb).ne',
+end, λ h x hx y hy hxy a b ha hb hab, by convert h _ hx _ hy hxy ha hb; rw [hab, div_one] ⟩
+
+lemma strict_convex.mem_smul_of_zero_mem (hs : strict_convex 𝕜 s) (zero_mem : (0 : E) ∈ s)
+  (hx : x ∈ s) (hx₀ : x ≠ 0) {t : 𝕜} (ht : 1 < t) :
+  x ∈ t • interior s :=
 begin
-  obtain rfl | hs := s.eq_empty_or_nonempty,
-  { simp_rw [smul_set_empty, add_empty] },
-  obtain rfl | hp' := hp.eq_or_lt,
-  { rw [zero_add, zero_smul_set hs, zero_add] },
-  obtain rfl | hq' := hq.eq_or_lt,
-  { rw [add_zero, zero_smul_set hs, add_zero] },
-  ext,
-  split,
-  { rintro ⟨v, hv, rfl⟩,
-    exact ⟨p • v, q • v, smul_mem_smul_set hv, smul_mem_smul_set hv, (add_smul _ _ _).symm⟩ },
-  { rintro ⟨v₁, v₂, ⟨v₁₁, h₁₂, rfl⟩, ⟨v₂₁, h₂₂, rfl⟩, rfl⟩,
-    have hpq := add_pos hp' hq',
-    exact mem_smul_set.2 ⟨_, h_conv h₁₂ h₂₂ (div_pos hp' hpq).le (div_pos hq' hpq).le
-      (by rw [←div_self hpq.ne', add_div] : p / (p + q) + q / (p + q) = 1),
-      by simp only [← mul_smul, smul_add, mul_div_cancel' _ hpq.ne']⟩ }
+  rw mem_smul_set_iff_inv_smul_mem₀ (zero_lt_one.trans ht).ne',
+  exact hs.smul_mem_of_zero_mem zero_mem hx hx₀ (inv_pos.2 $ zero_lt_one.trans ht)  (inv_lt_one ht),
 end
 
 end add_comm_group
@@ -572,12 +382,29 @@ Relates `convex` and `ord_connected`.
 -/
 
 section
+variables [topological_space E]
+
+@[simp] lemma strict_convex_iff_convex [linear_ordered_field 𝕜] [topological_space 𝕜]
+  [order_topology 𝕜] {s : set 𝕜} :
+  strict_convex 𝕜 s ↔ convex 𝕜 s :=
+begin
+  refine ⟨strict_convex.convex, λ hs, strict_convex_iff_open_segment_subset.2 (λ x hx y hy hxy, _)⟩,
+  obtain h | h := hxy.lt_or_lt,
+  { refine (open_segment_subset_Ioo h).trans _,
+    rw ←interior_Icc,
+    exact interior_mono (Icc_subset_segment.trans $ hs.segment_subset hx hy) },
+  { rw open_segment_symm,
+    refine (open_segment_subset_Ioo h).trans _,
+    rw ←interior_Icc,
+    exact interior_mono (Icc_subset_segment.trans $ hs.segment_subset hy hx) }
+end
 
 lemma set.ord_connected.strict_convex_of_chain [ordered_semiring 𝕜] [ordered_add_comm_monoid E]
-  [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} (hs : s.ord_connected) (h : zorn.chain (≤) s) :
+  [topological_space E] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} (hs : s.ord_connected)
+  (h : zorn.chain (≤) s) :
   strict_convex 𝕜 s :=
 begin
-  intros x y hx hy a b ha hb hab,
+  intros x hx y hy hxy a b ha hb hab,
   obtain hxy | hyx := h.total_of_refl hx hy,
   { refine hs.out hx hy (mem_Icc.2 ⟨_, _⟩),
     calc
@@ -602,7 +429,7 @@ lemma set.ord_connected.strict_convex [ordered_semiring 𝕜] [linear_ordered_ad
   strict_convex 𝕜 s :=
 hs.strict_convex_of_chain (zorn.chain_of_trichotomous s)
 
-lemma strict_convex_iff_ord_connected [linear_ordered_field 𝕜] {s : set 𝕜} :
+lemma strict_convex_iff_ord_connected [linear_ordered_field 𝕜] [topological_space 𝕜] {s : set 𝕜} :
   strict_convex 𝕜 s ↔ s.ord_connected :=
 begin
   simp_rw [convex_iff_segment_subset, segment_eq_interval, ord_connected_iff_interval_subset],
@@ -612,49 +439,3 @@ end
 alias strict_convex_iff_ord_connected ↔ strict_convex.ord_connected _
 
 end
-
-/-! #### Convexity of submodules/subspaces -/
-
-section submodule
-open submodule
-
-lemma submodule.strict_convex [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (K : submodule 𝕜 E) :
-  strict_convex 𝕜 (↑K : set E) :=
-by { repeat {intro}, refine add_mem _ (smul_mem _ _ _) (smul_mem _ _ _); assumption }
-
-lemma subspace.strict_convex [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] (K : subspace 𝕜 E) :
-  strict_convex 𝕜 (↑K : set E) :=
-K.strict_convex
-
-end submodule
-
-/-! ### Simplex -/
-
-section simplex
-
-variables (𝕜) (ι : Type*) [ordered_semiring 𝕜] [fintype ι]
-
-/-- The standard simplex in the space of functions `ι → 𝕜` is the set of vectors with non-negative
-coordinates with total sum `1`. This is the free object in the category of strict_convex spaces. -/
-def std_simplex : set (ι → 𝕜) :=
-{f | (∀ x, 0 ≤ f x) ∧ ∑ x, f x = 1}
-
-lemma std_simplex_eq_inter :
-  std_simplex 𝕜 ι = (⋂ x, {f | 0 ≤ f x}) ∩ {f | ∑ x, f x = 1} :=
-by { ext f, simp only [std_simplex, set.mem_inter_eq, set.mem_Inter, set.mem_set_of_eq] }
-
-lemma strict_convex_std_simplex : strict_convex 𝕜 (std_simplex 𝕜 ι) :=
-begin
-  refine λ f g hf hg a b ha hb hab, ⟨λ x, _, _⟩,
-  { apply_rules [add_nonneg, mul_nonneg, hf.1, hg.1] },
-  { erw [finset.sum_add_distrib, ← finset.smul_sum, ← finset.smul_sum, hf.2, hg.2,
-      smul_eq_mul, smul_eq_mul, mul_one, mul_one],
-    exact hab }
-end
-
-variable {ι}
-
-lemma ite_eq_mem_std_simplex (i : ι) : (λ j, ite (i = j) (1:𝕜) 0) ∈ std_simplex 𝕜 ι :=
-⟨λ j, by simp only; split_ifs; norm_num, by rw [finset.sum_ite_eq, if_pos (finset.mem_univ _)]⟩
-
-end simplex
diff --git a/src/topology/algebra/ordered/basic.lean b/src/topology/algebra/ordered/basic.lean
index 7886153ba518b..882d50b01629b 100644
--- a/src/topology/algebra/ordered/basic.lean
+++ b/src/topology/algebra/ordered/basic.lean
@@ -261,6 +261,17 @@ lemma is_open_lt [topological_space β] {f g : β → α} (hf : continuous f) (h
   is_open {b | f b < g b} :=
 by simp [lt_iff_not_ge, -not_le]; exact (is_closed_le hg hf).is_open_compl
 
+lemma subset_interior_le {α β : Type*} [topological_space α] [linear_order α]
+  [order_closed_topology α] [topological_space β] {f g : β → α} (hf : continuous f)
+  (hg : continuous g) :
+  {b | f b < g b} ⊆ interior {b | f b ≤ g b} :=
+begin
+  rw subset_interior_iff_subset_of_open,
+  { rintros p (hp : f p < g p),
+    exact hp.le },
+  { exact is_open_lt hf hg }
+end
+
 variables {a b : α}
 
 lemma is_open_Iio : is_open (Iio a) :=
@@ -489,6 +500,10 @@ variables [topological_space α] [linear_order α] [order_closed_topology α] {f
 section
 variables [topological_space β]
 
+lemma lt_subset_interior_le (hf : continuous f) (hg : continuous g) :
+  {b | f b < g b} ⊆ interior {b | f b ≤ g b} :=
+(subset_interior_iff_subset_of_open $ is_open_lt hf hg).2 $ λ p, le_of_lt
+
 lemma frontier_le_subset_eq (hf : continuous f) (hg : continuous g) :
   frontier {b | f b ≤ g b} ⊆ {b | f b = g b} :=
 begin

From dbf45e52bf7cc4881f78162599aa0c64027e5f10 Mon Sep 17 00:00:00 2001
From: YaelDillies <yael.dillies@gmail.com>
Date: Fri, 3 Dec 2021 10:49:39 +0000
Subject: [PATCH 3/8] yet more

---
 src/analysis/convex/strict.lean | 172 ++++++++++++++++++++++----------
 1 file changed, 117 insertions(+), 55 deletions(-)

diff --git a/src/analysis/convex/strict.lean b/src/analysis/convex/strict.lean
index 60a2308668b13..1c75c31ecfaae 100644
--- a/src/analysis/convex/strict.lean
+++ b/src/analysis/convex/strict.lean
@@ -11,11 +11,90 @@ import topology.algebra.ordered.basic
 # Strictly strict_convex sets
 -/
 
-variables {𝕜 E F β : Type*}
-
 open set
 open_locale pointwise
 
+namespace set
+section image2
+variables {α β γ : Type*} {s s' : set α} {t t' : set β} {f : α → β → γ}
+
+lemma image2_subset_left (ht : t ⊆ t') : image2 f s t ⊆ image2 f s t' :=
+image2_subset (subset.refl _) ht
+
+lemma image2_subset_right (hs : s ⊆ s') : image2 f s t ⊆ image2 f s' t :=
+image2_subset hs (subset.refl _)
+
+end image2
+
+variables {α β γ : Type*} {s s' s₁ s₂ t t' t₁ t₂ : set α} {f : α → β → γ}
+
+@[to_additive]
+lemma mul_subset_mul_left [has_mul α] (h : t₁ ⊆ t₂) : s * t₁ ⊆ s * t₂ := image2_subset_left h
+
+@[to_additive]
+lemma mul_subset_mul_right [has_mul α] (h : s₁ ⊆ s₂) : s₁ * t ⊆ s₂ * t := image2_subset_right h
+
+end set
+
+section has_continuous_add
+variables {α : Type*} [topological_space α] [add_comm_group α] [has_continuous_add α] {s t : set α}
+
+lemma add_interior_subset : s + interior t ⊆ interior (s + t) :=
+begin
+  rw subset_interior_iff_subset_of_open,
+  { rintro x ⟨a, b, ha, hb, rfl⟩,
+    exact set.add_mem_add ha (interior_subset hb) },
+  { rw ←set.Union_add_left_image,
+    exact is_open_bUnion (λ x hx, (homeomorph.add_left x).is_open_map _ is_open_interior) }
+end
+
+lemma interior_add_subset : interior s + t ⊆ interior (s + t) :=
+begin
+  rw subset_interior_iff_subset_of_open,
+  { rintro x ⟨a, b, ha, hb, rfl⟩,
+    exact set.add_mem_add (interior_subset ha) hb },
+  { rw ←set.Union_add_right_image,
+    exact is_open_bUnion (λ x hx, (homeomorph.add_right x).is_open_map _ is_open_interior) }
+end
+
+lemma interior_add_interior_subset {s t : set α} :
+  interior s + interior t ⊆ interior (s + t) :=
+(set.add_subset_add_left interior_subset).trans interior_add_subset
+
+lemma is_open_map_add : is_open_map (λ x : α × α, x.1 + x.2) :=
+begin
+  sorry
+end
+
+lemma is_open_map_sub : is_open_map (λ x : α × α, x.1 - x.2) :=
+begin
+  sorry
+end
+
+end has_continuous_add
+
+section open_segment
+variables {𝕜 E : Type*} [linear_ordered_ring 𝕜] [nontrivial 𝕜] [topological_space 𝕜]
+  [order_topology 𝕜] [densely_ordered 𝕜] [linear_ordered_add_comm_group E] [topological_space E]
+  [order_topology E] [module 𝕜 E] [has_continuous_smul 𝕜 E] {x y : E} {s : set E}
+
+open_locale convex
+
+lemma segment_subset_closure_open_segment : [x -[𝕜] y] ⊆ closure (open_segment 𝕜 x y) :=
+begin
+  rw [segment_eq_image, open_segment_eq_image, ←closure_Ioo (@zero_lt_one 𝕜 _ _)],
+  exact image_closure_subset_closure_image (by continuity),
+end
+
+lemma open_segment_subset_interior (h : [x -[𝕜] y] ⊆ s) : open_segment 𝕜 x y ⊆ interior s :=
+begin
+  sorry
+end
+
+end open_segment
+
+variables {𝕜 E F β : Type*}
+
 /-!
 ### Strict convexity of sets
 
@@ -136,6 +215,11 @@ begin
   exact hs _ hx _ hy (hfinj.ne hxy) ha hb hab,
 end
 
+lemma strict_convex.is_linear_preimage {s : set F} (hs : strict_convex 𝕜 s) {f : E → F}
+  (h : is_linear_map 𝕜 f) (hf : continuous f) (hfinj : injective f) :
+  strict_convex 𝕜 (s.preimage f) :=
+hs.linear_preimage (h.mk' f) hf hfinj
+
 section linear_ordered_cancel_add_comm_monoid
 variables [topological_space β] [linear_ordered_cancel_add_comm_monoid β] [order_topology β]
   [module 𝕜 β] [ordered_smul 𝕜 β]
@@ -230,30 +314,30 @@ begin
     rw singleton_add,
     exact (is_open_map_add_left _).image_interior_subset _
       (mem_image_of_mem _ $ ht _ hw _ hy (ne_of_apply_ne _ h) ha hb hab) },
-  obtain rfl | hvx := eq_or_ne w y,
+  obtain rfl | hwy := eq_or_ne w y,
   { rw convex.combo_self hab,
     suffices : a • v + b • x + w ∈ interior (s + {w}),
     { exact interior_mono (add_subset_add (subset.refl _) (singleton_subset_iff.2 hw)) this },
     rw add_singleton,
     exact (is_open_map_add_right _).image_interior_subset _
       (mem_image_of_mem _ $ hs _ hv _ hx hvx ha hb hab) },
-  sorry
+  exact interior_add_interior_subset (add_mem_add (hs _ hv _ hx hvx ha hb hab) $
+    ht _ hw _ hy hwy ha hb hab),
 end
 
-lemma strict_convex.sub {s : set (E × E)} (hs : strict_convex 𝕜 s) :
+lemma strict_convex.sub [has_continuous_add E] {s : set (E × E)} (hs : strict_convex 𝕜 s) :
   strict_convex 𝕜 ((λ x : E × E, x.1 - x.2) '' s) :=
-hs.is_linear_image is_linear_map.is_linear_map_sub begin
-  sorry
-end
+hs.is_linear_image is_linear_map.is_linear_map_sub is_open_map_sub
 
 end add_comm_group
 end ordered_semiring
 
 section ordered_comm_semiring
-variables [ordered_comm_semiring 𝕜] [topological_space E]
+variables [ordered_comm_semiring 𝕜] [topological_space 𝕜] [topological_space E]
 
 section add_comm_group
-variables [add_comm_group E] [module 𝕜 E] [no_zero_smul_divisors 𝕜 E] {s : set E}
+variables [add_comm_group E] [module 𝕜 E] [no_zero_smul_divisors 𝕜 E] [has_continuous_smul 𝕜 E]
+  {s : set E}
 
 lemma strict_convex.preimage_smul (hs : strict_convex 𝕜 s) (c : 𝕜) :
   strict_convex 𝕜 ((λ z, c • z) ⁻¹' s) :=
@@ -265,7 +349,8 @@ begin
     { exact strict_convex_univ },
     { exact strict_convex_empty } },
   refine hs.linear_preimage (linear_map.lsmul _ _ c) _ (smul_right_injective E hc),
-  sorry
+  unfold linear_map.lsmul linear_map.mk₂ linear_map.mk₂' linear_map.mk₂'ₛₗ,
+  exact continuous_const.smul continuous_id,
 end
 
 end add_comm_group
@@ -322,13 +407,13 @@ begin
     convex.combo_affine_apply hab⟩⟩,
 end
 
-lemma strict_convex.neg (hs : strict_convex 𝕜 s) : strict_convex 𝕜 ((λ z, -z) '' s) :=
-hs.is_linear_image is_linear_map.is_linear_map_neg begin
-  sorry
-end
+lemma strict_convex.neg [topological_add_group E] (hs : strict_convex 𝕜 s) :
+  strict_convex 𝕜 ((λ z, -z) '' s) :=
+hs.is_linear_image is_linear_map.is_linear_map_neg (homeomorph.neg E).is_open_map
 
-lemma strict_convex.neg_preimage (hs : strict_convex 𝕜 s) : strict_convex 𝕜 ((λ z, -z) ⁻¹' s) :=
-hs.is_linear_preimage is_linear_map.is_linear_map_neg
+lemma strict_convex.neg_preimage [topological_add_group E] (hs : strict_convex 𝕜 s) :
+  strict_convex 𝕜 ((λ z, -z) ⁻¹' s) :=
+hs.is_linear_preimage is_linear_map.is_linear_map_neg continuous_id.neg neg_injective
 
 end add_comm_group
 end ordered_ring
@@ -348,10 +433,11 @@ begin
   { exact hs.linear_image (linear_map.lsmul _ _ c) (is_open_map_smul₀ hc) }
 end
 
-lemma strict_convex.affinity [has_continuous_add E] (hs : strict_convex 𝕜 s) (z : E) (c : 𝕜) :
+lemma strict_convex.affinity [topological_space 𝕜] [has_continuous_add E] [has_continuous_smul 𝕜 E]
+  (hs : strict_convex 𝕜 s) (z : E) (c : 𝕜) :
   strict_convex 𝕜 ((λ x, z + c • x) '' s) :=
 begin
-  have h := (hs.smul c).add_right z,
+  have h := (hs.smul c).add_left z,
   rwa [←image_smul, image_image] at h,
 end
 
@@ -378,12 +464,20 @@ end linear_ordered_field
 
 /-!
 #### Convex sets in an ordered space
-Relates `convex` and `ord_connected`.
+Relates `convex` and `set.ord_connected`.
 -/
 
 section
 variables [topological_space E]
 
+lemma set.ord_connected.strict_convex [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E]
+  [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} (hs : s.ord_connected) :
+  strict_convex 𝕜 s :=
+begin
+  rw strict_convex_iff_open_segment_subset,
+  intros x hx y hy hxy,
+end
+
 @[simp] lemma strict_convex_iff_convex [linear_ordered_field 𝕜] [topological_space 𝕜]
   [order_topology 𝕜] {s : set 𝕜} :
   strict_convex 𝕜 s ↔ convex 𝕜 s :=
@@ -399,42 +493,10 @@ begin
     exact interior_mono (Icc_subset_segment.trans $ hs.segment_subset hy hx) }
 end
 
-lemma set.ord_connected.strict_convex_of_chain [ordered_semiring 𝕜] [ordered_add_comm_monoid E]
-  [topological_space E] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} (hs : s.ord_connected)
-  (h : zorn.chain (≤) s) :
-  strict_convex 𝕜 s :=
-begin
-  intros x hx y hy hxy a b ha hb hab,
-  obtain hxy | hyx := h.total_of_refl hx hy,
-  { refine hs.out hx hy (mem_Icc.2 ⟨_, _⟩),
-    calc
-      x   = a • x + b • x : (convex.combo_self hab _).symm
-      ... ≤ a • x + b • y : add_le_add_left (smul_le_smul_of_nonneg hxy hb) _,
-    calc
-      a • x + b • y
-          ≤ a • y + b • y : add_le_add_right (smul_le_smul_of_nonneg hxy ha) _
-      ... = y : strict_convex.combo_self hab _ },
-  { refine hs.out hy hx (mem_Icc.2 ⟨_, _⟩),
-    calc
-      y   = a • y + b • y : (convex.combo_self hab _).symm
-      ... ≤ a • x + b • y : add_le_add_right (smul_le_smul_of_nonneg hyx ha) _,
-    calc
-      a • x + b • y
-          ≤ a • x + b • x : add_le_add_left (smul_le_smul_of_nonneg hyx hb) _
-      ... = x : strict_convex.combo_self hab _ }
-end
-
-lemma set.ord_connected.strict_convex [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [module 𝕜 E]
-  [ordered_smul 𝕜 E] {s : set E} (hs : s.ord_connected) :
-  strict_convex 𝕜 s :=
-hs.strict_convex_of_chain (zorn.chain_of_trichotomous s)
-
-lemma strict_convex_iff_ord_connected [linear_ordered_field 𝕜] [topological_space 𝕜] {s : set 𝕜} :
+lemma strict_convex_iff_ord_connected [linear_ordered_field 𝕜] [topological_space 𝕜]
+  [order_topology 𝕜] {s : set 𝕜} :
   strict_convex 𝕜 s ↔ s.ord_connected :=
-begin
-  simp_rw [convex_iff_segment_subset, segment_eq_interval, ord_connected_iff_interval_subset],
-  exact forall_congr (λ x, forall_swap)
-end
+strict_convex_iff_convex.trans convex_iff_ord_connected
 
 alias strict_convex_iff_ord_connected ↔ strict_convex.ord_connected _
 

From a4738143c719d3075c5944e5651484117de19c54 Mon Sep 17 00:00:00 2001
From: YaelDillies <yael.dillies@gmail.com>
Date: Mon, 6 Dec 2021 21:11:24 +0100
Subject: [PATCH 4/8] remove sorried lemmas

---
 src/analysis/convex/strict.lean | 46 +++++++--------------------------
 1 file changed, 9 insertions(+), 37 deletions(-)

diff --git a/src/analysis/convex/strict.lean b/src/analysis/convex/strict.lean
index 1c75c31ecfaae..cef43eb311eac 100644
--- a/src/analysis/convex/strict.lean
+++ b/src/analysis/convex/strict.lean
@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2019 Alexander Bentkamp. All rights reserved.
+Copyright (c) 2021 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Alexander Bentkamp, Yury Kudriashov, Yaël Dillies
+Authors: Yaël Dillies
 -/
 import analysis.convex.function
 import topology.algebra.module
@@ -61,16 +61,6 @@ lemma interior_add_interior_subset {s t : set α} :
   interior s + interior t ⊆ interior (s + t) :=
 (set.add_subset_add_left interior_subset).trans interior_add_subset
 
-lemma is_open_map_add : is_open_map (λ x : α × α, x.1 + x.2) :=
-begin
-  sorry
-end
-
-lemma is_open_map_sub : is_open_map (λ x : α × α, x.1 - x.2) :=
-begin
-  sorry
-end
-
 end has_continuous_add
 
 section open_segment
@@ -86,11 +76,6 @@ begin
   exact image_closure_subset_closure_image (by continuity),
 end
 
-lemma open_segment_subset_interior (h : [x -[𝕜] y] ⊆ s) : open_segment 𝕜 x y ⊆ interior s :=
-begin
-  sorry
-end
-
 end open_segment
 
 variables {𝕜 E F β : Type*}
@@ -224,7 +209,7 @@ section linear_ordered_cancel_add_comm_monoid
 variables [topological_space β] [linear_ordered_cancel_add_comm_monoid β] [order_topology β]
   [module 𝕜 β] [ordered_smul 𝕜 β]
 
-lemma strict_convex_Iic [no_top_order β] (r : β) : strict_convex 𝕜 (Iic r) :=
+lemma strict_convex_Iic (r : β) : strict_convex 𝕜 (Iic r) :=
 begin
   rintro x (hx : x ≤ r) y (hy : y ≤ r) hxy a b ha hb hab,
   refine (subset_interior_iff_subset_of_open is_open_Iio).2 Iio_subset_Iic_self _,
@@ -236,10 +221,10 @@ begin
   { exact add_lt_add (smul_lt_smul_of_pos hx ha) (smul_lt_smul_of_pos hy hb) }
 end
 
-lemma strict_convex_Ici [no_bot_order β] (r : β) : strict_convex 𝕜 (Ici r) :=
-@strict_convex_Iic 𝕜 (order_dual β) _ _ _ _ _ _ _ r
+lemma strict_convex_Ici (r : β) : strict_convex 𝕜 (Ici r) :=
+@strict_convex_Iic 𝕜 (order_dual β) _ _ _ _ _ _ r
 
-lemma strict_convex_Icc [no_top_order β] [no_bot_order β] (r s : β) : strict_convex 𝕜 (Icc r s) :=
+lemma strict_convex_Icc (r s : β) : strict_convex 𝕜 (Icc r s) :=
 (strict_convex_Ici r).inter $ strict_convex_Iic s
 
 lemma strict_convex_Iio (r : β) : strict_convex 𝕜 (Iio r) :=
@@ -251,14 +236,13 @@ lemma strict_convex_Ioi (r : β) : strict_convex 𝕜 (Ioi r) :=
 lemma strict_convex_Ioo (r s : β) : strict_convex 𝕜 (Ioo r s) :=
 (strict_convex_Ioi r).inter $ strict_convex_Iio s
 
-lemma strict_convex_Ico [no_bot_order β] (r s : β) : strict_convex 𝕜 (Ico r s) :=
+lemma strict_convex_Ico (r s : β) : strict_convex 𝕜 (Ico r s) :=
 (strict_convex_Ici r).inter $ strict_convex_Iio s
 
-lemma strict_convex_Ioc [no_top_order β] (r s : β) : strict_convex 𝕜 (Ioc r s) :=
+lemma strict_convex_Ioc (r s : β) : strict_convex 𝕜 (Ioc r s) :=
 (strict_convex_Ioi r).inter $ strict_convex_Iic s
 
-lemma strict_convex_interval [no_top_order β] [no_bot_order β] (r s : β) :
-  strict_convex 𝕜 (interval r s) :=
+lemma strict_convex_interval (r s : β) : strict_convex 𝕜 (interval r s) :=
 strict_convex_Icc _ _
 
 end linear_ordered_cancel_add_comm_monoid
@@ -325,10 +309,6 @@ begin
     ht _ hw _ hy hwy ha hb hab),
 end
 
-lemma strict_convex.sub [has_continuous_add E] {s : set (E × E)} (hs : strict_convex 𝕜 s) :
-  strict_convex 𝕜 ((λ x : E × E, x.1 - x.2) '' s) :=
-hs.is_linear_image is_linear_map.is_linear_map_sub is_open_map_sub
-
 end add_comm_group
 end ordered_semiring
 
@@ -470,14 +450,6 @@ Relates `convex` and `set.ord_connected`.
 section
 variables [topological_space E]
 
-lemma set.ord_connected.strict_convex [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E]
-  [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} (hs : s.ord_connected) :
-  strict_convex 𝕜 s :=
-begin
-  rw strict_convex_iff_open_segment_subset,
-  intros x hx y hy hxy,
-end
-
 @[simp] lemma strict_convex_iff_convex [linear_ordered_field 𝕜] [topological_space 𝕜]
   [order_topology 𝕜] {s : set 𝕜} :
   strict_convex 𝕜 s ↔ convex 𝕜 s :=

From 5b728d819a34ab7b3e4a2bd991905fdb870a7720 Mon Sep 17 00:00:00 2001
From: YaelDillies <yael.dillies@gmail.com>
Date: Mon, 6 Dec 2021 21:37:08 +0100
Subject: [PATCH 5/8] reduce imports, move lemmas

---
 src/algebra/pointwise.lean      |  6 +++
 src/analysis/convex/strict.lean | 78 ++++++++++++---------------------
 src/data/set/basic.lean         |  6 +++
 3 files changed, 39 insertions(+), 51 deletions(-)

diff --git a/src/algebra/pointwise.lean b/src/algebra/pointwise.lean
index 0aa96cb0b31a6..944b01b51e453 100644
--- a/src/algebra/pointwise.lean
+++ b/src/algebra/pointwise.lean
@@ -216,6 +216,12 @@ end
 lemma mul_subset_mul [has_mul α] (h₁ : s₁ ⊆ t₁) (h₂ : s₂ ⊆ t₂) : s₁ * s₂ ⊆ t₁ * t₂ :=
 image2_subset h₁ h₂
 
+@[to_additive]
+lemma mul_subset_mul_left [has_mul α] (h : t₁ ⊆ t₂) : s * t₁ ⊆ s * t₂ := image2_subset_left h
+
+@[to_additive]
+lemma mul_subset_mul_right [has_mul α] (h : s₁ ⊆ s₂) : s₁ * t ⊆ s₂ * t := image2_subset_right h
+
 lemma pow_subset_pow [monoid α] (hst : s ⊆ t) (n : ℕ) :
   s ^ n ⊆ t ^ n :=
 begin
diff --git a/src/analysis/convex/strict.lean b/src/analysis/convex/strict.lean
index cef43eb311eac..90a81cc1c11fe 100644
--- a/src/analysis/convex/strict.lean
+++ b/src/analysis/convex/strict.lean
@@ -3,80 +3,55 @@ Copyright (c) 2021 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import analysis.convex.function
-import topology.algebra.module
+import analysis.convex.basic
+import topology.algebra.mul_action
 import topology.algebra.ordered.basic
 
 /-!
-# Strictly strict_convex sets
--/
+# Strictly convex sets
 
-open set
-open_locale pointwise
+This file defines strictly convex sets.
 
-namespace set
-section image2
-variables {α β γ : Type*} {s s' : set α} {t t' : set β} {f : α → β → γ}
+A set is strictly convex if the open segment between any two distinct points lies in its interior.
 
-lemma image2_subset_left (ht : t ⊆ t') : image2 f s t ⊆ image2 f s t' :=
-image2_subset (subset.refl _) ht
+## TODO
 
-lemma image2_subset_right (hs : s ⊆ s') : image2 f s t ⊆ image2 f s' t :=
-image2_subset hs (subset.refl _)
+Define strictly convex spaces.
 
-end image2
+Is there a better home for the pointwise topology lemmas?
+-/
 
-variables {α β γ : Type*} {s s' s₁ s₂ t t' t₁ t₂ : set α} {f : α → β → γ}
+open set
+open_locale convex pointwise
 
-@[to_additive]
-lemma mul_subset_mul_left [has_mul α] (h : t₁ ⊆ t₂) : s * t₁ ⊆ s * t₂ := image2_subset_left h
+section has_continuous_mul
+variables {α : Type*} [topological_space α] [comm_group α] [has_continuous_mul α] {s t : set α}
 
 @[to_additive]
-lemma mul_subset_mul_right [has_mul α] (h : s₁ ⊆ s₂) : s₁ * t ⊆ s₂ * t := image2_subset_right h
-
-end set
-
-section has_continuous_add
-variables {α : Type*} [topological_space α] [add_comm_group α] [has_continuous_add α] {s t : set α}
-
-lemma add_interior_subset : s + interior t ⊆ interior (s + t) :=
+lemma mul_interior_subset : s * interior t ⊆ interior (s * t) :=
 begin
   rw subset_interior_iff_subset_of_open,
   { rintro x ⟨a, b, ha, hb, rfl⟩,
-    exact set.add_mem_add ha (interior_subset hb) },
-  { rw ←set.Union_add_left_image,
-    exact is_open_bUnion (λ x hx, (homeomorph.add_left x).is_open_map _ is_open_interior) }
+    exact set.mul_mem_mul ha (interior_subset hb) },
+  { rw ←set.Union_mul_left_image,
+    exact is_open_bUnion (λ x hx, (homeomorph.mul_left x).is_open_map _ is_open_interior) }
 end
 
-lemma interior_add_subset : interior s + t ⊆ interior (s + t) :=
+@[to_additive]
+lemma interior_mul_subset : interior s * t ⊆ interior (s * t) :=
 begin
   rw subset_interior_iff_subset_of_open,
   { rintro x ⟨a, b, ha, hb, rfl⟩,
-    exact set.add_mem_add (interior_subset ha) hb },
-  { rw ←set.Union_add_right_image,
-    exact is_open_bUnion (λ x hx, (homeomorph.add_right x).is_open_map _ is_open_interior) }
+    exact set.mul_mem_mul (interior_subset ha) hb },
+  { rw ←set.Union_mul_right_image,
+    exact is_open_bUnion (λ x hx, (homeomorph.mul_right x).is_open_map _ is_open_interior) }
 end
 
-lemma interior_add_interior_subset {s t : set α} :
-  interior s + interior t ⊆ interior (s + t) :=
-(set.add_subset_add_left interior_subset).trans interior_add_subset
-
-end has_continuous_add
+lemma interior_mul_interior_subset {s t : set α} :
+  interior s * interior t ⊆ interior (s * t) :=
+(set.mul_subset_mul_left interior_subset).trans interior_mul_subset
 
-section open_segment
-variables {𝕜 E : Type*} [linear_ordered_ring 𝕜] [nontrivial 𝕜] [topological_space 𝕜]
-  [order_topology 𝕜] [densely_ordered 𝕜] [linear_ordered_add_comm_group E] [topological_space E]
-  [order_topology E] [module 𝕜 E] [has_continuous_smul 𝕜 E] {x y : E} {s : set E}
-
-open_locale convex
-
-lemma segment_subset_closure_open_segment : [x -[𝕜] y] ⊆ closure (open_segment 𝕜 x y) :=
-begin
-  rw [segment_eq_image, open_segment_eq_image, ←closure_Ioo (@zero_lt_one 𝕜 _ _)],
-  exact image_closure_subset_closure_image (by continuity),
-end
-
-end open_segment
+end has_continuous_mul
 
 variables {𝕜 E F β : Type*}
 
@@ -444,6 +419,7 @@ end linear_ordered_field
 
 /-!
 #### Convex sets in an ordered space
+
 Relates `convex` and `set.ord_connected`.
 -/
 
diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
index f6f518512a3eb..7cf2bb3831b60 100644
--- a/src/data/set/basic.lean
+++ b/src/data/set/basic.lean
@@ -2652,6 +2652,12 @@ lemma mem_image2_iff (hf : injective2 f) : f a b ∈ image2 f s t ↔ a ∈ s 
 lemma image2_subset (hs : s ⊆ s') (ht : t ⊆ t') : image2 f s t ⊆ image2 f s' t' :=
 by { rintro _ ⟨a, b, ha, hb, rfl⟩, exact mem_image2_of_mem (hs ha) (ht hb) }
 
+lemma image2_subset_left (ht : t ⊆ t') : image2 f s t ⊆ image2 f s t' :=
+image2_subset (subset.refl _) ht
+
+lemma image2_subset_right (hs : s ⊆ s') : image2 f s t ⊆ image2 f s' t :=
+image2_subset hs (subset.refl _)
+
 lemma forall_image2_iff {p : γ → Prop} :
   (∀ z ∈ image2 f s t, p z) ↔ ∀ (x ∈ s) (y ∈ t), p (f x y) :=
 ⟨λ h x hx y hy, h _ ⟨x, y, hx, hy, rfl⟩, λ h z ⟨x, y, hx, hy, hz⟩, hz ▸ h x hx y hy⟩

From 4df00ec91bf267560f0be56cb89f462e527c29f6 Mon Sep 17 00:00:00 2001
From: YaelDillies <yael.dillies@gmail.com>
Date: Tue, 7 Dec 2021 14:09:31 +0100
Subject: [PATCH 6/8] move pointwise lemmas

---
 src/analysis/convex/strict.lean         | 40 +-----------
 src/topology/algebra/group.lean         | 83 ++++++++++++++++++-------
 src/topology/algebra/ordered/basic.lean | 11 ----
 3 files changed, 61 insertions(+), 73 deletions(-)

diff --git a/src/analysis/convex/strict.lean b/src/analysis/convex/strict.lean
index 90a81cc1c11fe..eb3f77c164634 100644
--- a/src/analysis/convex/strict.lean
+++ b/src/analysis/convex/strict.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import analysis.convex.basic
-import topology.algebra.mul_action
+import topology.algebra.group
 import topology.algebra.ordered.basic
 
 /-!
@@ -17,51 +17,13 @@ A set is strictly convex if the open segment between any two distinct points lie
 ## TODO
 
 Define strictly convex spaces.
-
-Is there a better home for the pointwise topology lemmas?
 -/
 
 open set
 open_locale convex pointwise
 
-section has_continuous_mul
-variables {α : Type*} [topological_space α] [comm_group α] [has_continuous_mul α] {s t : set α}
-
-@[to_additive]
-lemma mul_interior_subset : s * interior t ⊆ interior (s * t) :=
-begin
-  rw subset_interior_iff_subset_of_open,
-  { rintro x ⟨a, b, ha, hb, rfl⟩,
-    exact set.mul_mem_mul ha (interior_subset hb) },
-  { rw ←set.Union_mul_left_image,
-    exact is_open_bUnion (λ x hx, (homeomorph.mul_left x).is_open_map _ is_open_interior) }
-end
-
-@[to_additive]
-lemma interior_mul_subset : interior s * t ⊆ interior (s * t) :=
-begin
-  rw subset_interior_iff_subset_of_open,
-  { rintro x ⟨a, b, ha, hb, rfl⟩,
-    exact set.mul_mem_mul (interior_subset ha) hb },
-  { rw ←set.Union_mul_right_image,
-    exact is_open_bUnion (λ x hx, (homeomorph.mul_right x).is_open_map _ is_open_interior) }
-end
-
-lemma interior_mul_interior_subset {s t : set α} :
-  interior s * interior t ⊆ interior (s * t) :=
-(set.mul_subset_mul_left interior_subset).trans interior_mul_subset
-
-end has_continuous_mul
-
 variables {𝕜 E F β : Type*}
 
-/-!
-### Strict convexity of sets
-
-This file defines strictly convex sets.
-
--/
-
 open function set
 open_locale convex
 
diff --git a/src/topology/algebra/group.lean b/src/topology/algebra/group.lean
index fe05d9c0f64ce..43a2bca12d7de 100644
--- a/src/topology/algebra/group.lean
+++ b/src/topology/algebra/group.lean
@@ -3,9 +3,8 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot
 -/
-
-import order.filter.pointwise
 import group_theory.quotient_group
+import order.filter.pointwise
 import topology.algebra.monoid
 import topology.homeomorph
 import topology.compacts
@@ -119,6 +118,64 @@ lemma discrete_topology_iff_open_singleton_one : discrete_topology G ↔ is_open
 
 end continuous_mul_group
 
+/-!
+### Topological operations on pointwise sums and products
+
+A few results about interior and closure of the pointwise addition/multiplication of sets in groups
+with continuous addition/multiplication. See also `submonoid.top_closure_mul_self_eq` in
+`topology.algebra.monoid`.
+-/
+
+section pointwise
+section group
+variables [group α] [has_continuous_mul α] {s t : set α}
+
+@[to_additive]
+lemma is_open.mul_left (ht : is_open t) :  is_open (s * t) :=
+begin
+  rw ←Union_mul_left_image,
+  exact is_open_Union (λ a, is_open_Union $ λ ha, is_open_map_mul_left a t ht),
+end
+
+@[to_additive]
+lemma is_open.mul_right (hs : is_open t) : is_open s → is_open (s * t) := λ hs,
+begin
+  rw ←Union_mul_right_image,
+  exact is_open_Union (λ a, is_open_Union $ λ ha, is_open_map_mul_right a s hs),
+end
+
+end group
+
+section comm_group
+variables [comm_group α] [has_continuous_mul α] {s t : set α}
+
+@[to_additive]
+lemma subset_interior_mul_left : interior s * t ⊆ interior (s * t) :=
+interior_maximal (set.mul_subset_mul_right interior_subset) is_open_interior.mul_right
+
+@[to_additive]
+lemma subset_interior_mul_right : s * interior t ⊆ interior (s * t) :=
+interior_maximal (set.mul_subset_mul_left interior_subset) is_open_interior.mul_left
+
+@[to_additive]
+lemma subset_interior_mul : interior s * interior t ⊆ interior (s * t) :=
+(set.mul_subset_mul_left interior_subset).trans interior_mul_subset
+
+@[to_additive]
+lemma subset_closure_mul_left : closure s * t ⊆ closure (s * t) :=
+closure_minimal (set.mul_subset_mul_right subset_closure) is_closed_closure.mul_right
+
+@[to_additive]
+lemma subset_closure_mul_right : s * closure t ⊆ closure (s * t) :=
+closure_minimal (set.mul_subset_mul_left subset_closure) is_closed_closure.mul_left
+
+@[to_additive]
+lemma subset_closure_mul : closure s * closure t ⊆ closure (s * t)  :=
+(set.mul_subset_mul_left subset_closure).trans closure_mul_subset_right
+
+end comm_group
+end pointwise
+
 section topological_group
 
 /-!
@@ -566,27 +623,7 @@ class add_group_with_zero_nhd (G : Type u) extends add_comm_group G :=
 section filter_mul
 
 section
-variables [topological_space G] [group G] [topological_group G]
-
-@[to_additive]
-lemma is_open.mul_left {s t : set G} : is_open t → is_open (s * t) := λ ht,
-begin
-  have : ∀a, is_open ((λ (x : G), a * x) '' t) :=
-    assume a, is_open_map_mul_left a t ht,
-  rw ← Union_mul_left_image,
-  exact is_open_Union (λa, is_open_Union $ λha, this _),
-end
-
-@[to_additive]
-lemma is_open.mul_right {s t : set G} : is_open s → is_open (s * t) := λ hs,
-begin
-  have : ∀a, is_open ((λ (x : G), x * a) '' s),
-    assume a, apply is_open_map_mul_right, exact hs,
-  rw ← Union_mul_right_image,
-  exact is_open_Union (λa, is_open_Union $ λha, this _),
-end
-
-variables (G)
+variables (G) [topological_space G] [group G] [topological_group G]
 
 @[to_additive]
 lemma topological_group.t1_space (h : @is_closed G _ {1}) : t1_space G :=
diff --git a/src/topology/algebra/ordered/basic.lean b/src/topology/algebra/ordered/basic.lean
index fd8628da51e30..db085ad9ba912 100644
--- a/src/topology/algebra/ordered/basic.lean
+++ b/src/topology/algebra/ordered/basic.lean
@@ -261,17 +261,6 @@ lemma is_open_lt [topological_space β] {f g : β → α} (hf : continuous f) (h
   is_open {b | f b < g b} :=
 by simp [lt_iff_not_ge, -not_le]; exact (is_closed_le hg hf).is_open_compl
 
-lemma subset_interior_le {α β : Type*} [topological_space α] [linear_order α]
-  [order_closed_topology α] [topological_space β] {f g : β → α} (hf : continuous f)
-  (hg : continuous g) :
-  {b | f b < g b} ⊆ interior {b | f b ≤ g b} :=
-begin
-  rw subset_interior_iff_subset_of_open,
-  { rintros p (hp : f p < g p),
-    exact hp.le },
-  { exact is_open_lt hf hg }
-end
-
 variables {a b : α}
 
 lemma is_open_Iio : is_open (Iio a) :=

From e8a16cde7befa29afb3b4156a3b5f8a4606eba03 Mon Sep 17 00:00:00 2001
From: YaelDillies <yael.dillies@gmail.com>
Date: Wed, 8 Dec 2021 21:08:09 +0100
Subject: [PATCH 7/8] fix

---
 src/analysis/convex/strict.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/analysis/convex/strict.lean b/src/analysis/convex/strict.lean
index eb3f77c164634..274eacfa78de1 100644
--- a/src/analysis/convex/strict.lean
+++ b/src/analysis/convex/strict.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import analysis.convex.basic
-import topology.algebra.group
+import topology.algebra.mul_action
 import topology.algebra.ordered.basic
 
 /-!
@@ -242,7 +242,7 @@ begin
     rw add_singleton,
     exact (is_open_map_add_right _).image_interior_subset _
       (mem_image_of_mem _ $ hs _ hv _ hx hvx ha hb hab) },
-  exact interior_add_interior_subset (add_mem_add (hs _ hv _ hx hvx ha hb hab) $
+  exact subset_interior_add (add_mem_add (hs _ hv _ hx hvx ha hb hab) $
     ht _ hw _ hy hwy ha hb hab),
 end
 

From f12defbce8cf660e209e3c958d53669c8d367c0d Mon Sep 17 00:00:00 2001
From: YaelDillies <yael.dillies@gmail.com>
Date: Sun, 12 Dec 2021 01:17:16 +0100
Subject: [PATCH 8/8] expand docstring, protect lemmas

---
 src/analysis/convex/strict.lean | 24 ++++++++++++++++++------
 1 file changed, 18 insertions(+), 6 deletions(-)

diff --git a/src/analysis/convex/strict.lean b/src/analysis/convex/strict.lean
index 274eacfa78de1..5a9a072f9116a 100644
--- a/src/analysis/convex/strict.lean
+++ b/src/analysis/convex/strict.lean
@@ -36,9 +36,10 @@ variables [add_comm_monoid E] [add_comm_monoid F]
 section has_scalar
 variables (𝕜) [has_scalar 𝕜 E] [has_scalar 𝕜 F] (s : set E)
 
-/-- Convexity of sets. -/
+/-- A set is strictly convex if the open segment between any two distinct points lies is in its
+interior. This basically means "convex and not flat on the boundary". -/
 def strict_convex : Prop :=
-s.pairwise (λ x y, ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior s)
+s.pairwise $ λ x y, ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior s
 
 variables {𝕜 s} {x y : E}
 
@@ -66,7 +67,7 @@ begin
   exact mem_univ _,
 end
 
-lemma strict_convex.inter {t : set E} (hs : strict_convex 𝕜 s) (ht : strict_convex 𝕜 t) :
+protected lemma strict_convex.inter {t : set E} (hs : strict_convex 𝕜 s) (ht : strict_convex 𝕜 t) :
   strict_convex 𝕜 (s ∩ t) :=
 begin
   intros x hx y hy hxy a b ha hb hab,
@@ -99,11 +100,11 @@ end has_scalar
 section module
 variables [module 𝕜 E] [module 𝕜 F] {s : set E}
 
-lemma strict_convex.convex (hs : strict_convex 𝕜 s) : convex 𝕜 s :=
+protected lemma strict_convex.convex (hs : strict_convex 𝕜 s) : convex 𝕜 s :=
 convex_iff_pairwise_pos.2 $ λ x hx y hy hxy a b ha hb hab,
   interior_subset $ hs x hx y hy hxy ha hb hab
 
-lemma convex.strict_convex (h : is_open s) (hs : convex 𝕜 s) : strict_convex 𝕜 s :=
+protected lemma convex.strict_convex (h : is_open s) (hs : convex 𝕜 s) : strict_convex 𝕜 s :=
 λ x hx y hy _ a b ha hb hab, h.interior_eq.symm ▸ hs hx hy ha.le hb.le hab
 
 lemma is_open.strict_convex_iff (h : is_open s) : strict_convex 𝕜 s ↔ convex 𝕜 s :=
@@ -114,7 +115,7 @@ lemma strict_convex_singleton (c : E) : strict_convex 𝕜 ({c} : set E) := pair
 lemma set.subsingleton.strict_convex (hs : s.subsingleton) : strict_convex 𝕜 s := hs.pairwise _
 
 lemma strict_convex.linear_image (hs : strict_convex 𝕜 s) (f : E →ₗ[𝕜] F) (hf : is_open_map f) :
-  strict_convex 𝕜 (s.image f) :=
+  strict_convex 𝕜 (f '' s) :=
 begin
   rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ hxy a b ha hb hab,
   exact hf.image_interior_subset _
@@ -279,6 +280,17 @@ variables [ordered_ring 𝕜] [topological_space E] [topological_space F]
 section add_comm_group
 variables [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] {s : set E} {x y : E}
 
+lemma strict_convex.eq_of_open_segment_subset_frontier [nontrivial 𝕜] [densely_ordered 𝕜]
+  (hs : strict_convex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s) (h : open_segment 𝕜 x y ⊆ frontier s) :
+  x = y :=
+begin
+  obtain ⟨a, ha₀, ha₁⟩ := densely_ordered.dense (0 : 𝕜) 1 zero_lt_one,
+  classical,
+  by_contra hxy,
+  exact (h ⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel'_right _ _, rfl⟩).2
+    (hs _ hx _ hy hxy ha₀ (sub_pos_of_lt ha₁) $ add_sub_cancel'_right _ _),
+end
+
 lemma strict_convex.add_smul_mem (hs : strict_convex 𝕜 s) (hx : x ∈ s) (hxy : x + y ∈ s)
   (hy : y ≠ 0) {t : 𝕜} (ht₀ : 0 < t) (ht₁ : t < 1) :
   x + t • y ∈ interior s :=