# 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 #

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

## TODO #

- Milman-Pettis
- Hanner's inequalities

## Tags #

convex, uniformly convex

source
class UniformConvexSpace (E : Type u_1) [SeminormedAddCommGroup E] :
Prop

A uniformly convex space is a real normed space where the triangle inequality is strict with a uniform bound. Namely, over the `x` and `y` of norm `1`, `‖x + y‖` is uniformly bounded above by a constant `< 2` when `‖x - y‖` is uniformly bounded below by a positive constant.

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

Instances

source
theorem exists_forall_sphere_dist_add_le_two_sub (E : Type u_1) [SeminormedAddCommGroup E] [UniformConvexSpace E] {ε : ℝ} (hε : 0 < ε) :
∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
source
theorem exists_forall_closed_ball_dist_add_le_two_sub (E : Type u_1) [SeminormedAddCommGroup E] [UniformConvexSpace E] {ε : ℝ} [NormedSpace ℝ E] (hε : 0 < ε) :
∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
source
theorem exists_forall_closed_ball_dist_add_le_two_mul_sub (E : Type u_1) [SeminormedAddCommGroup E] [UniformConvexSpace E] {ε : ℝ} [NormedSpace ℝ E] (hε : 0 < ε) (r : ℝ) :
∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
source
@[instance 100]
instance UniformConvexSpace.toStrictConvexSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [UniformConvexSpace E] :
StrictConvexSpace ℝ E