Strictly convex spaces #
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 #
StrictConvexSpace: a typeclass saying that a given normed space over a normed linear ordered
ℚ) 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
strictConvex_closedBall: a closed ball is strictly convex.
norm_combo_lt_of_ne: a nontrivial convex combination of two points in a closed ball belong to the corresponding open ball;
dist_add_dist_eq_iff: the triangle inequality
dist x y + dist y z ≤ dist x zis a strict inequality unless
ybelongs to the segment
[x -[ℝ] z].
Isometry.affineIsometryOfStrictConvexSpace: an isometry of
NormedAddTorsors for real normed spaces, strictly convex in the case of the codomain, is an affine isometry.
We also provide several lemmas that can be used as alternative constructors for
StrictConvex ℝ E:
closed_ball (0 : E) 1is strictly convex, then
Eis a strictly convex space;
Implementation notes #
While the definition is formulated for any normed linear ordered field, most of the lemmas are
formulated only for the case
𝕜 = ℝ.
convex, strictly convex
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
A real normed vector space is strictly convex provided that the unit ball is strictly convex.
Strict convexity is equivalent to
‖a • x + b • y‖ < 1 for all
y of norm at most
and all strictly positive
b such that
a + b = 1. This lemma shows that it suffices to
check this for points of norm one and some
b such that
a + b = 1.
x ≠ y belong to the same closed ball, then a convex combination of
positive coefficients belongs to the corresponding open ball.
x ≠ y belong to the same closed ball, then the open segment with endpoints
included in the corresponding open ball.
y are two distinct vectors of norm at most
r, then a convex combination of
y with positive coefficients has norm strictly less than
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
y are not in the same ray if and only if the
triangle inequality for
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.
An isometry of
NormedAddTorsors 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