Affine segments and membership criteria

Mathlib describes membership in a segment through the ray predicate SameRay by mem_segment_iff_sameRay: x ∈ [y -[𝕜] z] ↔ SameRay 𝕜 (x - y) (z - x). That form is symmetric in the two endpoints, and the differences x - y, z - x are exactly what a metric consumer does not want: such a consumer holds a point m and an endpoint w, and asks whether m lies on the segment [0, w] in terms of the two data it can measure — the direction of m against w, and the two norms. This file supplies that reading, together with its mirror in which the origin sits in the middle of the segment rather than at an end, and the inner-product form of both.

Each criterion is stated at the generality its proof uses. The origin-at-an-end one compares two norms, and is stated for a real normed space; the inner-product forms replace SameRay by the equality case of the Cauchy--Schwarz inequality, and are stated for a real inner product space.

The bridge between the ray form and the inner-product forms is Mathlib's pair sameRay_iff_norm_smul_eq : SameRay ℝ x y ↔ ‖x‖ • y = ‖y‖ • x and inner_eq_norm_mul_iff_real : ⟪x, y⟫_ℝ = ‖x‖ * ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y, used directly: together they say that two vectors lie on a common ray exactly when Cauchy--Schwarz is an equality for them. No strict convexity is involved: the alternative route through sameRay_iff_norm_add would need a StrictConvexSpace ℝ E instance, whereas sameRay_iff_norm_smul_eq and inner_eq_norm_mul_iff_real hold in any normed, respectively inner product, space.

The clamped affine segment Set.convexSegment joins two points of any convex set, with no topology or norm required. It agrees with the affine line map on [0, 1] and is constant outside that interval. Its smoothness in convex open subsets is developed in TauCeti/Geometry/Manifold/ContMDiff/Subtype.lean, and its Riemannian length in TauCeti/Geometry/Manifold/Riemannian/Convex.lean.

The affine half-open segment result is also recorded here: in an additive commutative group with a module structure over a linear ordered field, it identifies the image of a scalar interval under an affine parametrization with a segment whose terminal endpoint is removed.

Main results

• Set.convexSegment — an affine segment in a convex set, clamped to [0, 1].
• TauCeti.mem_segment_zero_left_iff_sameRay_and_norm_le — m ∈ [0 -[ℝ] w] ↔ SameRay ℝ m w ∧ ‖m‖ ≤ ‖w‖. Both conjuncts are needed.
• TauCeti.eq_of_mem_segment_zero_left_of_norm_eq — the norm separates the points of [0, w].
• TauCeti.mem_segment_zero_left_iff_real_inner_eq_norm_mul_and_norm_le and TauCeti.zero_mem_segment_iff_real_inner_eq_neg_norm_mul — the two criteria in a real inner product space.
• TauCeti.image_add_smul_Ico — the affine image of Ico 0 D is a segment with its terminal endpoint removed.

The origin-at-an-end and origin-in-the-middle criteria are consumed by TauCeti/Analysis/Complex/Conformal/Poincare/Betweenness.lean, which identifies the hyperbolic segments of the Poincaré disc issuing from, or straddling, the origin with the Euclidean ones; ℂ is a real inner product space with ⟪w, z⟫_ℝ = (z * conj w).re (Complex.inner), so the two inner-product criteria translate the ray and norm conditions into complex-number formulas. The affine half-open segment result is consumed by TauCeti/Analysis/Complex/Conformal/SchwarzChristoffel/UnboundedEdge.lean.

