Documentation

Mathlib.Analysis.Convex.StrictConvexSpace

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 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 StrictConvex ℝ 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 StrictConvexSpace (𝕜 : Type u_1) (E : Type u_2) [NormedLinearOrderedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] :

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 strictConvex_closedBall below.

See also StrictConvexSpace.of_strictConvex_closed_unit_ball.

Instances
    theorem strictConvex_closedBall (𝕜 : Type u_1) {E : Type u_2} [NormedLinearOrderedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [StrictConvexSpace 𝕜 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 StrictConvexSpace.of_norm_combo_lt_one {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] (h : ∀ (x y : E), x = 1y = 1x ya 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 StrictConvexSpace.of_norm_combo_ne_one {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] (h : ∀ (x y : E), x = 1y = 1x ya b, 0 a 0 b a + b = 1 a x + b y 1) :
    theorem StrictConvexSpace.of_norm_add_ne_two {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] (h : ∀ ⦃x y : E⦄, x = 1y = 1x yx + y 2) :
    theorem StrictConvexSpace.of_norm_add {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] (h : ∀ (x y : E), x = 1y = 1x + y = 2SameRay x y) :

    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} [NormedAddCommGroup E] [NormedSpace E] [StrictConvexSpace E] {x : E} {y : E} {z : E} {a : } {b : } {r : } (hx : x Metric.closedBall z r) (hy : y Metric.closedBall 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 openSegment_subset_ball_of_ne {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] [StrictConvexSpace E] {x : E} {y : E} {z : E} {r : } (hx : x Metric.closedBall z r) (hy : y Metric.closedBall 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} [NormedAddCommGroup E] [NormedSpace E] [StrictConvexSpace E] {x : E} {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} [NormedAddCommGroup E] [NormedSpace E] [StrictConvexSpace E] {x : E} {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.

    theorem dist_add_dist_eq_iff {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] [StrictConvexSpace E] {x : E} {y : E} {z : E} :
    dist x y + dist y z = dist x z y segment x z

    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} [NormedAddCommGroup E] [NormedSpace E] [StrictConvexSpace E] {x : E} {y : E} (h : x = y) :
    (1 / 2) (x + y) < x x y
    theorem eq_lineMap_of_dist_eq_mul_of_dist_eq_mul {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] [StrictConvexSpace E] {r : } {PE : Type u_4} [MetricSpace PE] [NormedAddTorsor E PE] {x : PE} {y : PE} {z : PE} (hxy : dist x y = r * dist x z) (hyz : dist y z = (1 - r) * dist x z) :
    y = ↑(AffineMap.lineMap x z) r
    theorem eq_midpoint_of_dist_eq_half {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] [StrictConvexSpace E] {PE : Type u_4} [MetricSpace PE] [NormedAddTorsor E PE] {x : PE} {y : PE} {z : PE} (hx : dist x y = dist x z / 2) (hy : dist y z = dist x z / 2) :
    y = midpoint x z
    noncomputable def Isometry.affineIsometryOfStrictConvexSpace {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] [StrictConvexSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {PF : Type u} {PE : Type u_4} [MetricSpace PF] [MetricSpace PE] [NormedAddTorsor F PF] [NormedAddTorsor E PE] {f : PFPE} (hi : Isometry f) :

    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 be surjective.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For