theorem exists_nonnegLinearCombination_of_sum_smul_mem_ray_ne_zero_terms {n ℓ : ℕ} {T : Set (Fin n → ℝ)} (d : Fin ℓ → Fin n → ℝ) (b : Fin ℓ → ℝ) (hd : ∀ (j : Fin ℓ), d j ∈ ray n T) (hb : ∀ (j : Fin ℓ), 0 ≤ b j) : ∃ r ≤ ℓ, ∃ (y : Fin r → Fin n → ℝ) (c : Fin r → ℝ), (∀ (i : Fin r), y i ∈ T) ∧ (∀ (i : Fin r), 0 ≤ c i) ∧ ∑ j : Fin ℓ, b j • d j = ∑ i : Fin r, c i • y i

A nonnegative linear combination of ray elements comes from a nonnegative combination in T.

theorem pad_nonnegLinearCombination_to_fixed_length {n r m : ℕ} {T : Set (Fin n → ℝ)} (hT : T.Nonempty) {x : Fin n → ℝ} (y : Fin r → Fin n → ℝ) (c : Fin r → ℝ) (hy : ∀ (i : Fin r), y i ∈ T) (hc : ∀ (i : Fin r), 0 ≤ c i) (hx : x = ∑ i : Fin r, c i • y i) (hr : r ≤ m - 1) : ∃ (y' : Fin (m - 1) → Fin n → ℝ) (c' : Fin (m - 1) → ℝ), (∀ (j : Fin (m - 1)), y' j ∈ T) ∧ (∀ (j : Fin (m - 1)), 0 ≤ c' j) ∧ x = ∑ j : Fin (m - 1), c' j • y' j

Pad a nonnegative linear combination to a fixed length using zero coefficients.

theorem convexConeGenerated_eq_mixedConvexHull_singleton_zero {n : ℕ} (T : Set (Fin n → ℝ)) : convexConeGenerated n T = mixedConvexHull {0} T

Proposition 17.0.11 (Cone as a mixed convex hull), LaTeX label prop:cone-as-mixed.

Let T ⊆ ℝⁿ. The convex cone generated by T can be viewed as the mixed convex hull with point-set {0} and direction-set T.

Moreover, a mixed convex combination of m elements of this mixed set is necessarily a combination of 0 and m-1 directions; hence it can be written as a nonnegative linear combination of m-1 vectors in T.

theorem isMixedConvexCombination_singleton_zero_imp_exists_nonnegLinearCombination {n m : ℕ} (T : Set (Fin n → ℝ)) (x : Fin n → ℝ) (hT : T.Nonempty) : IsMixedConvexCombination n m {0} T x → ∃ (y : Fin (m - 1) → Fin n → ℝ) (c : Fin (m - 1) → ℝ), (∀ (j : Fin (m - 1)), y j ∈ T) ∧ (∀ (j : Fin (m - 1)), 0 ≤ c j) ∧ x = ∑ j : Fin (m - 1), c j • y j

Proposition 17.0.11 (Cone as a mixed convex hull), LaTeX label prop:cone-as-mixed, part 2: when the point-set is {0}, a mixed convex combination reduces to a nonnegative linear combination of vectors from T.

def mixedAffineHull {n : ℕ} (S₀ S₁ : Set (Fin n → ℝ)) : Set (Fin n → ℝ)

Definition 17.0.12 (Affine hull of a mixed set), LaTeX label def:affine-hull. Let S = S₀ ∪ S₁ be a mixed set consisting of points S₀ ⊆ ℝⁿ and directions S₁ ⊆ ℝⁿ. Define aff S := aff (conv S); in other words, the affine hull of a mixed set is the affine hull of its (mixed) convex hull, i.e. the smallest affine set containing all points of S and receding in all directions of S.

If S contains directions only (i.e. S₀ = ∅), then conv S = aff S = ∅.

Equations

• mixedAffineHull S₀ S₁ = ↑(affineSpan ℝ (mixedConvexHull S₀ S₁))

theorem mixedConvexHull_empty_points {n : ℕ} (S₁ : Set (Fin n → ℝ)) : mixedConvexHull ∅ S₁ = ∅

Definition 17.0.12 (Affine hull of a mixed set), direction-only case: if there are no points, then the mixed convex hull is empty.

theorem affineSpan_empty_set {n : ℕ} : ↑(affineSpan ℝ ∅) = ∅

The affine span of the empty set is empty.

theorem mixedAffineHull_empty_points {n : ℕ} (S₁ : Set (Fin n → ℝ)) : mixedAffineHull ∅ S₁ = ∅

Definition 17.0.12 (Affine hull of a mixed set), direction-only case: if there are no points, then the mixed affine hull is empty.

def IsMixedAffinelyIndependent {n : ℕ} (S₀ S₁ : Finset (Fin n → ℝ)) : Prop

Definition 17.0.13 (Affine independence for mixed sets), LaTeX label def:aff-indep.

Let S contain m total elements (points and directions). We say that S is affinely independent if dim(aff S) = m - 1, where aff S is the affine hull of the mixed set (Definition 17.0.12).

For nonempty S, this means S contains at least one point and the lifted vectors (1, x₁), …, (1, xₖ), (0, xₖ₊₁), …, (0, xₘ) are linearly independent in ℝ^{n+1}, where x₁, …, xₖ are the points in S and xₖ₊₁, …, xₘ represent the distinct directions in S.

Equations

• IsMixedAffinelyIndependent S₀ S₁ = (Module.finrank ℝ ↥(affineSpan ℝ (mixedConvexHull ↑S₀ ↑S₁)).direction = S₀.card + S₁.card - 1)