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

• strictConvex_closedBall: a closed ball is strictly convex.
• combo_mem_ball_of_ne, openSegment_subset_ball_of_ne, norm_combo_lt_of_ne: a nontrivial convex combination of two points in a closed ball belong to the corresponding open ball;
• norm_add_lt_of_not_sameRay, sameRay_iff_norm_add, dist_add_dist_eq_iff: the triangle inequality dist x y + dist y z ≤ dist x z is a strict inequality unless y belongs 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:

• StrictConvexSpace.of_strictConvex_closed_unit_ball: if closed_ball (0 : E) 1 is strictly convex, then E is a strictly convex space;

• StrictConvexSpace.of_norm_add: if ‖x + y‖ = ‖x‖ + ‖y‖ implies SameRay ℝ x y for all nonzero x y : E, then E is 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 𝕜 = ℝ.

Tags

convex, strictly convex

class StrictConvexSpace (𝕜 : Type u_1) (E : Type u_2) [NormedLinearOrderedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] : Prop

• strictConvex_closedBall : ∀ (r : ℝ), 0 < r → StrictConvex 𝕜 (Metric.closedBall 0 r)

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.

theorem strictConvex_closedBall (𝕜 : Type u_1) {E : Type u_2} [NormedLinearOrderedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [StrictConvexSpace 𝕜 E] (x : E) (r : ℝ) : StrictConvex 𝕜 (Metric.closedBall x r)

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

theorem StrictConvexSpace.of_strictConvex_closed_unit_ball (𝕜 : Type u_1) {E : Type u_2} [NormedLinearOrderedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [LinearMap.CompatibleSMul E E 𝕜 ℝ] (h : StrictConvex 𝕜 (Metric.closedBall 0 1)) : StrictConvexSpace 𝕜 E

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‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, a + b = 1 ∧ ‖a • x + b • y‖ < 1) : StrictConvexSpace ℝ E

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‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ ‖a • x + b • y‖ ≠ 1) : StrictConvexSpace ℝ E

theorem StrictConvexSpace.of_norm_add_ne_two {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2) : StrictConvexSpace ℝ E

theorem StrictConvexSpace.of_pairwise_sphere_norm_ne_two {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : Set.Pairwise (Metric.sphere 0 1) fun x y => ‖x + y‖ ≠ 2) : StrictConvexSpace ℝ E

theorem StrictConvexSpace.of_norm_add {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y) : StrictConvexSpace ℝ E

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) : openSegment ℝ x y ⊆ Metric.ball z r

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.

theorem norm_add_lt_of_not_sameRay {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [StrictConvexSpace ℝ E] {x : E} {y : E} (h : ¬SameRay ℝ x y) : ‖x + y‖ < ‖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_sameRay {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [StrictConvexSpace ℝ E] {x : E} {y : E} (h : ¬SameRay ℝ x y) : ‖x‖ - ‖y‖ < ‖x - y‖

theorem abs_lt_norm_sub_of_not_sameRay {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [StrictConvexSpace ℝ E] {x : E} {y : E} (h : ¬SameRay ℝ x y) : |‖x‖ - ‖y‖| < ‖x - y‖

theorem sameRay_iff_norm_add {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [StrictConvexSpace ℝ E] {x : E} {y : E} : SameRay ℝ x y ↔ ‖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.

theorem not_sameRay_iff_norm_add_lt {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [StrictConvexSpace ℝ E] {x : E} {y : E} : ¬SameRay ℝ x y ↔ ‖x + y‖ < ‖x‖ + ‖y‖

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 sameRay_iff_norm_sub {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [StrictConvexSpace ℝ E] {x : E} {y : E} : SameRay ℝ x y ↔ ‖x - y‖ = |‖x‖ - ‖y‖|

theorem not_sameRay_iff_abs_lt_norm_sub {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [StrictConvexSpace ℝ E] {x : E} {y : E} : ¬SameRay ℝ x y ↔ |‖x‖ - ‖y‖| < ‖x - y‖

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 : PF → PE} (hi : Isometry f) : PF →ᵃⁱ[ℝ] PE

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.

@[simp]

theorem Isometry.coe_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 : PF → PE} (hi : Isometry f) : ↑(Isometry.affineIsometryOfStrictConvexSpace hi) = f

@[simp]

theorem Isometry.affineIsometryOfStrictConvexSpace_apply {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 : PF → PE} (hi : Isometry f) (p : PF) : ↑(Isometry.affineIsometryOfStrictConvexSpace hi) p = f p