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

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

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

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

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

instance UniformConvexSpace.toStrictConvexSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [UniformConvexSpace E] : StrictConvexSpace ℝ E

Equations

• (_ : StrictConvexSpace ℝ E) = (_ : StrictConvexSpace ℝ E)