chore(analysis/convex/strict_convex_space): generalize/add `strict_co…

…nvex_space.of_*` lemmas (#17206)

src/analysis/convex/segment.lean

@@ -110,14 +110,12 @@ begin
   simp only [subset_antisymm_iff, insert_subset, left_mem_segment, right_mem_segment,
     open_segment_subset_segment, true_and],
   rintro z ⟨a, b, ha, hb, hab, rfl⟩,
-  refine hb.eq_or_gt.imp _ (λ hb', ha.eq_or_gt.imp _ _),
+  refine hb.eq_or_gt.imp _ (λ hb', ha.eq_or_gt.imp _ $ λ ha', _),
   { rintro rfl,
-    rw add_zero at hab,
-    rw [hab, one_smul, zero_smul, add_zero] },
+    rw [← add_zero a, hab, one_smul, zero_smul, add_zero] },
   { rintro rfl,
-    rw zero_add at hab,
-    rw [hab, one_smul, zero_smul, zero_add] },
-  { exact λ ha', ⟨a, b, ha', hb', hab, rfl⟩ }
+    rw [← zero_add b, hab, one_smul, zero_smul, zero_add] },
+  { exact ⟨a, b, ha', hb', hab, rfl⟩ }
 end
 
 variables {𝕜}
@@ -306,6 +304,32 @@ begin
   rw [←sub_eq_neg_add, ←neg_sub, hxy, ←sub_eq_neg_add, hzx, smul_neg, smul_comm, neg_add_self]
 end
 
+open affine_map
+
+/-- If `z = line_map x y c` is a point on the line passing through `x` and `y`, then the open
+segment `open_segment 𝕜 x y` is included in the union of the open segments `open_segment 𝕜 x z`,
+`open_segment 𝕜 z y`, and the point `z`. Informally, `(x, y) ⊆ {z} ∪ (x, z) ∪ (z, y)`. -/
+lemma open_segment_subset_union (x y : E) {z : E} (hz : z ∈ range (line_map x y : 𝕜 → E)) :
+  open_segment 𝕜 x y ⊆ insert z (open_segment 𝕜 x z ∪ open_segment 𝕜 z y) :=
+begin
+  rcases hz with ⟨c, rfl⟩,
+  simp only [open_segment_eq_image_line_map, ← maps_to'],
+  rintro a ⟨h₀, h₁⟩,
+  rcases lt_trichotomy a c with hac|rfl|hca,
+  { right, left,
+    have hc : 0 < c, from h₀.trans hac,
+    refine ⟨a / c, ⟨div_pos h₀ hc, (div_lt_one hc).2 hac⟩, _⟩,
+    simp only [← homothety_eq_line_map, ← homothety_mul_apply, div_mul_cancel _ hc.ne'] },
+  { left, refl },
+  { right, right,
+    have hc : 0 < 1 - c, from sub_pos.2 (hca.trans h₁),
+    simp only [← line_map_apply_one_sub y],
+    refine ⟨(a - c) / (1 - c), ⟨div_pos (sub_pos.2 hca) hc,
+      (div_lt_one hc).2 $ sub_lt_sub_right h₁ _⟩, _⟩,
+    simp only [← homothety_eq_line_map, ← homothety_mul_apply, sub_mul, one_mul,
+      div_mul_cancel _ hc.ne', sub_sub_sub_cancel_right] }
+end
+
 end linear_ordered_field
 
 /-!

src/analysis/convex/strict_convex_space.lean

@@ -42,7 +42,7 @@ We also provide several lemmas that can be used as alternative constructors for
   convex, then `E` is a strictly convex space;
 
 - `strict_convex_space.of_norm_add`: if `∥x + y∥ = ∥x∥ + ∥y∥` implies `same_ray ℝ x y` for all
-  `x y : E`, then `E` is a strictly convex space.
+  nonzero `x y : E`, then `E` is a strictly convex space.
 
 ## Implementation notes
 
@@ -87,74 +87,63 @@ lemma strict_convex_space.of_strict_convex_closed_unit_ball
   strict_convex_space 𝕜 E :=
 ⟨λ r hr, by simpa only [smul_closed_unit_ball_of_nonneg hr.le] using h.smul r⟩
 
-/-- If `∥x + y∥ = ∥x∥ + ∥y∥` implies that `x y : E` are in the same ray, then `E` is a strictly
-convex space. -/
-lemma strict_convex_space.of_norm_add (h : ∀ x y : E, ∥x + y∥ = ∥x∥ + ∥y∥ → same_ray ℝ x y) :
+/-- Strict convexity is equivalent to `∥a • x + b • y∥ < 1` for all `x` and `y` of norm at most `1`
+and all strictly positive `a` and `b` such that `a + b = 1`. This lemma shows that it suffices to
+check this for points of norm one and some `a`, `b` such that `a + b = 1`. -/
+lemma strict_convex_space.of_norm_combo_lt_one
+  (h : ∀ x y : E, ∥x∥ = 1 → ∥y∥ = 1 → x ≠ y → ∃ a b : ℝ, a + b = 1 ∧ ∥a • x + b • y∥ < 1) :
   strict_convex_space ℝ E :=
 begin
-  refine strict_convex_space.of_strict_convex_closed_unit_ball ℝ (λ x hx y hy hne a b ha hb hab, _),
-  have hx' := hx, have hy' := hy,
-  rw [← closure_closed_ball, closure_eq_interior_union_frontier,
-    frontier_closed_ball (0 : E) one_ne_zero] at hx hy,
-  cases hx, { exact (convex_closed_ball _ _).combo_interior_self_mem_interior hx hy' ha hb.le hab },
-  cases hy, { exact (convex_closed_ball _ _).combo_self_interior_mem_interior hx' hy ha.le hb hab },
-  rw [interior_closed_ball (0 : E) one_ne_zero, mem_ball_zero_iff],
-  have hx₁ : ∥x∥ = 1, from mem_sphere_zero_iff_norm.1 hx,
-  have hy₁ : ∥y∥ = 1, from mem_sphere_zero_iff_norm.1 hy,
-  have ha' : ∥a∥ = a, from real.norm_of_nonneg ha.le,
-  have hb' : ∥b∥ = b, from real.norm_of_nonneg hb.le,
-  calc ∥a • x + b • y∥ < ∥a • x∥ + ∥b • y∥ : (norm_add_le _ _).lt_of_ne (λ H, hne _)
-  ... = 1 : by simpa only [norm_smul, hx₁, hy₁, mul_one, ha', hb'],
-  simpa only [norm_smul, hx₁, hy₁, ha', hb', mul_one, smul_comm a, smul_right_inj ha.ne',
-    smul_right_inj hb.ne'] using (h _ _ H).norm_smul_eq.symm
+  refine strict_convex_space.of_strict_convex_closed_unit_ball ℝ
+    ((convex_closed_ball _ _).strict_convex' $ λ x hx y hy hne, _),
+  rw [interior_closed_ball (0 : E) one_ne_zero, closed_ball_diff_ball, mem_sphere_zero_iff_norm]
+    at hx hy,
+  rcases h x y hx hy hne with ⟨a, b, hab, hlt⟩,
+  use b,
+  rwa [affine_map.line_map_apply_module, interior_closed_ball (0 : E) one_ne_zero,
+    mem_ball_zero_iff, sub_eq_iff_eq_add.2 hab.symm]
 end
 
-lemma strict_convex_space.of_norm_add_lt_aux {a b c d : ℝ} (ha : 0 < a) (hab : a + b = 1)
-  (hc : 0 < c) (hd : 0 < d) (hcd : c + d = 1) (hca : c ≤ a) {x y : E} (hy : ∥y∥ ≤ 1)
-  (hxy : ∥a • x + b • y∥ < 1) :
-  ∥c • x + d • y∥ < 1 :=
+lemma strict_convex_space.of_norm_combo_ne_one
+  (h : ∀ x y : E, ∥x∥ = 1 → ∥y∥ = 1 → x ≠ y →
+    ∃ a b : ℝ, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ ∥a • x + b • y∥ ≠ 1) :
+  strict_convex_space ℝ E :=
 begin
-  have hbd : b ≤ d,
-  { refine le_of_add_le_add_left (hab.trans_le _),
-    rw ←hcd,
-    exact add_le_add_right hca _ },
-  have h₁ : 0 < c / a := div_pos hc ha,
-  have h₂ : 0 ≤ d - c / a * b,
-  { rw [sub_nonneg, mul_comm_div, ←le_div_iff' hc],
-    exact div_le_div hd.le hbd hc hca },
-  calc ∥c • x + d • y∥ = ∥(c / a) • (a • x + b • y) + (d - c / a * b) • y∥
-        : by rw [smul_add, ←mul_smul, ←mul_smul, div_mul_cancel _ ha.ne', sub_smul,
-            add_add_sub_cancel]
-    ... ≤ ∥(c / a) • (a • x + b • y)∥ + ∥(d - c / a * b) • y∥ : norm_add_le _ _
-    ... = c / a * ∥a • x + b • y∥ + (d - c / a * b) * ∥y∥
-        : by rw [norm_smul_of_nonneg h₁.le, norm_smul_of_nonneg h₂]
-    ... < c / a * 1 + (d - c / a * b) * 1
-        : add_lt_add_of_lt_of_le (mul_lt_mul_of_pos_left hxy h₁) (mul_le_mul_of_nonneg_left hy h₂)
-    ... = 1 : begin
-      nth_rewrite 0 ←hab,
-      rw [mul_add, div_mul_cancel _ ha.ne', mul_one, add_add_sub_cancel, hcd],
-    end,
+  refine strict_convex_space.of_strict_convex_closed_unit_ball ℝ
+    ((convex_closed_ball _ _).strict_convex _),
+  simp only [interior_closed_ball _ one_ne_zero, closed_ball_diff_ball, set.pairwise,
+    frontier_closed_ball _ one_ne_zero, mem_sphere_zero_iff_norm],
+  intros x hx y hy hne,
+  rcases h x y hx hy hne with ⟨a, b, ha, hb, hab, hne'⟩,
+  exact ⟨_, ⟨a, b, ha, hb, hab, rfl⟩, mt mem_sphere_zero_iff_norm.1 hne'⟩
 end
 
-/-- Strict convexity is equivalent to `∥a • x + b • y∥ < 1` for all `x` and `y` of norm at most `1`
-and all strictly positive `a` and `b` such that `a + b = 1`. This shows that we only need to check
-it for fixed `a` and `b`. -/
-lemma strict_convex_space.of_norm_add_lt {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1)
-  (h : ∀ x y : E, ∥x∥ ≤ 1 → ∥y∥ ≤ 1 → x ≠ y → ∥a • x + b • y∥ < 1) :
+lemma strict_convex_space.of_norm_add_ne_two
+  (h : ∀ ⦃x y : E⦄, ∥x∥ = 1 → ∥y∥ = 1 → x ≠ y → ∥x + y∥ ≠ 2) :
+  strict_convex_space ℝ E :=
+begin
+  refine strict_convex_space.of_norm_combo_ne_one
+    (λ x y hx hy hne, ⟨1/2, 1/2, one_half_pos.le, one_half_pos.le, add_halves _, _⟩),
+  rw [← smul_add, norm_smul, real.norm_of_nonneg one_half_pos.le, one_div,
+    ← div_eq_inv_mul, ne.def, div_eq_one_iff_eq (@two_ne_zero ℝ _ _)],
+  exact h hx hy hne,
+end
+
+lemma strict_convex_space.of_pairwise_sphere_norm_ne_two
+  (h : (sphere (0 : E) 1).pairwise $ λ x y, ∥x + y∥ ≠ 2) :
+  strict_convex_space ℝ E :=
+strict_convex_space.of_norm_add_ne_two $ λ x y hx hy,
+  h (mem_sphere_zero_iff_norm.2 hx) (mem_sphere_zero_iff_norm.2 hy)
+
+/-- If `∥x + y∥ = ∥x∥ + ∥y∥` implies that `x y : E` are in the same ray, then `E` is a strictly
+convex space. See also a more -/
+lemma strict_convex_space.of_norm_add
+  (h : ∀ x y : E, ∥x∥ = 1 → ∥y∥ = 1 → ∥x + y∥ = 2 → same_ray ℝ x y) :
   strict_convex_space ℝ E :=
 begin
-  refine strict_convex_space.of_strict_convex_closed_unit_ball _ (λ x hx y hy hxy c d hc hd hcd, _),
-  rw [interior_closed_ball (0 : E) one_ne_zero, mem_ball_zero_iff],
-  rw mem_closed_ball_zero_iff at hx hy,
-  obtain hca | hac := le_total c a,
-  { exact strict_convex_space.of_norm_add_lt_aux ha hab hc hd hcd hca hy (h _ _ hx hy hxy) },
-  rw add_comm at ⊢ hab hcd,
-  refine strict_convex_space.of_norm_add_lt_aux hb hab hd hc hcd _ hx _,
-  { refine le_of_add_le_add_right (hcd.trans_le _),
-    rw ←hab,
-    exact add_le_add_left hac _ },
-  { rw add_comm,
-    exact h _ _ hx hy hxy }
+  refine strict_convex_space.of_pairwise_sphere_norm_ne_two (λ x hx y hy, mt $ λ h₂, _),
+  rw mem_sphere_zero_iff_norm at hx hy,
+  exact (same_ray_iff_of_norm_eq (hx.trans hy.symm)).1 (h x y hx hy h₂)
 end
 
 variables [strict_convex_space ℝ E] {x y z : E} {a b r : ℝ}

src/analysis/convex/topology.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alexander Bentkamp, Yury Kudryashov
 -/
 import analysis.convex.jensen
+import analysis.convex.strict
 import analysis.normed.group.pointwise
 import topology.algebra.module.finite_dimension
 import analysis.normed_space.ray
@@ -204,6 +205,39 @@ have hf : continuous (function.uncurry f),
 show f x y ∈ closure s,
   from map_mem_closure₂ hf hx hy (λ x' hx' y' hy', hs hx' hy' ha hb hab)
 
+open affine_map
+
+/-- A convex set `s` is strictly convex provided that for any two distinct points of
+`s \ interior s`, the line passing through these points has nonempty intersection with
+`interior s`. -/
+protected lemma convex.strict_convex' {s : set E} (hs : convex 𝕜 s)
+  (h : (s \ interior s).pairwise $ λ x y, ∃ c : 𝕜, line_map x y c ∈ interior s) :
+  strict_convex 𝕜 s :=
+begin
+  refine strict_convex_iff_open_segment_subset.2 _,
+  intros x hx y hy hne,
+  by_cases hx' : x ∈ interior s, { exact hs.open_segment_interior_self_subset_interior hx' hy },
+  by_cases hy' : y ∈ interior s, { exact hs.open_segment_self_interior_subset_interior hx hy' },
+  rcases h ⟨hx, hx'⟩ ⟨hy, hy'⟩ hne with ⟨c, hc⟩,
+  refine (open_segment_subset_union x y ⟨c, rfl⟩).trans (insert_subset.2 ⟨hc, union_subset _ _⟩),
+  exacts [hs.open_segment_self_interior_subset_interior hx hc,
+    hs.open_segment_interior_self_subset_interior hc hy]
+end
+
+/-- A convex set `s` is strictly convex provided that for any two distinct points `x`, `y` of
+`s \ interior s`, the segment with endpoints `x`, `y` has nonempty intersection with
+`interior s`. -/
+protected lemma convex.strict_convex {s : set E} (hs : convex 𝕜 s)
+  (h : (s \ interior s).pairwise $ λ x y, ([x -[𝕜] y] \ frontier s).nonempty) :
+  strict_convex 𝕜 s :=
+begin
+  refine (hs.strict_convex' $ h.imp_on $ λ x hx y hy hne, _),
+  simp only [segment_eq_image_line_map, ← self_diff_frontier],
+  rintro ⟨_, ⟨⟨c, hc, rfl⟩, hcs⟩⟩,
+  refine ⟨c, hs.segment_subset hx.1 hy.1 _, hcs⟩,
+  exact (segment_eq_image_line_map 𝕜 x y).symm ▸ mem_image_of_mem _ hc
+end
+
 end has_continuous_const_smul
 
 section has_continuous_smul

src/analysis/convex/uniform.lean

@@ -122,8 +122,6 @@ variables [normed_add_comm_group E] [normed_space ℝ E] [uniform_convex_space E
 
 @[priority 100] -- See note [lower instance priority]
 instance uniform_convex_space.to_strict_convex_space : strict_convex_space ℝ E :=
-strict_convex_space.of_norm_add_lt one_half_pos one_half_pos (add_halves _) $ λ x y hx hy hxy, begin
-  obtain ⟨δ, hδ, h⟩ := exists_forall_closed_ball_dist_add_le_two_sub E (norm_sub_pos_iff.2 hxy),
-  rw [←smul_add, norm_smul_of_nonneg one_half_pos.le, ←lt_div_iff' one_half_pos, one_div_one_div],
-  exact (h hx hy le_rfl).trans_lt (sub_lt_self _ hδ),
-end
+strict_convex_space.of_norm_add_ne_two $ λ x y hx hy hxy,
+  let ⟨δ, hδ, h⟩ := exists_forall_closed_ball_dist_add_le_two_sub E (norm_sub_pos_iff.2 hxy)
+  in ((h hx.le hy.le le_rfl).trans_lt $ sub_lt_self _ hδ).ne