.lake/packages/mathlib/Mathlib/Analysis/Convex/Uniform.lean

1/-

3Released under Apache 2.0 license as described in the file LICENSE.

4Authors: Yaël Dillies

5-/

6module

8public import Mathlib.Analysis.Convex.StrictConvexSpace

10/-!

11# Uniformly convex spaces

13This file defines uniformly convex spaces, which are real normed vector spaces in which for all

14strictly positive `ε`, there exists some strictly positive `δ` such that `ε ≤ ‖x - y‖` implies

15`‖x + y‖ ≤ 2 - δ` for all `x` and `y` of norm at most than `1`. This means that the triangle

16inequality is strict with a uniform bound, as opposed to strictly convex spaces where the triangle

17inequality is strict but not necessarily uniformly (`‖x + y‖ < ‖x‖ + ‖y‖` for all `x` and `y` not in

18the same ray).

20## Main declarations

22`UniformConvexSpace E` means that `E` is a uniformly convex space.

24## TODO

26* Milman-Pettis

27* Hanner's inequalities

29## Tags

31convex, uniformly convex

32-/

34public section

36/-- A *uniformly convex space* is a real normed space where the triangle inequality is strict with a

37uniform bound. Namely, over the `x` and `y` of norm `1`, `‖x + y‖` is uniformly bounded above

38by a constant `< 2` when `‖x - y‖` is uniformly bounded below by a positive constant. -/

39class UniformConvexSpace (E : Type*) [SeminormedAddCommGroup E] : Prop where

40 uniform_convex : ∀ ⦃ε : ℝ⦄,

    0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y⦄, ‖y‖ = 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ

43variable {E : Type*}

45section SeminormedAddCommGroup

47variable (E) [SeminormedAddCommGroup E] [UniformConvexSpace E] {ε : ℝ}

49theorem exists_forall_sphere_dist_add_le_two_sub (hε : 0 < ε) :

    ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y⦄, ‖y‖ = 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ :=

51 UniformConvexSpace.uniform_convex hε

53variable [NormedSpace ℝ E]

55theorem exists_forall_closed_ball_dist_add_le_two_sub (hε : 0 < ε) :

    ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y⦄, ‖y‖ ≤ 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ := by

57 have hε' : 0 < ε / 3 := div_pos hε zero_lt_three

58 obtain ⟨δ, hδ, h⟩ := exists_forall_sphere_dist_add_le_two_sub E hε'

59 set δ' := min (1 / 2) (min (ε / 3) <| δ / 3)

60 refine ⟨δ', lt_min one_half_pos <| lt_min hε' (div_pos hδ zero_lt_three), fun x hx y hy hxy => ?_⟩

61 obtain hx' | hx' := le_or_gt ‖x‖ (1 - δ')

62 · rw [← one_add_one_eq_two]

63 exact (norm_add_le_of_le hx' hy).trans (sub_add_eq_add_sub _ _ _).le

64 obtain hy' | hy' := le_or_gt ‖y‖ (1 - δ')

65 · rw [← one_add_one_eq_two]

66 exact (norm_add_le_of_le hx hy').trans (add_sub_assoc _ _ _).ge

67 have hδ' : 0 < 1 - δ' := sub_pos_of_lt (min_lt_of_left_lt one_half_lt_one)

68 have h₁ : ∀ z : E, 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1 := by

69 rintro z hz

70 rw [norm_smul_of_nonneg (inv_nonneg.2 <| norm_nonneg _), inv_mul_cancel₀ (hδ'.trans hz).ne']

71 have h₂ : ∀ z : E, ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ' := by

72 rintro z hz hδz

73 nth_rw 3 [← one_smul ℝ z]

74 rwa [← sub_smul,

75 norm_smul_of_nonneg (sub_nonneg_of_le <| (one_le_inv₀ (hδ'.trans_le hδz)).2 hz),

76 sub_mul, inv_mul_cancel₀ (hδ'.trans_le hδz).ne', one_mul, sub_le_comm]

77 set x' := ‖x‖⁻¹ • x

78 set y' := ‖y‖⁻¹ • y

79 have hxy' : ε / 3 ≤ ‖x' - y'‖ :=

80 calc

81 ε / 3 = ε - (ε / 3 + ε / 3) := by ring

82 _ ≤ ‖x - y‖ - (‖x' - x‖ + ‖y' - y‖) := by

83 gcongr

84 · exact (h₂ _ hx hx'.le).trans <| min_le_of_right_le <| min_le_left _ _

85 · exact (h₂ _ hy hy'.le).trans <| min_le_of_right_le <| min_le_left _ _

86 _ ≤ _ := by

87 have : ∀ x' y', x - y = x' - y' + (x - x') + (y' - y) := fun _ _ => by abel

88 rw [sub_le_iff_le_add, norm_sub_rev _ x, ← add_assoc, this]

89 exact norm_add₃_le

90 calc

91 ‖x + y‖ ≤ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖ := by

92 have : ∀ x' y', x + y = x' + y' + (x - x') + (y - y') := fun _ _ => by abel

93 rw [norm_sub_rev, norm_sub_rev y', this]

94 exact norm_add₃_le

95 _ ≤ 2 - δ + δ' + δ' := by

96 gcongr

97 exacts [h (h₁ _ hx') (h₁ _ hy') hxy', h₂ _ hx hx'.le, h₂ _ hy hy'.le]

98 _ ≤ 2 - δ' := by

99 suffices δ' ≤ δ / 3 by linarith

100 exact min_le_of_right_le <| min_le_right _ _

101

102theorem exists_forall_closed_ball_dist_add_le_two_mul_sub (hε : 0 < ε) (r : ℝ) :

103

    ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ := by

104 obtain hr | hr := le_or_gt r 0

105 · exact ⟨1, one_pos, fun x hx y hy h => (hε.not_ge <|

106 h.trans <| (norm_sub_le _ _).trans <| add_nonpos (hx.trans hr) (hy.trans hr)).elim⟩

107 obtain ⟨δ, hδ, h⟩ := exists_forall_closed_ball_dist_add_le_two_sub E (div_pos hε hr)

108 refine ⟨δ * r, mul_pos hδ hr, fun x hx y hy hxy => ?_⟩

109 rw [← div_le_one hr, div_eq_inv_mul, ← norm_smul_of_nonneg (inv_nonneg.2 hr.le)] at hx hy

110 have := h hx hy

111 simp_rw [← smul_add, ← smul_sub, norm_smul_of_nonneg (inv_nonneg.2 hr.le), ← div_eq_inv_mul,

112 div_le_div_iff_of_pos_right hr, div_le_iff₀ hr, sub_mul] at this

113 exact this hxy

114

115end SeminormedAddCommGroup

116

117variable [NormedAddCommGroup E] [NormedSpace ℝ E] [UniformConvexSpace E]

118

119-- See note [lower instance priority]

120instance (priority := 100) UniformConvexSpace.toStrictConvexSpace : StrictConvexSpace ℝ E :=

121 StrictConvexSpace.of_norm_add_ne_two fun _ _ hx hy hxy =>

122 let ⟨_, hδ, h⟩ := exists_forall_closed_ball_dist_add_le_two_sub E (norm_sub_pos_iff.2 hxy)

123 ((h hx.le hy.le le_rfl).trans_lt <| sub_lt_self _ hδ).ne