[Merged by Bors] - feat(analysis/convex/uniform): Uniformly convex spaces

src/analysis/convex/uniform.lean

@@ -0,0 +1,143 @@
+/-
+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
+-/
+import analysis.convex.strict_convex_space
+
+/-!
+# Uniformly convex spaces
+
+This file defines uniformly convex spaces, which are real normed vector spaces in which for all
+strictly positive `ε`, there exists some strictly positive `δ` such that `ε ≤ ∥x - y∥` implies
+`∥x + y∥ ≤ 2 - δ` for all `x` and `y` of norm at most than `1`. This means that the triangle
+inequality is strict with a uniform bound, as opposed to strictly convex spaces where the triangle
+inequality is strict but not necessarily uniformly (`∥x + y∥ < ∥x∥ + ∥y∥` for all `x` and `y` not in
+the same ray).
+
+## Main declarations
+
+`uniform_convex_space E` means that `E` is a uniformly convex space.
+
+## TODO
+
+* Milman-Pettis
+* Hanner's inequalities
+
+## Tags
+
+convex, uniformly convex
+-/
+
+open set metric
+open_locale convex pointwise
+
+/-- A *uniformly convex space* is a real normed space where .
+
+See also `uniform_convex_space.of_uniform_convex_closed_unit_ball`. -/
+class uniform_convex_space (E : Type*) [semi_normed_group E] : Prop :=
+(uniform_convex : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ δ, 0 < δ ∧
+  ∀ ⦃x : E⦄, ∥x∥ = 1 → ∀ ⦃y⦄, ∥y∥ = 1 → ε ≤ ∥x - y∥ → ∥x + y∥ ≤ 2 - δ)
+
+variables {E : Type*}
+
+section semi_normed_group
+variables (E) [semi_normed_group E] [uniform_convex_space E] {ε : ℝ}
+
+lemma exists_forall_sphere_dist_add_le_two_sub (hε : 0 < ε) :
+  ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ∥x∥ = 1 → ∀ ⦃y⦄, ∥y∥ = 1 → ε ≤ ∥x - y∥ → ∥x + y∥ ≤ 2 - δ :=
+uniform_convex_space.uniform_convex hε
+
+variables [normed_space ℝ E]
+
+lemma exists_forall_sphere_dist_add_le_two_mul_sub (hε : 0 < ε) (r : ℝ) :
+  ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ∥x∥ = r → ∀ ⦃y⦄, ∥y∥ = r → ε ≤ ∥x - y∥ → ∥x + y∥ ≤ 2 * r - δ :=
+begin
+  obtain hr | hr := le_or_lt r 0,
+  { exact ⟨1, one_pos, λ x hx y hy h, (hε.not_le $ h.trans $ (norm_sub_le _ _).trans $
+     add_nonpos (hx.trans_le hr) (hy.trans_le hr)).elim⟩ },
+  obtain ⟨δ, hδ, h⟩ := exists_forall_sphere_dist_add_le_two_sub E (div_pos hε hr),
+  refine ⟨δ * r, mul_pos hδ hr, λ x hx y hy hxy, _⟩,
+  rw [eq_comm, ←inv_mul_eq_one₀ hr.ne', ←norm_smul_of_nonneg (inv_nonneg.2 hr.le)] at hx hy;
+    try { apply_instance },
+  have := h hx hy,
+  simp_rw [←smul_add, ←smul_sub, norm_smul_of_nonneg (inv_nonneg.2 hr.le), ←div_eq_inv_mul,
+    div_le_div_right hr, div_le_iff hr, sub_mul] at this,
+  exact this hxy,
+end
+
+lemma exists_forall_ball_dist_add_le_two_sub (hε : 0 < ε) :
+  ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ∥x∥ ≤ 1 → ∀ ⦃y⦄, ∥y∥ ≤ 1 → ε ≤ ∥x - y∥ → ∥x + y∥ ≤ 2 - δ :=
+begin
+  have hε' : 0 < ε / 3 := div_pos hε zero_lt_three,
+  obtain ⟨δ, hδ, h⟩ := exists_forall_sphere_dist_add_le_two_sub E hε',
+  set δ' := min (1/2) (min (ε/3) $ δ/3),
+  refine ⟨δ', lt_min one_half_pos $ lt_min hε' (div_pos hδ zero_lt_three), λ x hx y hy hxy, _⟩,
+  obtain hx' | hx' := le_or_lt (∥x∥) (1 - δ'),
+  { exact (norm_add_le_of_le hx' hy).trans (sub_add_eq_add_sub _ _ _).le },
+  obtain hy' | hy' := le_or_lt (∥y∥) (1 - δ'),
+  { exact (norm_add_le_of_le hx hy').trans (add_sub_assoc _ _ _).ge },
+  have hδ' : 0 < 1 - δ' := sub_pos_of_lt  (min_lt_of_left_lt one_half_lt_one),
+  have h₁ : ∀ z : E, 1 - δ' < ∥z∥ → ∥∥z∥⁻¹ • z∥ = 1,
+  { rintro z hz,
+    rw [norm_smul_of_nonneg (inv_nonneg.2 $ norm_nonneg _), inv_mul_cancel (hδ'.trans hz).ne'] },
+  have h₂ : ∀ z : E, ∥z∥ ≤ 1 → 1 - δ' ≤ ∥z∥ → ∥∥z∥⁻¹ • z - z∥ ≤ δ',
+  { rintro z hz hδz,
+    nth_rewrite 2 ←one_smul ℝ z,
+    rwa [←sub_smul, norm_smul_of_nonneg (sub_nonneg_of_le $ one_le_inv (hδ'.trans_le hδz) hz),
+      sub_mul, inv_mul_cancel (hδ'.trans_le hδz).ne', one_mul, sub_le] },
+  set x' := ∥x∥⁻¹ • x,
+  set y' := ∥y∥⁻¹ • y,
+  have hxy' : ε/3 ≤ ∥x' - y'∥ :=
+  calc ε/3 = ε - (ε/3 + ε/3) : by ring
+    ... ≤ ∥x - y∥ - (∥x' - x∥ + ∥y' - y∥) : sub_le_sub hxy (add_le_add
+          ((h₂ _ hx hx'.le).trans $ min_le_of_right_le $ min_le_left _ _) $
+          (h₂ _ hy hy'.le).trans $ min_le_of_right_le $ min_le_left _ _)
+    ... ≤ _ : begin
+        have : ∀ x' y', x - y = x' - y' + (x - x') + (y' - y) := λ _ _, by abel,
+        rw [sub_le_iff_le_add, norm_sub_rev _ x, ←add_assoc, this],
+        exact norm_add₃_le _ _ _,
+      end,
+  calc ∥x + y∥ ≤ ∥x' + y'∥ + ∥x' - x∥ + ∥y' - y∥ : begin
+        have : ∀ x' y', x + y = x' + y' + (x - x') + (y - y') := λ _ _, by abel,
+        rw [norm_sub_rev, norm_sub_rev y', this],
+        exact norm_add₃_le _ _ _,
+      end
+    ... ≤ 2 - δ + δ' + δ'
+        : add_le_add_three (h (h₁ _ hx') (h₁ _ hy') hxy') (h₂ _ hx hx'.le) (h₂ _ hy hy'.le)
+    ... ≤ 2 - δ' : begin
+        rw [←le_sub_iff_add_le, ←le_sub_iff_add_le, sub_sub, sub_sub],
+        refine sub_le_sub_left _ _,
+        ring_nf,
+        rw ←mul_div_cancel' δ three_ne_zero,
+        exact mul_le_mul_of_nonneg_left (min_le_of_right_le $ min_le_right _ _) three_pos.le,
+      end,
+end
+
+lemma exists_forall_ball_dist_add_le_two_mul_sub (hε : 0 < ε) (r : ℝ) :
+  ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ∥x∥ ≤ r → ∀ ⦃y⦄, ∥y∥ ≤ r → ε ≤ ∥x - y∥ → ∥x + y∥ ≤ 2 * r - δ :=
+begin
+  obtain hr | hr := le_or_lt r 0,
+  { exact ⟨1, one_pos, λ x hx y hy h, (hε.not_le $ h.trans $ (norm_sub_le _ _).trans $
+     add_nonpos (hx.trans hr) (hy.trans hr)).elim⟩ },
+  obtain ⟨δ, hδ, h⟩ := exists_forall_ball_dist_add_le_two_sub E (div_pos hε hr),
+  refine ⟨δ * r, mul_pos hδ hr, λ x hx y hy hxy, _⟩,
+  rw [←div_le_one hr, div_eq_inv_mul, ←norm_smul_of_nonneg (inv_nonneg.2 hr.le)] at hx hy;
+    try { apply_instance },
+  have := h hx hy,
+  simp_rw [←smul_add, ←smul_sub, norm_smul_of_nonneg (inv_nonneg.2 hr.le), ←div_eq_inv_mul,
+    div_le_div_right hr, div_le_iff hr, sub_mul] at this,
+  exact this hxy,
+end
+
+end semi_normed_group
+
+variables [normed_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_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

src/analysis/inner_product_space/basic.lean

@@ -5,8 +5,8 @@ Authors: Zhouhang Zhou, Sébastien Gouëzel, Frédéric Dupuis
 -/
 import algebra.direct_sum.module
 import analysis.complex.basic
+import analysis.convex.uniform
 import analysis.normed_space.bounded_linear_maps
-import analysis.convex.strict_convex_space
 import linear_algebra.bilinear_form
 import linear_algebra.sesquilinear_form
 
@@ -1071,6 +1071,19 @@ begin
   simp only [sq, ← mul_div_right_comm, ← add_div]
 end
 
+@[priority 100] -- See note [lower instance priority]
+instance inner_product_space.to_uniform_convex_space : uniform_convex_space F :=
+⟨λ ε hε, begin
+  refine ⟨2 - sqrt (4 - ε^2), sub_pos_of_lt $ (sqrt_lt' zero_lt_two).2 _, λ x hx y hy hxy, _⟩,
+  { norm_num,
+    exact pow_pos hε _ },
+  rw sub_sub_cancel,
+  refine le_sqrt_of_sq_le _,
+  rw [sq, eq_sub_iff_add_eq.2 (parallelogram_law_with_norm x y), ←sq (∥x - y∥), hx, hy],
+  norm_num,
+  exact pow_le_pow_of_le_left hε.le hxy _,
+end⟩
+
 section complex
 
 variables {V : Type*}
@@ -1574,19 +1587,6 @@ Compare `abs_inner_eq_norm_iff`, which takes the weaker hypothesis `abs ⟪x, y
 lemma inner_eq_norm_mul_iff_real {x y : F} : ⟪x, y⟫_ℝ = ∥x∥ * ∥y∥ ↔ ∥y∥ • x = ∥x∥ • y :=
 inner_eq_norm_mul_iff
 
-/-- An inner product space is strictly convex. We do not register this as an instance for an inner
-space over `𝕜`, `is_R_or_C 𝕜`, because there is no order of the typeclass argument that does not
-lead to a search of `[is_scalar_tower ℝ ?m E]` with unknown `?m`. -/
-instance inner_product_space.strict_convex_space : strict_convex_space ℝ F :=
-begin
-  refine strict_convex_space.of_norm_add (λ x y h, _),
-  rw [same_ray_iff_norm_smul_eq, eq_comm, ← inner_eq_norm_mul_iff_real,
-    real_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two, h,
-    add_mul_self_eq, sub_sub, add_sub_add_right_eq_sub, add_sub_cancel', mul_assoc,
-    mul_div_cancel_left],
-  exact _root_.two_ne_zero
-end
-
 /-- If the inner product of two unit vectors is `1`, then the two vectors are equal. One form of
 the equality case for Cauchy-Schwarz. -/
 lemma inner_eq_norm_mul_iff_of_norm_one {x y : E} (hx : ∥x∥ = 1) (hy : ∥y∥ = 1) :

src/analysis/normed/group/basic.lean

@@ -172,6 +172,9 @@ lemma norm_add_le_of_le {g₁ g₂ : E} {n₁ n₂ : ℝ} (H₁ : ∥g₁∥ ≤
   ∥g₁ + g₂∥ ≤ n₁ + n₂ :=
 le_trans (norm_add_le g₁ g₂) (add_le_add H₁ H₂)
 
+lemma norm_add₃_le (x y z : E) : ∥x + y + z∥ ≤ ∥x∥ + ∥y∥ + ∥z∥ :=
+norm_add_le_of_le (norm_add_le _ _) le_rfl
+
 lemma dist_add_add_le (g₁ g₂ h₁ h₂ : E) :
   dist (g₁ + g₂) (h₁ + h₂) ≤ dist g₁ h₁ + dist g₂ h₂ :=
 by simpa only [dist_add_left, dist_add_right] using dist_triangle (g₁ + g₂) (h₁ + g₂) (h₁ + h₂)
@@ -1046,7 +1049,7 @@ def normed_group.of_core (E : Type*) [add_comm_group E] [has_norm E]
   end
   ..semi_normed_group.of_core E (normed_group.core.to_semi_normed_group.core C) }
 
-variables [normed_group E] [normed_group F]
+variables [normed_group E] [normed_group F] {x y : E}
 
 @[simp] lemma norm_eq_zero {g : E} : ∥g∥ = 0 ↔ g = 0 := norm_eq_zero_iff'
 
@@ -1059,6 +1062,9 @@ lemma norm_ne_zero_iff {g : E} : ∥g∥ ≠ 0 ↔ g ≠ 0 := not_congr norm_eq_
 lemma norm_sub_eq_zero_iff {u v : E} : ∥u - v∥ = 0 ↔ u = v :=
 by rw [norm_eq_zero, sub_eq_zero]
 
+lemma norm_sub_pos_iff : 0 < ∥x - y∥ ↔ x ≠ y :=
+by { rw [(norm_nonneg _).lt_iff_ne, ne_comm], exact norm_sub_eq_zero_iff.not }
+
 lemma eq_of_norm_sub_le_zero {g h : E} (a : ∥g - h∥ ≤ 0) : g = h :=
 by rwa [← sub_eq_zero, ← norm_le_zero_iff]