theorem closure_convexHull_iUnion_eq_iUnion_weighted_sum_and_recessionCone {n m : ℕ} (C : Fin m → Set (EuclideanSpace ℝ (Fin n))) (hCne : ∀ (i : Fin m), (C i).Nonempty) (hCclosed : ∀ (i : Fin m), IsClosed (C i)) (hCconv : ∀ (i : Fin m), Convex ℝ (C i)) (hlineal : ∀ (z : Fin m → EuclideanSpace ℝ (Fin n)), (∀ (i : Fin m), z i ∈ (C i).recessionCone) → ∑ i : Fin m, z i = 0 → ∀ (i : Fin m), z i ∈ (C i).linealitySpace) (hm : 0 < m) : have C0 := (convexHull ℝ) (⋃ (i : Fin m), C i); (closure C0 = ⋃ (lam : Fin m → ℝ), ⋃ (_ : (∀ (i : Fin m), 0 ≤ lam i) ∧ ∑ i : Fin m, lam i = 1), ∑ i : Fin m, if lam i = 0 then (C i).recessionCone else lam i • C i) ∧ (closure C0).recessionCone = ∑ i : Fin m, (C i).recessionCone

Theorem 9.8. Let C1, ..., Cm be nonempty closed convex sets in ℝ^n such that whenever z1, ..., zm satisfy zi ∈ 0^+ Ci and z1 + ... + zm = 0, each zi lies in the lineality space of Ci. Let C = conv (C1 ∪ ... ∪ Cm). Then cl C = ⋃ {lam1 C1 + ... + lamm Cm | lam_i ≥ 0^+, lam1 + ... + lamm = 1}, where lam_i ≥ 0^+ means lam_i Ci is interpreted as 0^+ Ci when lam_i = 0. Moreover, 0^+ (cl C) = 0^+ C1 + ... + 0^+ Cm.

theorem recessionCone_sum_mem_finset {n m : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCconv : Convex ℝ C) {s : Finset (Fin m)} (z : Fin m → EuclideanSpace ℝ (Fin n)) (hz : ∀ i ∈ s, z i ∈ C.recessionCone) : ∑ i ∈ s, z i ∈ C.recessionCone

Finite sums of recession cone elements stay in the recession cone.

theorem linealitySpace_of_sum_zero_same_recession {n m : ℕ} (C : Fin m → Set (EuclideanSpace ℝ (Fin n))) (K : Set (EuclideanSpace ℝ (Fin n))) (hCconv : ∀ (i : Fin m), Convex ℝ (C i)) (hK : ∀ (i : Fin m), (C i).recessionCone = K) (z : Fin m → EuclideanSpace ℝ (Fin n)) : (∀ (i : Fin m), z i ∈ K) → ∑ i : Fin m, z i = 0 → ∀ (i : Fin m), z i ∈ (C i).linealitySpace

Zero-sum vectors in a common recession cone give lineality directions.

theorem absorb_recessionCone_into_positive_weight {n : ℕ} {C K : Set (EuclideanSpace ℝ (Fin n))} (hK : C.recessionCone = K) {t : ℝ} (ht : 0 < t) : K + t • C = t • C

A positive weight absorbs the recession cone.

theorem weighted_sum_subset_convexHull {n m : ℕ} (C : Fin m → Set (EuclideanSpace ℝ (Fin n))) {lam : Fin m → ℝ} (hlam : ∀ (i : Fin m), 0 ≤ lam i) (hsum : ∑ i : Fin m, lam i = 1) : ∑ i : Fin m, lam i • C i ⊆ (convexHull ℝ) (⋃ (i : Fin m), C i)

Weighted Minkowski sums lie in the convex hull of the union.

theorem mem_sum_if_recessionCone {n m : ℕ} (C : Fin m → Set (EuclideanSpace ℝ (Fin n))) (K : Set (EuclideanSpace ℝ (Fin n))) (hCne : ∀ (i : Fin m), (C i).Nonempty) (hCconv : ∀ (i : Fin m), Convex ℝ (C i)) (hK : ∀ (i : Fin m), (C i).recessionCone = K) {lam : Fin m → ℝ} (hlam : ∀ (i : Fin m), 0 ≤ lam i) (hsum : ∑ i : Fin m, lam i = 1) {x : EuclideanSpace ℝ (Fin n)} (hx : x ∈ ∑ i : Fin m, if lam i = 0 then K else lam i • C i) : x ∈ ∑ i : Fin m, lam i • C i

A weighted recession-cone sum can be reduced to the usual weighted sum.

theorem sum_recessionCone_eq_K {n m : ℕ} (C : Fin m → Set (EuclideanSpace ℝ (Fin n))) (K : Set (EuclideanSpace ℝ (Fin n))) (hCconv : ∀ (i : Fin m), Convex ℝ (C i)) (hK : ∀ (i : Fin m), (C i).recessionCone = K) (hm : 0 < m) : ∑ i : Fin m, (C i).recessionCone = K

