mathlib3 documentation

analysis.convex.strict_convex_space

Strictly convex spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines strictly convex spaces. A normed space is strictly convex if all closed balls are strictly convex. This does not mean that the norm is strictly convex (in fact, it never is).

Main definitions #

strict_convex_space: a typeclass saying that a given normed space over a normed linear ordered field (e.g., or ) is strictly convex. The definition requires strict convexity of a closed ball of positive radius with center at the origin; strict convexity of any other closed ball follows from this assumption.

Main results #

In a strictly convex space, we prove

We also provide several lemmas that can be used as alternative constructors for strict_convex ℝ E:

Implementation notes #

While the definition is formulated for any normed linear ordered field, most of the lemmas are formulated only for the case 𝕜 = ℝ.

Tags #

convex, strictly convex

@[class]
structure strict_convex_space (𝕜 : Type u_1) (E : Type u_2) [normed_linear_ordered_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] :
Prop

A strictly convex space is a normed space where the closed balls are strictly convex. We only require balls of positive radius with center at the origin to be strictly convex in the definition, then prove that any closed ball is strictly convex in strict_convex_closed_ball below.

See also strict_convex_space.of_strict_convex_closed_unit_ball.

Instances of this typeclass
theorem strict_convex_closed_ball (𝕜 : Type u_1) {E : Type u_2} [normed_linear_ordered_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [strict_convex_space 𝕜 E] (x : E) (r : ) :

A closed ball in a strictly convex space is strictly convex.

A real normed vector space is strictly convex provided that the unit ball is strictly convex.

theorem strict_convex_space.of_norm_combo_lt_one {E : Type u_2} [normed_add_comm_group E] [normed_space E] (h : (x y : E), x = 1 y = 1 x y ( (a b : ), a + b = 1 a x + b y < 1)) :

Strict convexity is equivalent to ‖a • x + b • y‖ < 1 for all x and y of norm at most 1 and all strictly positive a and b such that a + b = 1. This lemma shows that it suffices to check this for points of norm one and some a, b such that a + b = 1.

theorem strict_convex_space.of_norm_combo_ne_one {E : Type u_2} [normed_add_comm_group E] [normed_space E] (h : (x y : E), x = 1 y = 1 x y ( (a b : ), 0 a 0 b a + b = 1 a x + b y 1)) :

If ‖x + y‖ = ‖x‖ + ‖y‖ implies that x y : E are in the same ray, then E is a strictly convex space. See also a more

theorem combo_mem_ball_of_ne {E : Type u_2} [normed_add_comm_group E] [normed_space E] [strict_convex_space E] {x y z : E} {a b r : } (hx : x metric.closed_ball z r) (hy : y metric.closed_ball z r) (hne : x y) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
a x + b y metric.ball z r

If x ≠ y belong to the same closed ball, then a convex combination of x and y with positive coefficients belongs to the corresponding open ball.

theorem open_segment_subset_ball_of_ne {E : Type u_2} [normed_add_comm_group E] [normed_space E] [strict_convex_space E] {x y z : E} {r : } (hx : x metric.closed_ball z r) (hy : y metric.closed_ball z r) (hne : x y) :

If x ≠ y belong to the same closed ball, then the open segment with endpoints x and y is included in the corresponding open ball.

theorem norm_combo_lt_of_ne {E : Type u_2} [normed_add_comm_group E] [normed_space E] [strict_convex_space E] {x y : E} {a b r : } (hx : x r) (hy : y r) (hne : x y) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
a x + b y < r

If x and y are two distinct vectors of norm at most r, then a convex combination of x and y with positive coefficients has norm strictly less than r.

In a strictly convex space, if x and y are not in the same ray, then ‖x + y‖ < ‖x‖ + ‖y‖.

In a strictly convex space, two vectors x, y are in the same ray if and only if the triangle inequality for x and y becomes an equality.

theorem eq_of_norm_eq_of_norm_add_eq {E : Type u_2} [normed_add_comm_group E] [normed_space E] [strict_convex_space E] {x y : E} (h₁ : x = y) (h₂ : x + y = x + y) :
x = y

If x and y are two vectors in a strictly convex space have the same norm and the norm of their sum is equal to the sum of their norms, then they are equal.

In a strictly convex space, two vectors x, y are not in the same ray if and only if the triangle inequality for x and y is strict.

In a strictly convex space, the triangle inequality turns into an equality if and only if the middle point belongs to the segment joining two other points.

theorem norm_midpoint_lt_iff {E : Type u_2} [normed_add_comm_group E] [normed_space E] [strict_convex_space E] {x y : E} (h : x = y) :
(1 / 2) (x + y) < x x y
theorem eq_midpoint_of_dist_eq_half {E : Type u_2} [normed_add_comm_group E] [normed_space E] [strict_convex_space E] {PE : Type u_5} [metric_space PE] [normed_add_torsor E PE] {x y z : PE} (hx : has_dist.dist x y = has_dist.dist x z / 2) (hy : has_dist.dist y z = has_dist.dist x z / 2) :
y = midpoint x z

An isometry of normed_add_torsors for real normed spaces, strictly convex in the case of the codomain, is an affine isometry. Unlike Mazur-Ulam, this does not require the isometry to be surjective.

Equations