feat(analysis/convex/strict_convex_space): Strictly convex spaces (#1…

…1794)

Define `strictly_convex_space`, a `Prop`-valued mixin to state that a normed space is strictly convex.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/analysis/convex/integral.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 -/
 import analysis.convex.function
-import analysis.convex.strict
+import analysis.convex.strict_convex_space
 import measure_theory.function.ae_eq_of_integral
 import measure_theory.integral.average
 
@@ -21,7 +21,7 @@ In this file we prove several forms of Jensen's inequality for integrals.
 - for strictly convex sets: `strict_convex.ae_eq_const_or_average_mem_interior`;
 
 - for a closed ball in a strictly convex normed space:
-  `strict_convex.ae_eq_const_or_norm_integral_lt_of_norm_le_const`
+  `ae_eq_const_or_norm_integral_lt_of_norm_le_const`;
 
 - for strictly convex functions: `strict_convex_on.ae_eq_const_or_map_average_lt`.
 
@@ -309,12 +309,11 @@ lemma strict_concave_on.ae_eq_const_or_lt_map_average [is_finite_measure μ] {s
 by simpa only [pi.neg_apply, average_neg, neg_lt_neg_iff]
   using hg.neg.ae_eq_const_or_map_average_lt hgc.neg hsc hfs hfi hgi.neg
 
-/-- If the closed ball of radius `C` in a normed space `E` is strictly convex and `f : α → E` is
-a function such that `∥f x∥ ≤ C` a.e., then either either this function is a.e. equal to its
-average value, or the norm of its integral is strictly less than `(μ univ).to_real * C`. -/
-lemma strict_convex.ae_eq_const_or_norm_integral_lt_of_norm_le_const [is_finite_measure μ]
-  {f : α → E} {C : ℝ} (h_convex : strict_convex ℝ (closed_ball (0 : E) C))
-  (h_le : ∀ᵐ x ∂μ, ∥f x∥ ≤ C) :
+/-- If `E` is a strictly normed space and `f : α → E` is a function such that `∥f x∥ ≤ C` a.e., then
+either either this function is a.e. equal to its average value, or the norm of its integral is
+strictly less than `(μ univ).to_real * C`. -/
+lemma ae_eq_const_or_norm_integral_lt_of_norm_le_const [strict_convex_space ℝ E]
+  [is_finite_measure μ] {f : α → E} {C : ℝ} (h_le : ∀ᵐ x ∂μ, ∥f x∥ ≤ C) :
   (f =ᵐ[μ] const α ⨍ x, f x ∂μ) ∨ ∥∫ x, f x ∂μ∥ < (μ univ).to_real * C :=
 begin
   cases le_or_lt C 0 with hC0 hC0,
@@ -332,5 +331,6 @@ begin
     from ennreal.to_real_pos (mt measure_univ_eq_zero.1 hμ) (measure_ne_top _ _),
   simpa only [interior_closed_ball _ hC0.ne', mem_ball_zero_iff, average_def', norm_smul,
     real.norm_eq_abs, abs_inv, abs_of_pos hμ', ← div_eq_inv_mul, div_lt_iff' hμ']
-    using h_convex.ae_eq_const_or_average_mem_interior is_closed_ball h_le hfi,
+    using (strict_convex_closed_ball ℝ (0 : E) C).ae_eq_const_or_average_mem_interior
+      is_closed_ball h_le hfi
 end

src/analysis/convex/strict.lean

@@ -12,10 +12,6 @@ import topology.algebra.order.basic
 This file defines strictly convex sets.
 
 A set is strictly convex if the open segment between any two distinct points lies in its interior.
-
-## TODO
-
-Define strictly convex spaces.
 -/
 
 open set

src/analysis/convex/strict_convex_space.lean

@@ -0,0 +1,163 @@
+/-
+Copyright (c) 2022 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies, Yury Kudryashov
+-/
+import analysis.convex.strict
+import analysis.convex.topology
+import analysis.normed_space.ordered
+import analysis.normed_space.pointwise
+
+/-!
+# Strictly convex spaces
+
+This file defines strictly convex spaces. A normed space is strictly convex if all closed balls are
+strictly convex. This does **not** mean that the norm is strictly convex (in fact, it never is).
+
+## Main definitions
+
+`strict_convex_space`: a typeclass saying that a given normed space over a normed linear ordered
+field (e.g., `ℝ` or `ℚ`) is strictly convex. The definition requires strict convexity of a closed
+ball of positive radius with center at the origin; strict convexity of any other closed ball follows
+from this assumption.
+
+## Main results
+
+In a strictly convex space, we prove
+
+- `strict_convex_closed_ball`: a closed ball is strictly convex.
+- `combo_mem_ball_of_ne`, `open_segment_subset_ball_of_ne`, `norm_combo_lt_of_ne`:
+  a nontrivial convex combination of two points in a closed ball belong to the corresponding open
+  ball;
+- `norm_add_lt_of_not_same_ray`, `same_ray_iff_norm_add`, `dist_add_dist_eq_iff`:
+  the triangle inequality `dist x y + dist y z ≤ dist x z` is a strict inequality unless `y` belongs
+  to the segment `[x -[ℝ] z]`.
+
+We also provide several lemmas that can be used as alternative constructors for `strict_convex ℝ E`:
+
+- `strict_convex_space.of_strict_convex_closed_unit_ball`: if `closed_ball (0 : E) 1` is strictly
+  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.
+
+## Implementation notes
+
+While the definition is formulated for any normed linear ordered field, most of the lemmas are
+formulated only for the case `𝕜 = ℝ`.
+
+## Tags
+
+convex, strictly convex
+-/
+
+open set metric
+open_locale convex pointwise
+
+/-- A *strictly convex space* is a normed space where the closed balls are strictly convex. We only
+require balls of positive radius with center at the origin to be strictly convex in the definition,
+then prove that any closed ball is strictly convex in `strict_convex_closed_ball` below.
+
+See also `strict_convex_space.of_strict_convex_closed_unit_ball`. -/
+class strict_convex_space (𝕜 E : Type*) [normed_linear_ordered_field 𝕜] [normed_group E]
+  [normed_space 𝕜 E] : Prop :=
+(strict_convex_closed_ball : ∀ r : ℝ, 0 < r → strict_convex 𝕜 (closed_ball (0 : E) r))
+
+variables (𝕜 : Type*) {E : Type*} [normed_linear_ordered_field 𝕜]
+  [normed_group E] [normed_space 𝕜 E]
+
+/-- A closed ball in a strictly convex space is strictly convex. -/
+lemma strict_convex_closed_ball [strict_convex_space 𝕜 E] (x : E) (r : ℝ) :
+  strict_convex 𝕜 (closed_ball x r) :=
+begin
+  cases le_or_lt r 0 with hr hr,
+  { exact (subsingleton_closed_ball x hr).strict_convex },
+  rw ← vadd_closed_ball_zero,
+  exact (strict_convex_space.strict_convex_closed_ball r hr).vadd _,
+end
+
+variables [normed_space ℝ E]
+
+/-- A real normed vector space is strictly convex provided that the unit ball is strictly convex. -/
+lemma strict_convex_space.of_strict_convex_closed_unit_ball
+  [linear_map.compatible_smul E E 𝕜 ℝ] (h : strict_convex 𝕜 (closed_ball (0 : E) 1)) :
+  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_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_mem_interior_left hx hy' ha hb.le hab },
+  cases hy, { exact (convex_closed_ball _ _).combo_mem_interior_right 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
+end
+
+variables [strict_convex_space ℝ E] {x y z : E} {a b r : ℝ}
+
+/-- If `x ≠ y` belong to the same closed ball, then a convex combination of `x` and `y` with
+positive coefficients belongs to the corresponding open ball. -/
+lemma combo_mem_ball_of_ne (hx : x ∈ closed_ball z r) (hy : y ∈ closed_ball z r) (hne : x ≠ y)
+  (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) : a • x + b • y ∈ ball z r :=
+begin
+  rcases eq_or_ne r 0 with rfl|hr,
+  { rw [closed_ball_zero, mem_singleton_iff] at hx hy,
+    exact (hne (hx.trans hy.symm)).elim },
+  { simp only [← interior_closed_ball _ hr] at hx hy ⊢,
+    exact strict_convex_closed_ball ℝ z r hx hy hne ha hb hab }
+end
+
+/-- If `x ≠ y` belong to the same closed ball, then the open segment with endpoints `x` and `y` is
+included in the corresponding open ball. -/
+lemma open_segment_subset_ball_of_ne (hx : x ∈ closed_ball z r) (hy : y ∈ closed_ball z r)
+  (hne : x ≠ y) : open_segment ℝ x y ⊆ ball z r :=
+(open_segment_subset_iff _).2 $ λ a b, combo_mem_ball_of_ne hx hy hne
+
+/-- If `x` and `y` are two distinct vectors of norm at most `r`, then a convex combination of `x`
+and `y` with positive coefficients has norm strictly less than `r`. -/
+lemma norm_combo_lt_of_ne (hx : ∥x∥ ≤ r) (hy : ∥y∥ ≤ r) (hne : x ≠ y) (ha : 0 < a) (hb : 0 < b)
+  (hab : a + b = 1) : ∥a • x + b • y∥ < r :=
+begin
+  simp only [← mem_ball_zero_iff, ← mem_closed_ball_zero_iff] at hx hy ⊢,
+  exact combo_mem_ball_of_ne hx hy hne ha hb hab
+end
+
+/-- In a strictly convex space, if `x` and `y` are not in the same ray, then `∥x + y∥ < ∥x∥ +
+∥y∥`. -/
+lemma norm_add_lt_of_not_same_ray (h : ¬same_ray ℝ x y) : ∥x + y∥ < ∥x∥ + ∥y∥ :=
+begin
+  simp only [same_ray_iff_inv_norm_smul_eq, not_or_distrib, ← ne.def] at h,
+  rcases h with ⟨hx, hy, hne⟩,
+  rw ← norm_pos_iff at hx hy,
+  have hxy : 0 < ∥x∥ + ∥y∥ := add_pos hx hy,
+  have := combo_mem_ball_of_ne (inv_norm_smul_mem_closed_unit_ball x)
+    (inv_norm_smul_mem_closed_unit_ball y) hne (div_pos hx hxy) (div_pos hy hxy)
+    (by rw [← add_div, div_self hxy.ne']),
+  rwa [mem_ball_zero_iff, div_eq_inv_mul, div_eq_inv_mul, mul_smul, mul_smul,
+    smul_inv_smul₀ hx.ne', smul_inv_smul₀ hy.ne', ← smul_add, norm_smul,
+    real.norm_of_nonneg (inv_pos.2 hxy).le, ← div_eq_inv_mul, div_lt_one hxy] at this
+end
+
+/-- In a strictly convex space, two vectors `x`, `y` are in the same ray if and only if the triangle
+inequality for `x` and `y` becomes an equality. -/
+lemma same_ray_iff_norm_add : same_ray ℝ x y ↔ ∥x + y∥ = ∥x∥ + ∥y∥ :=
+⟨same_ray.norm_add, λ h, not_not.1 $ λ h', (norm_add_lt_of_not_same_ray h').ne h⟩
+
+/-- In a strictly convex space, the triangle inequality turns into an equality if and only if the
+middle point belongs to the segment joining two other points. -/
+lemma dist_add_dist_eq_iff : dist x y + dist y z = dist x z ↔ y ∈ [x -[ℝ] z] :=
+by simp only [mem_segment_iff_same_ray, same_ray_iff_norm_add, dist_eq_norm',
+  sub_add_sub_cancel', eq_comm]

src/analysis/convex/topology.lean

@@ -5,6 +5,7 @@ Authors: Alexander Bentkamp, Yury Kudriashov
 -/
 import analysis.convex.jensen
 import analysis.normed_space.finite_dimension
+import analysis.normed_space.ray
 import topology.path_connected
 import topology.algebra.affine
 
@@ -29,7 +30,7 @@ We prove the following facts:
 variables {ι : Type*} {E : Type*}
 
 open set
-open_locale pointwise
+open_locale pointwise convex
 
 lemma real.convex_iff_is_preconnected {s : set ℝ} : convex ℝ s ↔ is_preconnected s :=
 convex_iff_ord_connected.trans is_preconnected_iff_ord_connected.symm
@@ -291,4 +292,11 @@ instance normed_space.loc_path_connected : loc_path_connected_space E :=
 loc_path_connected_of_bases (λ x, metric.nhds_basis_ball)
   (λ x r r_pos, (convex_ball x r).is_path_connected $ by simp [r_pos])
 
+lemma dist_add_dist_of_mem_segment {x y z : E} (h : y ∈ [x -[ℝ] z]) :
+  dist x y + dist y z = dist x z :=
+begin
+  simp only [dist_eq_norm, mem_segment_iff_same_ray] at *,
+  simpa only [sub_add_sub_cancel', norm_sub_rev] using h.norm_add.symm
+end
+
 end normed_space

src/analysis/inner_product_space/basic.lean

@@ -1477,8 +1477,7 @@ begin
       rwa [is_R_or_C.abs_div, abs_of_real, _root_.abs_mul, abs_norm_eq_norm, abs_norm_eq_norm,
           div_eq_one_iff_eq hxy0] at h } },
   rw [h₁, abs_inner_div_norm_mul_norm_eq_one_iff x y],
-  have : x ≠ 0 := λ h, (hx0' $ norm_eq_zero.mpr h),
-  simp [this]
+  simp [hx0]
 end
 
 /-- The inner product of two vectors, divided by the product of their

src/analysis/normed_space/basic.lean

@@ -66,6 +66,11 @@ end
 @[simp] lemma abs_norm_eq_norm (z : β) : |∥z∥| = ∥z∥ :=
   (abs_eq (norm_nonneg z)).mpr (or.inl rfl)
 
+lemma inv_norm_smul_mem_closed_unit_ball [normed_space ℝ β] (x : β) :
+  ∥x∥⁻¹ • x ∈ closed_ball (0 : β) 1 :=
+by simp only [mem_closed_ball_zero_iff, norm_smul, norm_inv, norm_norm, ← div_eq_inv_mul,
+  div_self_le_one]
+
 lemma dist_smul [normed_space α β] (s : α) (x y : β) : dist (s • x) (s • y) = ∥s∥ * dist x y :=
 by simp only [dist_eq_norm, (norm_smul _ _).symm, smul_sub]