The sum of a nonempty family of equal recession cones is the cone.

theorem convexHull_iUnion_closed_and_recessionCone_eq {n m : ℕ} (C : Fin m → Set (EuclideanSpace ℝ (Fin n))) (K : Set (EuclideanSpace ℝ (Fin n))) (hCne : ∀ (i : Fin m), (C i).Nonempty) (hCclosed : ∀ (i : Fin m), IsClosed (C i)) (hCconv : ∀ (i : Fin m), Convex ℝ (C i)) (hK : ∀ (i : Fin m), (C i).recessionCone = K) (hm : 0 < m) : have C0 := (convexHull ℝ) (⋃ (i : Fin m), C i); IsClosed C0 ∧ C0.recessionCone = K

Corollary 9.8.1. If C1, ..., Cm are nonempty closed convex sets in ℝ^n all having the same recession cone K, then C = conv (C1 ∪ ... ∪ Cm) is closed and has K as its recession cone.

theorem iUnion_replace_empty_eq {n m : ℕ} (C : Fin m → Set (EuclideanSpace ℝ (Fin n))) (i0 : Fin m) [DecidablePred fun (i : Fin m) => (C i).Nonempty] : (⋃ (i : Fin m), if (C i).Nonempty then C i else C i0) = ⋃ (i : Fin m), C i

Replace empty members of a finite family by a fixed set without changing the union.

theorem recessionCone_eq_singleton_zero_of_bounded {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hCbdd : Bornology.IsBounded C) : C.recessionCone = {0}

Bounded closed convex sets have recession cone {0}.

theorem convexHull_iUnion_nonempty {n m : ℕ} (C : Fin m → Set (EuclideanSpace ℝ (Fin n))) (hne : ∃ (i : Fin m), (C i).Nonempty) : ((convexHull ℝ) (⋃ (i : Fin m), C i)).Nonempty

If some member of a finite family is nonempty, the convex hull of the union is nonempty.

theorem convexHull_iUnion_closed_and_bounded {n m : ℕ} (C : Fin m → Set (EuclideanSpace ℝ (Fin n))) (hCclosed : ∀ (i : Fin m), IsClosed (C i)) (hCbdd : ∀ (i : Fin m), Bornology.IsBounded (C i)) (hCconv : ∀ (i : Fin m), Convex ℝ (C i)) : IsClosed ((convexHull ℝ) (⋃ (i : Fin m), C i)) ∧ Bornology.IsBounded ((convexHull ℝ) (⋃ (i : Fin m), C i))

Corollary 9.8.2 9.8.2.1. If C1, ..., Cm are closed bounded convex sets in ℝ^n, then conv (C1 ∪ ... ∪ Cm) is closed and bounded.

theorem epigraph_family_closed_convex_nonempty {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} (hclosed : ∀ (i : Fin m), ClosedConvexFunction (f i)) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (i : Fin m) : (epigraph Set.univ (f i)).Nonempty ∧ IsClosed (epigraph Set.univ (f i)) ∧ Convex ℝ (epigraph Set.univ (f i))

Closed proper convex functions have closed, convex, nonempty epigraphs.

theorem convexHull_union_epigraph_subset_epigraph_of_minorant {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} {h : (Fin n → ℝ) → EReal} (hh : ConvexFunctionOn Set.univ h) (hle : ∀ (i : Fin m), h ≤ f i) : (convexHull ℝ) (⋃ (i : Fin m), epigraph Set.univ (f i)) ⊆ epigraph Set.univ h

The convex hull of a union of epigraphs lies in the epigraph of any convex minorant.

theorem recessionCone_epigraph_eq_epigraph_k {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} {k : (Fin n → ℝ) → EReal} (hconv : ∀ (i : Fin m), Convex ℝ (epigraph Set.univ (f i))) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hk : ∀ (i : Fin m) (y : Fin n → ℝ), k y = sSup {r : EReal | ∃ (x : Fin n → ℝ), r = f i (x + y) - f i x}) (i : Fin m) : (epigraph Set.univ (f i)).recessionCone = epigraph Set.univ k

Recession cones of the epigraph family agree with the common recession function.

theorem convexHull_union_epigraph_closed_recession_prod {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} {k : (Fin n → ℝ) → EReal} (hclosed : ∀ (i : Fin m), ClosedConvexFunction (f i)) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hk : ∀ (i : Fin m) (y : Fin n → ℝ), k y = sSup {r : EReal | ∃ (x : Fin n → ℝ), r = f i (x + y) - f i x}) (hm : 0 < m) : have C0 := (convexHull ℝ) (⋃ (i : Fin m), epigraph Set.univ (f i)); IsClosed C0 ∧ C0.recessionCone = epigraph Set.univ k

Closedness and recession cone of the convex hull of a finite epigraph family in product space.