theorem sum_cones_subset_K0 (n m : ℕ) (C : Fin m.succ → Set (EuclideanSpace ℝ (Fin n))) : have C0 := (convexHull ℝ) (⋃ (i : Fin m.succ), C i); have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ); have first := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords v 0; have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => (EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i); have S0 := {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ C0}; have K0 := ↑(ConvexCone.hull ℝ S0); have S := fun (i : Fin m.succ) => {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ C i}; have K := fun (i : Fin m.succ) => ↑(ConvexCone.hull ℝ (S i)); ∑ i : Fin m.succ, K i ⊆ K0

The Minkowski sum of the lifted cones lies in the cone over the convex hull.

theorem S0_subset_closure_sum_cones (n m : ℕ) (C : Fin m.succ → Set (EuclideanSpace ℝ (Fin n))) (hCne : ∀ (i : Fin m.succ), (C i).Nonempty) (hCconv : ∀ (i : Fin m.succ), Convex ℝ (C i)) : have C0 := (convexHull ℝ) (⋃ (i : Fin m.succ), C i); have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ); have first := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords v 0; have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => (EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i); have S0 := {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ C0}; have S := fun (i : Fin m.succ) => {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ C i}; have K := fun (i : Fin m.succ) => ↑(ConvexCone.hull ℝ (S i)); S0 ⊆ closure (∑ i : Fin m.succ, K i)

Base points of the cone over C0 lie in the closure of the sum of cones.

theorem K0_subset_closure_sum_cones (n m : ℕ) (C : Fin m.succ → Set (EuclideanSpace ℝ (Fin n))) (hCne : ∀ (i : Fin m.succ), (C i).Nonempty) (hCconv : ∀ (i : Fin m.succ), Convex ℝ (C i)) : have C0 := (convexHull ℝ) (⋃ (i : Fin m.succ), C i); have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ); have first := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords v 0; have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => (EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i); have S0 := {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ C0}; have K0 := ↑(ConvexCone.hull ℝ S0); have S := fun (i : Fin m.succ) => {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ C i}; have K := fun (i : Fin m.succ) => ↑(ConvexCone.hull ℝ (S i)); K0 ⊆ closure (∑ i : Fin m.succ, K i)

The lifted cone over C0 lies in the closure of the sum of cones.

theorem euclideanRelativeInterior_convexHull_iUnion_eq (n m : ℕ) (C : Fin m → Set (EuclideanSpace ℝ (Fin n))) (hCne : ∀ (i : Fin m), (C i).Nonempty) (hCconv : ∀ (i : Fin m), Convex ℝ (C i)) : euclideanRelativeInterior n ((convexHull ℝ) (⋃ (i : Fin m), C i)) = {x : EuclideanSpace ℝ (Fin n) | ∃ (w : Fin m → ℝ) (x_i : Fin m → EuclideanSpace ℝ (Fin n)), (∀ (i : Fin m), 0 < w i) ∧ ∑ i : Fin m, w i = 1 ∧ (∀ (i : Fin m), x_i i ∈ euclideanRelativeInterior n (C i)) ∧ x = ∑ i : Fin m, w i • x_i i}

Theorem 6.9: Let C_1, ..., C_m be non-empty convex sets in R^n, and let C_0 = conv (C_1 ∪ ... ∪ C_m). Then ri C_0 = ⋃ {λ_1 ri C_1 + ... + λ_m ri C_m | λ_i > 0, λ_1 + ... + λ_m = 1}.

theorem tail_linearMap_apply (n : ℕ) : have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ); have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => (EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i); have A := LinearMap.snd ℝ (EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin n)) ∘ₗ ↑(appendAffineEquiv 1 n).symm.linear; ∀ (v : EuclideanSpace ℝ (Fin (1 + n))), A v = tail v

The tail projection agrees with the linear map obtained from appendAffineEquiv.

theorem tail_image_cone_eq_convexCone_hull (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) : have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ); have first := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords v 0; have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => (EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i); have S := {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ C}; have K := ↑(ConvexCone.hull ℝ S); have A := LinearMap.snd ℝ (EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin n)) ∘ₗ ↑(appendAffineEquiv 1 n).symm.linear; ⇑A '' K = ↑(ConvexCone.hull ℝ C)

The tail projection of the lifted cone equals the cone generated by C.

theorem tail_image_ri_cone_eq_smul_ri (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) (hCne : C.Nonempty) : have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ); have first := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords v 0; have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => (EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i); have S := {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ C}; have K := ↑(ConvexCone.hull ℝ S); have A := LinearMap.snd ℝ (EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin n)) ∘ₗ ↑(appendAffineEquiv 1 n).symm.linear; ⇑A '' euclideanRelativeInterior (1 + n) K = {v : EuclideanSpace ℝ (Fin n) | ∃ (r : ℝ), 0 < r ∧ ∃ x ∈ euclideanRelativeInterior n C, v = r • x}

The tail projection of the relative interior gives positive scalings of ri C.

theorem euclideanRelativeInterior_convexConeGenerated_eq_smul (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) (hCne : C.Nonempty) : have K := ↑(ConvexCone.hull ℝ C); euclideanRelativeInterior n K = {v : EuclideanSpace ℝ (Fin n) | ∃ (r : ℝ), 0 < r ∧ ∃ x ∈ euclideanRelativeInterior n C, v = r • x}

Text 6.19: More generally, the relative interior of the convex cone in R^n generated by a non-empty convex set C consists of the vectors of the form λ x with λ > 0 and x ∈ ri C.

theorem smul_convexCone_eq_self (n : ℕ) (K : ConvexCone ℝ (EuclideanSpace ℝ (Fin n))) (r : ℝ) (hr : 0 < r) : r • ↑K = ↑K

A convex cone is invariant under positive scalar multiplication.

theorem convexCone_of_convex_smul_invariant (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) (hsmul : ∀ (r : ℝ), 0 < r → r • C = C) : ∃ (K' : ConvexCone ℝ (EuclideanSpace ℝ (Fin n))), ↑K' = C

A convex set invariant under positive scalings is a convex cone.

theorem ri_smul_invariant_of_cone (n : ℕ) (K : ConvexCone ℝ (EuclideanSpace ℝ (Fin n))) (r : ℝ) (hr : 0 < r) : r • euclideanRelativeInterior n ↑K = euclideanRelativeInterior n ↑K

The relative interior of a convex cone is invariant under positive scalings.

theorem euclideanRelativeInterior_and_closure_convexCone (n : ℕ) (K : ConvexCone ℝ (EuclideanSpace ℝ (Fin n))) : (∃ (K' : ConvexCone ℝ (EuclideanSpace ℝ (Fin n))), ↑K' = euclideanRelativeInterior n ↑K) ∧ ∃ (K' : ConvexCone ℝ (EuclideanSpace ℝ (Fin n))), ↑K' = closure ↑K

Text 6.20: The relative interior and the closure of a convex cone are convex cones.