feat(analysis/convex/{basic,function}): add lemmas, golf (#11608)

* add `segment_subset_iff`, `open_segment_subset_iff`, use them to golf some proofs;
* add `mem_segment_iff_div`, `mem_open_segment_iff_div`, use the
  former in the proof of `convex_iff_div`;
* move the proof of `mpr` in `convex_on_iff_convex_epigraph` to a new
  lemma;
* prove that the strict epigraph of a convex function include the open
  segment provided that one of the endpoints is in the strong epigraph
  and the other is in the epigraph; use it in the proof of
  `convex_on.convex_strict_epigraph`.

src/analysis/convex/basic.lean

@@ -73,6 +73,16 @@ lemma open_segment_subset_segment (x y : E) :
   open_segment 𝕜 x y ⊆ [x -[𝕜] y] :=
 λ z ⟨a, b, ha, hb, hab, hz⟩, ⟨a, b, ha.le, hb.le, hab, hz⟩
 
+lemma segment_subset_iff {x y : E} {s : set E} :
+  [x -[𝕜] y] ⊆ s ↔ ∀ a b : 𝕜, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s :=
+⟨λ H a b ha hb hab, H ⟨a, b, ha, hb, hab, rfl⟩,
+  λ H z ⟨a, b, ha, hb, hab, hz⟩, hz ▸ H a b ha hb hab⟩
+
+lemma open_segment_subset_iff {x y : E} {s : set E} :
+  open_segment 𝕜 x y ⊆ s ↔ ∀ a b : 𝕜, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s :=
+⟨λ H a b ha hb hab, H ⟨a, b, ha, hb, hab, rfl⟩,
+  λ H z ⟨a, b, ha, hb, hab, hz⟩, hz ▸ H a b ha hb hab⟩
+
 end has_scalar
 
 open_locale convex
@@ -101,7 +111,7 @@ lemma mem_open_segment_of_ne_left_right {x y z : E} (hx : x ≠ z) (hy : y ≠ z
   z ∈ open_segment 𝕜 x y :=
 begin
   obtain ⟨a, b, ha, hb, hab, hz⟩ := hz,
-    by_cases ha' : a = 0,
+  by_cases ha' : a = 0,
   { rw [ha', zero_add] at hab,
     rw [ha', hab, zero_smul, one_smul, zero_add] at hz,
     exact (hy hz).elim },
@@ -268,6 +278,31 @@ variables [linear_ordered_field 𝕜]
 section add_comm_group
 variables [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F]
 
+lemma mem_segment_iff_div {x y z : E} : x ∈ [y -[𝕜] z] ↔
+  ∃ a b : 𝕜, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x :=
+begin
+  split,
+  { rintro ⟨a, b, ha, hb, hab, rfl⟩,
+    use [a, b, ha, hb],
+    simp * },
+  { rintro ⟨a, b, ha, hb, hab, rfl⟩,
+    refine ⟨a / (a + b), b / (a + b), div_nonneg ha hab.le, div_nonneg hb hab.le, _, rfl⟩,
+    rw [← add_div, div_self hab.ne'] }
+end
+
+lemma mem_open_segment_iff_div {x y z : E} : x ∈ open_segment 𝕜 y z ↔
+  ∃ a b : 𝕜, 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x :=
+begin
+  split,
+  { rintro ⟨a, b, ha, hb, hab, rfl⟩,
+    use [a, b, ha, hb],
+    rw [hab, div_one, div_one] },
+  { rintro ⟨a, b, ha, hb, rfl⟩,
+    have hab : 0 < a + b, from add_pos ha hb,
+    refine ⟨a / (a + b), b / (a + b), div_pos ha hab, div_pos hb hab, _, rfl⟩,
+    rw [← add_div, div_self hab.ne'] }
+end
+
 @[simp] lemma left_mem_open_segment_iff [no_zero_smul_divisors 𝕜 E] {x y : E} :
   x ∈ open_segment 𝕜 x y ↔ x = y :=
 begin
@@ -479,11 +514,7 @@ variables {𝕜 s}
 
 lemma convex_iff_segment_subset :
   convex 𝕜 s ↔ ∀ ⦃x y⦄, x ∈ s → y ∈ s → [x -[𝕜] y] ⊆ s :=
-begin
-  refine forall₄_congr (λ x y hx hy, ⟨_, λ h a b ha hb hab, h ⟨a, b, ha, hb, hab, rfl⟩⟩),
-  rintro h _ ⟨a, b, ha, hb, hab, rfl⟩,
-  exact h ha hb hab,
-end
+forall₄_congr $ λ x y hx hy, (segment_subset_iff _).symm
 
 lemma convex.segment_subset (h : convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
   [x -[𝕜] y] ⊆ s :=
@@ -504,9 +535,10 @@ iff.intro
   (λ h x y hx hy a b ha hb hab,
     (h ha hb hab) (set.add_mem_add ⟨_, hx, rfl⟩ ⟨_, hy, rfl⟩))
 
+alias convex_iff_pointwise_add_subset ↔ convex.set_combo_subset _
+
 lemma convex_empty : convex 𝕜 (∅ : set E) :=
-by simp only [convex_iff_pointwise_add_subset, add_empty, forall_const, empty_subset,
-  implies_true_iff, smul_set_empty]
+λ x y, false.elim
 
 lemma convex_univ : convex 𝕜 (set.univ : set E) := λ _ _ _ _ _ _ _ _ _, trivial
 
@@ -561,46 +593,34 @@ end has_scalar
 section module
 variables [module 𝕜 E] [module 𝕜 F] {s : set E}
 
+lemma convex_iff_open_segment_subset :
+  convex 𝕜 s ↔ ∀ ⦃x y⦄, x ∈ s → y ∈ s → open_segment 𝕜 x y ⊆ s :=
+convex_iff_segment_subset.trans $ forall₄_congr $ λ x y hx hy,
+  (open_segment_subset_iff_segment_subset hx hy).symm
+
 lemma convex_iff_forall_pos :
   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
+convex_iff_open_segment_subset.trans $ forall₄_congr $ λ x y hx hy,
+  open_segment_subset_iff 𝕜
 
 lemma convex_iff_pairwise_pos :
   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, _⟩,
+  refine convex_iff_forall_pos.trans ⟨λ h x hx y hy _, h hx hy, _⟩,
   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 convex.combo_self hab },
-  exact h hx hy hxy ha' hb' hab,
+  { exact h hx hy hxy ha hb hab },
 end
 
-lemma convex_iff_open_segment_subset :
-  convex 𝕜 s ↔ ∀ ⦃x y⦄, x ∈ s → y ∈ s → open_segment 𝕜 x y ⊆ s :=
-convex_iff_segment_subset.trans $ forall₄_congr $ λ x y hx hy,
-  (open_segment_subset_iff_segment_subset hx hy).symm
+protected lemma set.subsingleton.convex {s : set E} (h : s.subsingleton) : convex 𝕜 s :=
+convex_iff_pairwise_pos.mpr (h.pairwise _)
 
 lemma convex_singleton (c : E) : 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
+subsingleton_singleton.convex
 
-lemma convex.linear_image (hs : convex 𝕜 s) (f : E →ₗ[𝕜] F) : convex 𝕜 (s.image f) :=
+lemma convex.linear_image (hs : convex 𝕜 s) (f : E →ₗ[𝕜] F) : convex 𝕜 (f '' s) :=
 begin
   intros x y hx hy a b ha hb hab,
   obtain ⟨x', hx', rfl⟩ := mem_image_iff_bex.1 hx,
@@ -613,15 +633,15 @@ lemma convex.is_linear_image (hs : convex 𝕜 s) {f : E → F} (hf : is_linear_
 hs.linear_image $ hf.mk' f
 
 lemma convex.linear_preimage {s : set F} (hs : convex 𝕜 s) (f : E →ₗ[𝕜] F) :
-  convex 𝕜 (s.preimage f) :=
+  convex 𝕜 (f ⁻¹' s) :=
 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 convex.is_linear_preimage {s : set F} (hs : convex 𝕜 s) {f : E → F} (hf : is_linear_map 𝕜 f) :
-  convex 𝕜 (preimage f s) :=
+  convex 𝕜 (f ⁻¹' s) :=
 hs.linear_preimage $ hf.mk' f
 
 lemma convex.add {t : set E} (hs : convex 𝕜 s) (ht : convex 𝕜 t) : convex 𝕜 (s + t) :=
@@ -946,21 +966,13 @@ variables [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F]
 /-- Alternative definition of set convexity, using division. -/
 lemma convex_iff_div :
   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,
+    0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s :=
 begin
-  have h', from h hx hy ha hb,
-  rw [hab, div_one, div_one] at h',
-  exact h' zero_lt_one
-end⟩
+  simp only [convex_iff_segment_subset, subset_def, mem_segment_iff_div],
+  refine forall₄_congr (λ x y hx hy, ⟨λ H a b ha hb hab, H _ ⟨a, b, ha, hb, hab, rfl⟩, _⟩),
+  rintro H _ ⟨a, b, ha, hb, hab, rfl⟩,
+  exact H ha hb hab
+end
 
 lemma convex.mem_smul_of_zero_mem (h : convex 𝕜 s) {x : E} (zero_mem : (0 : E) ∈ s)
   (hx : x ∈ s) {t : 𝕜} (ht : 1 ≤ t) :
@@ -1004,24 +1016,11 @@ lemma set.ord_connected.convex_of_chain [ordered_semiring 𝕜] [ordered_add_com
   [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} (hs : s.ord_connected) (h : zorn.chain (≤) s) :
   convex 𝕜 s :=
 begin
-  intros x y hx hy a b ha hb hab,
+  refine convex_iff_segment_subset.mpr (λ x y hx hy, _),
   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 : 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 : convex.combo_self hab _ }
+  { exact (segment_subset_Icc hxy).trans (hs.out hx hy) },
+  { rw segment_symm,
+    exact (segment_subset_Icc hyx).trans (hs.out hy hx) }
 end
 
 lemma set.ord_connected.convex [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [module 𝕜 E]

src/analysis/convex/function.lean

@@ -133,6 +133,15 @@ lemma convex_on_const (c : β) (hs : convex 𝕜 s) : convex_on 𝕜 s (λ x:E,
 lemma concave_on_const (c : β) (hs : convex 𝕜 s) : concave_on 𝕜 s (λ x:E, c) :=
 @convex_on_const _ _ (order_dual β) _ _ _ _ _ _ c hs
 
+lemma convex_on_of_convex_epigraph (h : convex 𝕜 {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2}) :
+  convex_on 𝕜 s f :=
+⟨λ x y hx hy a b ha hb hab, (@h (x, f x) (y, f y) ⟨hx, le_rfl⟩ ⟨hy, le_rfl⟩ a b ha hb hab).1,
+  λ x y hx hy a b ha hb hab, (@h (x, f x) (y, f y) ⟨hx, le_rfl⟩ ⟨hy, le_rfl⟩ a b ha hb hab).2⟩
+
+lemma concave_on_of_convex_hypograph (h : convex 𝕜 {p : E × β | p.1 ∈ s ∧ p.2 ≤ f p.1}) :
+  concave_on 𝕜 s f :=
+@convex_on_of_convex_epigraph 𝕜  E (order_dual β) _ _ _ _ _ _ _ h
+
 end module
 
 section ordered_smul
@@ -167,9 +176,7 @@ hf.dual.convex_epigraph
 
 lemma convex_on_iff_convex_epigraph :
   convex_on 𝕜 s f ↔ convex 𝕜 {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2} :=
-⟨convex_on.convex_epigraph, λ h,
-  ⟨λ x y hx hy a b ha hb hab, (@h (x, f x) (y, f y) ⟨hx, le_rfl⟩ ⟨hy, le_rfl⟩ a b ha hb hab).1,
-  λ x y hx hy a b ha hb hab, (@h (x, f x) (y, f y) ⟨hx, le_rfl⟩ ⟨hy, le_rfl⟩ a b ha hb hab).2⟩⟩
+⟨convex_on.convex_epigraph, convex_on_of_convex_epigraph⟩
 
 lemma concave_on_iff_convex_hypograph :
   concave_on 𝕜 s f ↔ convex 𝕜 {p : E × β | p.1 ∈ s ∧ p.2 ≤ f p.1} :=
@@ -258,17 +265,7 @@ lemma linear_map.concave_on (f : E →ₗ[𝕜] β) {s : set E} (hs : convex 
 
 lemma strict_convex_on.convex_on {s : set E} {f : E → β} (hf : strict_convex_on 𝕜 s f) :
   convex_on 𝕜 s f :=
-⟨hf.1, λ x y hx hy a b ha hb hab, begin
-  obtain rfl | hxy := eq_or_ne x y,
-  { rw [convex.combo_self hab, convex.combo_self hab] },
-  obtain rfl | ha' := ha.eq_or_lt,
-  { rw zero_add at hab,
-    rw [hab, zero_smul, zero_smul, one_smul, one_smul, zero_add, zero_add] },
-  obtain rfl | hb' := hb.eq_or_lt,
-  { rw add_zero at hab,
-    rw [hab, zero_smul, zero_smul, one_smul, one_smul, add_zero, add_zero] },
-  exact (hf.2 hx hy hxy ha' hb' hab).le,
-end⟩
+convex_on_iff_pairwise_pos.mpr ⟨hf.1, λ x hx y hy hxy a b ha hb hab, (hf.2 hx hy hxy ha hb hab).le⟩
 
 lemma strict_concave_on.concave_on {s : set E} {f : E → β} (hf : strict_concave_on 𝕜 s f) :
   concave_on 𝕜 s f :=
@@ -399,17 +396,27 @@ convex_iff_forall_pos.2 $ λ x y hx hy a b ha hb hab, ⟨hf.1 hx.1 hy.1 ha.le hb
 lemma concave_on.convex_gt (hf : concave_on 𝕜 s f) (r : β) : convex 𝕜 {x ∈ s | r < f x} :=
 hf.dual.convex_lt r
 
-lemma convex_on.convex_strict_epigraph (hf : convex_on 𝕜 s f) :
-  convex 𝕜 {p : E × β | p.1 ∈ s ∧ f p.1 < p.2} :=
+lemma convex_on.open_segment_subset_strict_epigraph (hf : convex_on 𝕜 s f) (p q : E × β)
+  (hp : p.1 ∈ s ∧ f p.1 < p.2) (hq : q.1 ∈ s ∧ f q.1 ≤ q.2) :
+  open_segment 𝕜 p q ⊆ {p : E × β | p.1 ∈ s ∧ f p.1 < p.2} :=
 begin
-  rw convex_iff_forall_pos,
-  rintro ⟨x, r⟩ ⟨y, t⟩ ⟨hx, hr⟩ ⟨hy, ht⟩ a b ha hb hab,
-  refine ⟨hf.1 hx hy ha.le hb.le hab, _⟩,
-  calc f (a • x + b • y) ≤ a • f x + b • f y : hf.2 hx hy ha.le hb.le hab
-  ... < a • r + b • t : add_lt_add (smul_lt_smul_of_pos hr ha)
-                            (smul_lt_smul_of_pos ht hb)
+  rintro _ ⟨a, b, ha, hb, hab, rfl⟩,
+  refine ⟨hf.1 hp.1 hq.1 ha.le hb.le hab, _⟩,
+  calc f (a • p.1 + b • q.1) ≤ a • f p.1 + b • f q.1 : hf.2 hp.1 hq.1 ha.le hb.le hab
+  ... < a • p.2 + b • q.2 :
+    add_lt_add_of_lt_of_le (smul_lt_smul_of_pos hp.2 ha) (smul_le_smul_of_nonneg hq.2 hb.le)
 end
 
+lemma concave_on.open_segment_subset_strict_hypograph (hf : concave_on 𝕜 s f) (p q : E × β)
+  (hp : p.1 ∈ s ∧ p.2 < f p.1) (hq : q.1 ∈ s ∧ q.2 ≤ f q.1) :
+  open_segment 𝕜 p q ⊆ {p : E × β | p.1 ∈ s ∧ p.2 < f p.1} :=
+hf.dual.open_segment_subset_strict_epigraph p q hp hq
+
+lemma convex_on.convex_strict_epigraph (hf : convex_on 𝕜 s f) :
+  convex 𝕜 {p : E × β | p.1 ∈ s ∧ f p.1 < p.2} :=
+convex_iff_open_segment_subset.mpr $
+  λ p q hp hq, hf.open_segment_subset_strict_epigraph p q hp ⟨hq.1, hq.2.le⟩
+
 lemma concave_on.convex_strict_hypograph (hf : concave_on 𝕜 s f) :
   convex 𝕜 {p : E × β | p.1 ∈ s ∧ p.2 < f p.1} :=
 hf.dual.convex_strict_epigraph

src/analysis/convex/strict.lean

@@ -45,13 +45,7 @@ variables {𝕜 s} {x y : E}
 
 lemma strict_convex_iff_open_segment_subset :
   strict_convex 𝕜 s ↔ s.pairwise (λ x y, open_segment 𝕜 x y ⊆ interior s) :=
-begin
-  split,
-  { rintro h x hx y hy hxy z ⟨a, b, ha, hb, hab, rfl⟩,
-    exact h hx hy hxy ha hb hab },
-  { rintro h x hx y hy hxy a b ha hb hab,
-    exact h hx hy hxy ⟨a, b, ha, hb, hab, rfl⟩ }
-end
+forall₅_congr $ λ x hx y hy hxy, (open_segment_subset_iff 𝕜).symm
 
 lemma strict_convex.open_segment_subset (hs : strict_convex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s)
   (h : x ≠ y) :
@@ -103,6 +97,7 @@ variables [module 𝕜 E] [module 𝕜 F] {s : set E}
 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 hx hy hxy ha hb hab
 
+/-- An open convex set is strictly convex. -/
 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
 
@@ -398,6 +393,7 @@ Relates `convex` and `set.ord_connected`.
 section
 variables [topological_space E]
 
+/-- A set in a linear ordered field is strictly convex if and only if it is convex. -/
 @[simp] lemma strict_convex_iff_convex [linear_ordered_field 𝕜] [topological_space 𝕜]
   [order_topology 𝕜] {s : set 𝕜} :
   strict_convex 𝕜 s ↔ convex 𝕜 s :=