Convex combinations: sub-convex combinations and the centroid

This file collects facts on three topics about finite convex combinations in a vector space over a linearly ordered field: sub-convex combinations, the centroid, and the closed interiors of simplices given in an affine chart.

A convex set containing 0 also contains every combination ∑ i, w i • z i of its points with nonnegative weights of total at most 1, the missing weight being put on 0 (Convex.sum_mem_of_zero_mem). If the set is moreover symmetric, the coefficients may have any sign as long as their absolute values sum to at most 1 (Convex.sum_mem_of_sum_abs_le_one). In particular such a set contains the weighted cross-polytope {x | ∑ i, a i * |b.repr x i| ≤ 1} as soon as it contains each (a i)⁻¹ • b i for positive weights a i (Convex.weighted_crosspolytope_subset). This containment is the step in the lower bound of Minkowski's second theorem that places a cross-polytope spanned by vectors attaining the successive minima inside the body; its volume is OrthonormalBasis.volume_weighted_crosspolytope.

Over a linearly ordered field there is no topology to speak of relative interiors, but the centroid of a nonempty finite set s still behaves like a relative interior point of the convex hull of s: for every point p of the affine span of s, the point slightly beyond the centroid on the ray from p remains in the convex hull (Finset.exists_lineMap_centroid_mem_convexHull).

This is what makes a point outside a "visible" set lie off the affine span of every simplex in it, as used for cones of geometric simplicial complexes. It also shows that an affine map injective on the convex hull of a set is injective on its affine span (AffineMap.injOn_affineSpan_iff_injOn_convexHull), so it carries an affinely independent family to an affinely independent one as soon as it is injective on the convex hull of the family (AffineIndependent.map_of_injOn_convexHull). A map which agrees with an affine map on the convex hull of a set carries that hull onto the convex hull of the image (Set.EqOn.image_convexHull). These are what make the image of a simplex under a map affine on it, and injective on it, again a simplex.

The closed interior of a simplex is the convex hull of its vertices (Affine.Simplex.convexHull_eq_closedInterior). When the vertices are the images of points x i of a vector space under an injective affine map f, the closed interior is the image under f of the convex hull of the x i (Affine.Simplex.closedInterior_eq_image_convexHull, and Affine.Triangle.closedInterior_eq_image_convexHull for triangles), so questions about a simplex can be settled in coordinates. For instance, the closed interior of a simplex in an affine space contains the segment between any two of its points (Affine.Simplex.lineMap_mem_closedInterior). Over ℝ this means that a point moving linearly in the closed interior and a point moving linearly along a segment disjoint from it never meet, so their difference, when parallel to a fixed vector d, keeps its sign (Affine.Simplex.pos_iff_pos_of_disjoint). In coordinates, a bound f x ≤ w by a linear map f that holds at the vertices holds on the whole convex hull (IsLinearMap.le_of_mem_convexHull).

References

• J.-H. Evertse, Geometry of Numbers, §2.3, Lemma 2.10 and the lower-bound proof of Theorem 2.9, printed pp.26–27: https://pub.math.leidenuniv.nl/~evertsejh/dio19-2.pdf.

theorem IsLinearMap.le_of_mem_convexHull {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] [Module 𝕜 β] [PosSMulMono 𝕜 β] {f : E → β} (hf : IsLinearMap 𝕜 f) {s : Set E} {w : β} (hs : ∀ q ∈ s, f q ≤ w) {p : E} (hp : p ∈ (convexHull 𝕜) s) : f p ≤ w

A bound f q ≤ w by a linear map f that holds on a set s holds on its convex hull.

