mathlib documentation

analysis.convex.uniform

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 #

Tags #

convex, uniformly convex

@[class]
structure uniform_convex_space (E : Type u_1) [seminormed_add_comm_group 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.

See also uniform_convex_space.of_uniform_convex_closed_unit_ball.

Instances of this typeclass
theorem exists_forall_sphere_dist_add_le_two_sub (E : Type u_1) [seminormed_add_comm_group E] [uniform_convex_space E] {ε : } (hε : 0 < ε) :
∃ (δ : ), 0 < δ ∀ ⦃x : E⦄, x = 1∀ ⦃y : E⦄, y = 1ε x - yx + y 2 - δ
theorem exists_forall_closed_ball_dist_add_le_two_sub (E : Type u_1) [seminormed_add_comm_group E] [uniform_convex_space E] {ε : } [normed_space E] (hε : 0 < ε) :
∃ (δ : ), 0 < δ ∀ ⦃x : E⦄, x 1∀ ⦃y : E⦄, y 1ε x - yx + y 2 - δ
theorem exists_forall_closed_ball_dist_add_le_two_mul_sub (E : Type u_1) [seminormed_add_comm_group E] [uniform_convex_space E] {ε : } [normed_space E] (hε : 0 < ε) (r : ) :
∃ (δ : ), 0 < δ ∀ ⦃x : E⦄, x r∀ ⦃y : E⦄, y rε x - yx + y 2 * r - δ