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 #
strict_convex_space: 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
strict_convex_closed_ball: 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.affine_isometry_of_strict_convex_space: an isometry of
normed_add_torsors 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
strict_convex ℝ 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
Instances of this typeclass
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 shows that we only need to check
it for fixed
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
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
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