mathlib3 documentation

analysis.convex.strict_convex_space

Strictly convex spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

strict_convex_closed_ball: a closed ball is strictly convex.
combo_mem_ball_of_ne, open_segment_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_same_ray, same_ray_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.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:

strict_convex_space.of_strict_convex_closed_unit_ball: if closed_ball (0 : E) 1 is strictly convex, then E is a strictly convex space;
strict_convex_space.of_norm_add: if ‖x + y‖ = ‖x‖ + ‖y‖ implies same_ray ℝ 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]

structure strict_convex_space (𝕜 : Type u_1) (E : Type u_2) [normed_linear_ordered_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] :

Prop

strict_convex_closed_ball : ∀ (r : ℝ), 0 < r → strict_convex 𝕜 (metric.closed_ball 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 strict_convex_closed_ball below.

See also strict_convex_space.of_strict_convex_closed_unit_ball.

Instances of this typeclass

uniform_convex_space.to_strict_convex_space

theorem strict_convex_closed_ball (𝕜 : Type u_1) {E : Type u_2} [normed_linear_ordered_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [strict_convex_space 𝕜 E] (x : E) (r : ℝ) :

strict_convex 𝕜 (metric.closed_ball x r)

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

theorem strict_convex_space.of_strict_convex_closed_unit_ball (𝕜 : Type u_1) {E : Type u_2} [normed_linear_ordered_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [normed_space ℝ E] [linear_map.compatible_smul E E 𝕜 ℝ] (h : strict_convex 𝕜 (metric.closed_ball 0 1)) :

strict_convex_space 𝕜 E

A real normed vector space is strictly convex provided that the unit ball is strictly convex.

theorem strict_convex_space.of_norm_combo_lt_one {E : Type u_2} [normed_add_comm_group E] [normed_space ℝ E] (h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → (∃ (a b : ℝ), a + b = 1 ∧ ‖a • x + b • y‖ < 1)) :

strict_convex_space ℝ 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 strict_convex_space.of_norm_combo_ne_one {E : Type u_2} [normed_add_comm_group E] [normed_space ℝ 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)) :

strict_convex_space ℝ E

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

strict_convex_space ℝ E

theorem strict_convex_space.of_pairwise_sphere_norm_ne_two {E : Type u_2} [normed_add_comm_group E] [normed_space ℝ E] (h : (metric.sphere 0 1).pairwise (λ (x y : E), ‖x + y‖ ≠ 2)) :

strict_convex_space ℝ E

theorem strict_convex_space.of_norm_add {E : Type u_2} [normed_add_comm_group E] [normed_space ℝ E] (h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → same_ray ℝ x y) :

strict_convex_space ℝ 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} [normed_add_comm_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_add_comm_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) :

open_segment ℝ 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} [normed_add_comm_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_add_comm_group E] [normed_space ℝ E] [strict_convex_space ℝ E] {x y : E} (h : ¬same_ray ℝ 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_same_ray {E : Type u_2} [normed_add_comm_group E] [normed_space ℝ E] [strict_convex_space ℝ E] {x y : E} (h : ¬same_ray ℝ x y) :

‖x‖ - ‖y‖ < ‖x - y‖

theorem abs_lt_norm_sub_of_not_same_ray {E : Type u_2} [normed_add_comm_group E] [normed_space ℝ E] [strict_convex_space ℝ E] {x y : E} (h : ¬same_ray ℝ x y) :

|‖x‖ - ‖y‖| < ‖x - y‖

theorem same_ray_iff_norm_add {E : Type u_2} [normed_add_comm_group E] [normed_space ℝ E] [strict_convex_space ℝ E] {x y : E} :

same_ray ℝ 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} [normed_add_comm_group E] [normed_space ℝ E] [strict_convex_space ℝ E] {x 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_same_ray_iff_norm_add_lt {E : Type u_2} [normed_add_comm_group E] [normed_space ℝ E] [strict_convex_space ℝ E] {x y : E} :

¬same_ray ℝ 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 same_ray_iff_norm_sub {E : Type u_2} [normed_add_comm_group E] [normed_space ℝ E] [strict_convex_space ℝ E] {x y : E} :

same_ray ℝ x y ↔ ‖x - y‖ = |‖x‖ - ‖y‖|

theorem not_same_ray_iff_abs_lt_norm_sub {E : Type u_2} [normed_add_comm_group E] [normed_space ℝ E] [strict_convex_space ℝ E] {x y : E} :

¬same_ray ℝ x y ↔ |‖x‖ - ‖y‖| < ‖x - y‖

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

has_dist.dist x y + has_dist.dist y z = has_dist.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} [normed_add_comm_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_add_comm_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) :

y = ⇑(affine_map.line_map x z) r

theorem eq_midpoint_of_dist_eq_half {E : Type u_2} [normed_add_comm_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_add_comm_group E] [normed_space ℝ E] [strict_convex_space ℝ E] {F : Type u_3} [normed_add_comm_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) :

PF →ᵃⁱ[ℝ ] PE

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

hi.affine_isometry_of_strict_convex_space = {to_affine_map := {to_fun := (affine_map.of_map_midpoint f _ _).to_fun, linear := (affine_map.of_map_midpoint f _ _).linear, map_vadd' := _}, norm_map := _}

@[simp]

theorem isometry.coe_affine_isometry_of_strict_convex_space {E : Type u_2} [normed_add_comm_group E] [normed_space ℝ E] [strict_convex_space ℝ E] {F : Type u_3} [normed_add_comm_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) :

⇑(hi.affine_isometry_of_strict_convex_space) = f

@[simp]

theorem isometry.affine_isometry_of_strict_convex_space_apply {E : Type u_2} [normed_add_comm_group E] [normed_space ℝ E] [strict_convex_space ℝ E] {F : Type u_3} [normed_add_comm_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) :

⇑(hi.affine_isometry_of_strict_convex_space) p = f p