theorem Set.EqOn.image_convexHull {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {f : E → F} {g : E →ᵃ[𝕜] F} {s : Set E} (h : EqOn f (⇑g) ((convexHull 𝕜) s)) : f '' (convexHull 𝕜) s = (convexHull 𝕜) (f '' s)

A map which agrees with an affine map on the convex hull of a set s carries that convex hull onto the convex hull of the image of s.

theorem Convex.sum_mem_of_zero_mem {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (h₀ : 0 ∈ s) {t : Finset ι} {w : ι → 𝕜} {z : ι → E} (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hw₁ : ∑ i ∈ t, w i ≤ 1) (hz : ∀ i ∈ t, z i ∈ s) : ∑ i ∈ t, w i • z i ∈ s

A convex set containing 0 contains every combination of its points with nonnegative weights of total at most 1.

theorem Convex.sum_mem_of_sum_abs_le_one {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (h₀ : 0 ∈ s) (hneg : ∀ x ∈ s, -x ∈ s) {t : Finset ι} {c : ι → 𝕜} {z : ι → E} (hc : ∑ i ∈ t, |c i| ≤ 1) (hz : ∀ i ∈ t, z i ∈ s) : ∑ i ∈ t, c i • z i ∈ s

A convex set containing 0 and symmetric about it contains every combination of its points whose coefficients have absolute values of total at most 1.

theorem Convex.weighted_crosspolytope_subset {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} [Fintype ι] (hs : Convex 𝕜 s) (h₀ : 0 ∈ s) (hneg : ∀ x ∈ s, -x ∈ s) (b : Module.Basis ι 𝕜 E) {a : ι → 𝕜} (ha : ∀ (i : ι), 0 < a i) (hb : ∀ (i : ι), b i ∈ a i • s) : {x : E | ∑ i : ι, a i * |(b.repr x) i| ≤ 1} ⊆ s

A weighted cross-polytope inside a symmetric convex set. Let s be a convex set containing 0 and symmetric about it, b a basis and a positive weights with b i ∈ a i • s for every i. Then s contains the weighted cross-polytope {x | ∑ i, a i * |b.repr x i| ≤ 1}.

theorem Finset.exists_lineMap_centroid_mem_convexHull {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Finset E) {p : E} (hp : p ∈ affineSpan 𝕜 ↑s) : ∃ (ε : 𝕜), 0 < ε ∧ (AffineMap.lineMap p (centroid 𝕜 s id)) (1 + ε) ∈ (convexHull 𝕜) ↑s

For every point p in the affine span of a nonempty finite set s, some point strictly beyond the centroid of s on the ray from p still lies in the convex hull of s.

theorem AffineMap.eq_zero_of_injOn_convexHull {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {F : Type u_4} [AddCommGroup F] [Module 𝕜 F] (f : E →ᵃ[𝕜] F) {s : Set E} (hf : Set.InjOn (⇑f) ((convexHull 𝕜) s)) {v : E} (hv : v ∈ vectorSpan 𝕜 s) (hfv : f.linear v = 0) : v = 0

An affine map whose linear part kills a direction v of the affine span of a set s is not injective on the convex hull of s, unless v = 0.

theorem AffineMap.injOn_affineSpan_iff_injOn_convexHull {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {F : Type u_4} [AddCommGroup F] [Module 𝕜 F] (f : E →ᵃ[𝕜] F) (s : Set E) : Set.InjOn ⇑f ↑(affineSpan 𝕜 s) ↔ Set.InjOn (⇑f) ((convexHull 𝕜) s)

An affine map is injective on the affine span of a set as soon as it is injective on its convex hull.

theorem AffineIndependent.map_of_injOn_convexHull {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {F : Type u_4} [AddCommGroup F] [Module 𝕜 F] {p : ι → E} (hp : AffineIndependent 𝕜 p) (f : E →ᵃ[𝕜] F) (hf : Set.InjOn (⇑f) ((convexHull 𝕜) (Set.range p))) : AffineIndependent 𝕜 (⇑f ∘ p)

The image of an affinely independent family under an affine map is affinely independent as soon as the map is injective on the convex hull of the family.

theorem Affine.Simplex.closedInterior_eq_image_convexHull {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {V : Type u_4} {P : Type u_5} [AddCommGroup V] [Module 𝕜 V] [AddTorsor V P] {n : ℕ} (s : Simplex 𝕜 P n) {f : E →ᵃ[𝕜] P} {x : Fin (n + 1) → E} (hx : s.points = ⇑f ∘ x) : s.closedInterior = ⇑f '' (convexHull 𝕜) (Set.range x)

The closed interior of a simplex whose vertices are the images of points x i of a vector space under an affine map f is the image under f of the convex hull of the x i.

theorem Affine.Simplex.lineMap_mem_closedInterior {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {V : Type u_4} {P : Type u_5} [AddCommGroup V] [Module 𝕜 V] [AddTorsor V P] {n : ℕ} (s : Simplex 𝕜 P n) {x y : P} (hx : x ∈ s.closedInterior) (hy : y ∈ s.closedInterior) {t : 𝕜} (ht : t ∈ Set.Icc 0 1) : (AffineMap.lineMap x y) t ∈ s.closedInterior

The closed interior of a simplex in an affine space contains the segment between any two of its points.

theorem Affine.Simplex.pos_iff_pos_of_disjoint {V : Type u_4} {P : Type u_5} [AddCommGroup V] [Module ℝ V] [AddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) {p₁ p₂ x y x' y' : P} {d : V} (hdisj : ∀ z ∈ s.closedInterior, z ∉ affineSegment ℝ p₁ p₂) (hx : x ∈ s.closedInterior) (hy : y ∈ s.closedInterior) (hx' : x' ∈ affineSegment ℝ p₁ p₂) (hy' : y' ∈ affineSegment ℝ p₁ p₂) {h₀ h₁ : ℝ} (h₀d : h₀ • d = x -ᵥ x') (h₁d : h₁ • d = y -ᵥ y') : 0 < h₀ ↔ 0 < h₁

Heights over a segment disjoint from a simplex keep their sign. Let x, y be points of the closed interior of a real simplex and x', y' points of a segment disjoint from it, with x - x' = h₀ • d and y - y' = h₁ • d. Then h₀ and h₁ have the same sign: moving x to y and x' to y' linearly, the two moving points never meet, so their height h₀ + μ (h₁ - h₀) never vanishes.

theorem Affine.Triangle.closedInterior_eq_image_convexHull {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {V : Type u_4} {P : Type u_5} [AddCommGroup V] [Module 𝕜 V] [AddTorsor V P] (t : Triangle 𝕜 P) {f : E →ᵃ[𝕜] P} {x y z : E} (ht : t.points = ![f x, f y, f z]) : Simplex.closedInterior t = ⇑f '' (convexHull 𝕜) {x, y, z}

A triangle whose vertices are the images of x, y, z under an affine map f from a vector space has closed interior the image under f of the convex hull of x, y, z.