def Set.convexSegment {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [LinearOrder 𝕜] [IsOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) (hs : Convex 𝕜 s) (x y : ↑s) : 𝕜 → ↑s

The affine segment between two points of a convex set, parametrized on [0, 1] and extended constantly outside that interval. No topology is needed for this construction.

Equations

• s.convexSegment hs x y = Set.IccExtend ⋯ fun (t : ↑(Set.Icc 0 1)) => ⟨(AffineMap.lineMap ↑x ↑y) ↑t, ⋯⟩

@[simp]

theorem Set.coe_convexSegment_apply {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [LinearOrder 𝕜] [IsOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) (hs : Convex 𝕜 s) (x y : ↑s) (t : 𝕜) : ↑(s.convexSegment hs x y t) = (AffineMap.lineMap ↑x ↑y) ↑(projIcc 0 1 ⋯ t)

The ambient value of the clamped segment is the affine line map at the clamped parameter.

theorem Set.convexSegment_val_eqOn {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [LinearOrder 𝕜] [IsOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) (hs : Convex 𝕜 s) (x y : ↑s) : EqOn (Subtype.val ∘ s.convexSegment hs x y) (⇑(AffineMap.lineMap ↑x ↑y)) (Icc 0 1)

On [0, 1], the clamped segment agrees with the ambient affine line map.

@[simp]

theorem Set.convexSegment_zero {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [LinearOrder 𝕜] [IsOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) (hs : Convex 𝕜 s) (x y : ↑s) : s.convexSegment hs x y 0 = x

The clamped segment starts at its first endpoint.

@[simp]

theorem Set.convexSegment_one {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [LinearOrder 𝕜] [IsOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) (hs : Convex 𝕜 s) (x y : ↑s) : s.convexSegment hs x y 1 = y

The clamped segment ends at its second endpoint.

Segments and rays

theorem TauCeti.mem_segment_zero_left_iff_sameRay_and_norm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {m w : E} : m ∈ segment ℝ 0 w ↔ SameRay ℝ m w ∧ ‖m‖ ≤ ‖w‖

Membership in the segment from the origin, read off the direction and the two norms. A point m lies on [0, w] exactly when it points along w and is no further from the origin than w is.

Both conjuncts are needed: for w ≠ 0 the point (2 : ℝ) • w satisfies the first without satisfying the second.

theorem TauCeti.eq_of_mem_segment_zero_left_of_norm_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {w m₁ m₂ : E} (h₁ : m₁ ∈ segment ℝ 0 w) (h₂ : m₂ ∈ segment ℝ 0 w) (h : ‖m₁‖ = ‖m₂‖) : m₁ = m₂

Two points of a segment from the origin with the same norm coincide. The segment [0, w] carries no two distinct points at the same distance from 0: it is contained in a ray, on which the norm is injective (norm_injOn_ray_right).

Half-open affine segments

theorem TauCeti.image_add_smul_Ico {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {x y u : E} {D : 𝕜} (hDpos : 0 < D) (hu : u ≠ 0) (hdir : y - x = D • u) : (fun (t : 𝕜) => x + t • u) '' Set.Ico 0 D = segment 𝕜 x y \ {y}

A nonzero affine ray parametrizes a half-open segment. If y - x = D • u with D > 0, then the points x + t • u for 0 ≤ t < D are exactly the segment from x to y with y removed.

The inner-product forms

theorem TauCeti.mem_segment_zero_left_iff_real_inner_eq_norm_mul_and_norm_le {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x y : F} : x ∈ segment ℝ 0 y ↔ inner ℝ x y = ‖x‖ * ‖y‖ ∧ ‖x‖ ≤ ‖y‖

Membership in the segment from the origin, read off the inner product. The inner-product form of TauCeti.mem_segment_zero_left_iff_sameRay_and_norm_le: by sameRay_iff_norm_smul_eq and inner_eq_norm_mul_iff_real, two vectors lie on a common ray exactly when Cauchy–Schwarz is an equality for them.

theorem TauCeti.zero_mem_segment_iff_real_inner_eq_neg_norm_mul {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x y : F} : 0 ∈ segment ℝ x y ↔ inner ℝ x y = -(‖x‖ * ‖y‖)

The origin lies between two vectors exactly when their inner product is minimal. The mirror of TauCeti.mem_segment_zero_left_iff_real_inner_eq_norm_mul_and_norm_le, with the origin in the middle of the segment rather than at an end: mem_segment_iff_sameRay at the point 0 says that x and -y lie on a common ray, so Cauchy–Schwarz is an equality at the other end of its range, ⟪x, y⟫_ℝ = -(‖x‖ * ‖y‖).

No nondegeneracy is needed: if x = 0 then 0 is an endpoint of the segment and both sides hold, and symmetrically for y.