# 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

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.

## Instances

## Equations

- ⋯ = ⋯