mathlib documentation

analysis.convex.strict_convex_space

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 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_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_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_add {E : Type u_2} [normed_group E] [normed_space E] (h : ∀ (x y : E), x + y = x + ysame_ray x y) :

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

theorem strict_convex_space.of_norm_add_lt_aux {E : Type u_2} [normed_group E] [normed_space E] {a b c d : } (ha : 0 < a) (hab : a + b = 1) (hc : 0 < c) (hd : 0 < d) (hcd : c + d = 1) (hca : c a) {x y : E} (hy : y 1) (hxy : a x + b y < 1) :
c x + d y < 1
theorem strict_convex_space.of_norm_add_lt {E : Type u_2} [normed_group E] [normed_space E] {a b : } (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (h : ∀ (x y : E), x 1y 1x ya 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 shows that we only need to check it for fixed a and b.

theorem combo_mem_ball_of_ne {E : Type u_2} [normed_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_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_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.

theorem norm_add_lt_of_not_same_ray {E : Type u_2} [normed_group E] [normed_space E] [strict_convex_space E] {x y : E} (h : ¬same_ray x y) :

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

theorem lt_norm_sub_of_not_same_ray {E : Type u_2} [normed_group E] [normed_space E] [strict_convex_space E] {x y : E} (h : ¬same_ray x y) :
theorem same_ray_iff_norm_add {E : Type u_2} [normed_group E] [normed_space E] [strict_convex_space E] {x y : E} :

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.

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.

theorem dist_add_dist_eq_iff {E : Type u_2} [normed_group E] [normed_space E] [strict_convex_space E] {x y z : E} :

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_group E] [normed_space E] [strict_convex_space E] {x y : E} (h : x = y) :
(1 / 2) (x + y) < x x y
theorem eq_line_map_of_dist_eq_mul_of_dist_eq_mul {E : Type u_2} [normed_group E] [normed_space E] [strict_convex_space E] {r : } {PE : Type u_5} [metric_space PE] [normed_add_torsor E PE] {x y z : PE} (hxy : has_dist.dist x y = r * has_dist.dist x z) (hyz : has_dist.dist y z = (1 - r) * has_dist.dist x z) :
theorem eq_midpoint_of_dist_eq_half {E : Type u_2} [normed_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
noncomputable def isometry.affine_isometry_of_strict_convex_space {E : Type u_2} [normed_group E] [normed_space E] [strict_convex_space E] {F : Type u_3} [normed_group F] [normed_space F] {PF : Type u_4} {PE : Type u_5} [metric_space PF] [metric_space PE] [normed_add_torsor F PF] [normed_add_torsor E PE] {f : PF → PE} (hi : isometry f) :

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
@[simp]
theorem isometry.coe_affine_isometry_of_strict_convex_space {E : Type u_2} [normed_group E] [normed_space E] [strict_convex_space E] {F : Type u_3} [normed_group F] [normed_space F] {PF : Type u_4} {PE : Type u_5} [metric_space PF] [metric_space PE] [normed_add_torsor F PF] [normed_add_torsor E PE] {f : PF → PE} (hi : isometry f) :
@[simp]
theorem isometry.affine_isometry_of_strict_convex_space_apply {E : Type u_2} [normed_group E] [normed_space E] [strict_convex_space E] {F : Type u_3} [normed_group F] [normed_space F] {PF : Type u_4} {PE : Type u_5} [metric_space PF] [metric_space PE] [normed_add_torsor F PF] [normed_add_torsor E PE] {f : PF → PE} (hi : isometry f) (p : PF) :