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

src/analysis/convex/strict_convex_space.lean

@@ -106,6 +106,54 @@ begin
     smul_right_inj hb.ne'] using (h _ _ H).norm_smul_eq.symm
 end
 
+lemma strict_convex_space.of_norm_add_lt_aux {a b c d : ℝ} (ha : 0 < a) (hb : 0 < b)
+  (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 :=
+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,
+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) :
+  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 hb 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 ha 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 }
+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

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
 
@@ -1033,7 +1033,7 @@ begin
 end
 omit 𝕜
 
-lemma parallelogram_law_with_norm_real {x y : F} :
+lemma parallelogram_law_with_norm_real (x y : F) :
   ∥x + y∥ * ∥x + y∥ + ∥x - y∥ * ∥x - y∥ = 2 * (∥x∥ * ∥x∥ + ∥y∥ * ∥y∥) :=
 by { have h := @parallelogram_law_with_norm ℝ F _ _ x y, simpa using h }
 
@@ -1067,6 +1067,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_iff 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_real 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*}
@@ -1570,19 +1583,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

@@ -166,6 +166,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₂)
@@ -1010,7 +1013,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'
 
@@ -1023,6 +1026,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]
 

src/data/complex/basic.lean

@@ -511,8 +511,8 @@ lemma im_le_abs (z : ℂ) : z.im ≤ abs z :=
 (abs_le.1 (abs_im_le_abs _)).2
 
 @[simp] lemma abs_re_lt_abs {z : ℂ} : |z.re| < abs z ↔ z.im ≠ 0 :=
-by rw [abs, real.lt_sqrt (_root_.abs_nonneg _) (norm_sq_nonneg z), norm_sq_apply,
-  _root_.sq_abs, ← sq, lt_add_iff_pos_right, mul_self_pos]
+by rw [abs, real.lt_sqrt (_root_.abs_nonneg _), norm_sq_apply, _root_.sq_abs, ← sq,
+  lt_add_iff_pos_right, mul_self_pos]
 
 @[simp] lemma abs_im_lt_abs {z : ℂ} : |z.im| < abs z ↔ z.re ≠ 0 :=
 by simpa using @abs_re_lt_abs (z * I)

src/data/real/sqrt.lean

@@ -207,6 +207,9 @@ lt_iff_lt_of_le_iff_le (sqrt_le_sqrt_iff hx)
 theorem sqrt_lt_sqrt_iff_of_pos (hy : 0 < y) : sqrt x < sqrt y ↔ x < y :=
 by rw [sqrt, sqrt, nnreal.coe_lt_coe, nnreal.sqrt_lt_sqrt_iff, to_nnreal_lt_to_nnreal_iff hy]
 
+lemma sqrt_lt_iff (hy : 0 < y) : sqrt x < y ↔ x < y ^ 2 :=
+by rw [←sqrt_lt_sqrt_iff_of_pos (pow_pos hy _), sqrt_sq hy.le]
+
 theorem sqrt_le_sqrt (h : x ≤ y) : sqrt x ≤ sqrt y :=
 by { rw [sqrt, sqrt, nnreal.coe_le_coe, nnreal.sqrt_le_sqrt_iff], exact to_nnreal_le_to_nnreal h }
 
@@ -293,16 +296,11 @@ by rw [←div_sqrt, one_div_div, div_sqrt]
 theorem sqrt_div_self : sqrt x / x = (sqrt x)⁻¹ :=
 by rw [sqrt_div_self', one_div]
 
-theorem lt_sqrt (hx : 0 ≤ x) (hy : 0 ≤ y) : x < sqrt y ↔ x ^ 2 < y :=
-by rw [mul_self_lt_mul_self_iff hx (sqrt_nonneg y), sq, mul_self_sqrt hy]
+lemma lt_sqrt (hx : 0 ≤ x) : x < sqrt y ↔ x ^ 2 < y :=
+by rw [←sqrt_lt_sqrt_iff (sq_nonneg _), sqrt_sq hx]
 
-theorem sq_lt : x^2 < y ↔ -sqrt y < x ∧ x < sqrt y :=
-begin
-  split,
-  { simpa only [← sqrt_lt_sqrt_iff (sq_nonneg x), sqrt_sq_eq_abs] using abs_lt.mp },
-  { rw [← abs_lt, ← sq_abs],
-    exact λ h, (lt_sqrt (abs_nonneg x) (sqrt_pos.mp (lt_of_le_of_lt (abs_nonneg x) h)).le).mp h },
-end
+lemma sq_lt : x^2 < y ↔ -sqrt y < x ∧ x < sqrt y :=
+by rw [←abs_lt, ←sq_abs, lt_sqrt (abs_nonneg _)]
 
 theorem neg_sqrt_lt_of_sq_lt (h : x^2 < y) : -sqrt y < x := (sq_lt.mp h).1