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
- uniform_convex : ∀ ⦃ε : ℝ⦄, 0 < ε → (∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ∥x∥ = 1 → ∀ ⦃y : E⦄, ∥y∥ = 1 → ε ≤ ∥x - y∥ → ∥x + y∥ ≤ 2 - δ)
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.
See also uniform_convex_space.of_uniform_convex_closed_unit_ball.