def IsConvexSet (n : ℕ) (C : Set (Fin n → ℝ)) : Prop

Definition 2.0.1. A subset C of Real^n is convex if (1 - λ) • x + λ • y ∈ C whenever x ∈ C, y ∈ C, and 0 < λ < 1.

Equations

• IsConvexSet n C = ∀ x ∈ C, ∀ y ∈ C, ∀ (t : ℝ), 0 < t → t < 1 → (1 - t) • x + t • y ∈ C

theorem isConvexSet_imp_convex (n : ℕ) (C : Set (Fin n → ℝ)) : IsConvexSet n C → Convex ℝ C

Convert the book's strict-parameter definition to mathlib's Convex.

theorem convex_imp_isConvexSet (n : ℕ) (C : Set (Fin n → ℝ)) : Convex ℝ C → IsConvexSet n C

Convert mathlib's Convex to the book's strict-parameter definition.

theorem isConvexSet_iff_convex (n : ℕ) (C : Set (Fin n → ℝ)) : IsConvexSet n C ↔ Convex ℝ C

The book's convexity definition is equivalent to mathlib's Convex for subsets of Real^n.

def lineSegment (n : ℕ) (x y : Fin n → ℝ) : Set (Fin n → ℝ)

Definition 2.0.2. The set {(1 - λ) • x + λ • y | 0 ≤ λ ≤ 1} is called the (closed) line segment between x and y.

Equations

• lineSegment n x y = segment ℝ x y

theorem lineSegment_eq_image (n : ℕ) (x y : Fin n → ℝ) : lineSegment n x y = (fun (t : ℝ) => (1 - t) • x + t • y) '' Set.Icc 0 1

The book's description of the line segment as an image of Icc (0:Real) 1 agrees with mathlib's segment.

def closedHalfSpaceLE (n : ℕ) (b : Fin n → ℝ) (β : ℝ) : Set (Fin n → ℝ)

Definition 2.0.3. For non-zero b ∈ Real^n and β ∈ Real, the set {x | ⟪x, b⟫ ≤ β} is a closed half-space.

Equations

• closedHalfSpaceLE n b β = {x : Fin n → ℝ | x ⬝ᵥ b ≤ β}

def closedHalfSpaceGE (n : ℕ) (b : Fin n → ℝ) (β : ℝ) : Set (Fin n → ℝ)

Definition 2.0.3. For non-zero b ∈ Real^n and β ∈ Real, the set {x | ⟪x, b⟫ ≥ β} is a closed half-space.

Equations

• closedHalfSpaceGE n b β = {x : Fin n → ℝ | x ⬝ᵥ b ≥ β}

def openHalfSpaceLT (n : ℕ) (b : Fin n → ℝ) (β : ℝ) : Set (Fin n → ℝ)

Definition 2.0.3. For non-zero b ∈ Real^n and β ∈ Real, the set {x | ⟪x, b⟫ < β} is an open half-space.

Equations

• openHalfSpaceLT n b β = {x : Fin n → ℝ | x ⬝ᵥ b < β}

def openHalfSpaceGT (n : ℕ) (b : Fin n → ℝ) (β : ℝ) : Set (Fin n → ℝ)

Definition 2.0.3. For non-zero b ∈ Real^n and β ∈ Real, the set {x | ⟪x, b⟫ > β} is an open half-space.

Equations

• openHalfSpaceGT n b β = {x : Fin n → ℝ | x ⬝ᵥ b > β}

theorem convex_iInter_family {ι : Sort u_1} (n : ℕ) (C : ι → Set (Fin n → ℝ)) (hC : ∀ (i : ι), Convex ℝ (C i)) : Convex ℝ (⋂ (i : ι), C i)

Theorem 2.1. The intersection of an arbitrary collection of convex sets is convex.

theorem isLinearMap_dotProduct_left (n : ℕ) (b : Fin n → ℝ) : IsLinearMap ℝ fun (x : Fin n → ℝ) => x ⬝ᵥ b

The dot product with a fixed vector is linear in the left argument.

theorem convex_dotProduct_le (n : ℕ) (b : Fin n → ℝ) (β : ℝ) : Convex ℝ {x : Fin n → ℝ | x ⬝ᵥ b ≤ β}

Each half-space defined by a dot product inequality is convex.

theorem convex_set_of_dotProduct_le {ι : Sort u_1} (n : ℕ) (b : ι → Fin n → ℝ) (β : ι → ℝ) : Convex ℝ {x : Fin n → ℝ | ∀ (i : ι), x ⬝ᵥ b i ≤ β i}

Corollary 2.1.1. For vectors b i ∈ Real^n and scalars β i ∈ Real indexed by an arbitrary set ι, the set C = {x | ⟪x, b i⟫ ≤ β i, ∀ i} is convex.

def IsPolyhedralConvexSet (n : ℕ) (C : Set (Fin n → ℝ)) : Prop

Definition 2.1.2. A set is a polyhedral convex set if it can be expressed as the intersection of finitely many closed half-spaces in Real^n.

Equations

• IsPolyhedralConvexSet n C = ∃ (ι : Type) (x : Fintype ι) (b : ι → Fin n → ℝ) (β : ι → ℝ), C = ⋂ (i : ι), closedHalfSpaceLE n (b i) (β i)

def IsConvexCombination (n m : ℕ) (x : Fin m → Fin n → ℝ) (y : Fin n → ℝ) : Prop

Definition 2.2.10. A vector sum λ₁ x₁ + ⋯ + λₘ xₘ is called a convex combination of x₁, ..., xₘ if λ i ≥ 0 for all i and λ₁ + ⋯ + λₘ = 1.

Equations

• IsConvexCombination n m x y = ∃ (w : Fin m → ℝ), (∀ (i : Fin m), 0 ≤ w i) ∧ ∑ i : Fin m, w i = 1 ∧ y = ∑ i : Fin m, w i • x i

theorem convex_mem_of_isConvexCombination (n : ℕ) (C : Set (Fin n → ℝ)) : Convex ℝ C → ∀ (m : ℕ) (x : Fin m → Fin n → ℝ) (y : Fin n → ℝ), (∀ (i : Fin m), x i ∈ C) → IsConvexCombination n m x y → y ∈ C

A convex set contains all finite convex combinations of its elements.

theorem isConvexCombination_two (n : ℕ) (x y : Fin n → ℝ) (a b : ℝ) : 0 ≤ a → 0 ≤ b → a + b = 1 → IsConvexCombination n 2 (fun (i : Fin 2) => if i = 0 then x else y) (a • x + b • y)

A two-point convex combination is an IsConvexCombination.

theorem convex_of_contains_convexCombinations (n : ℕ) (C : Set (Fin n → ℝ)) : (∀ (m : ℕ) (x : Fin m → Fin n → ℝ) (y : Fin n → ℝ), (∀ (i : Fin m), x i ∈ C) → IsConvexCombination n m x y → y ∈ C) → Convex ℝ C

If a set contains all finite convex combinations of its elements, then it is convex.

theorem convex_iff_contains_convex_combinations (n : ℕ) (C : Set (Fin n → ℝ)) : Convex ℝ C ↔ ∀ (m : ℕ) (x : Fin m → Fin n → ℝ) (y : Fin n → ℝ), (∀ (i : Fin m), x i ∈ C) → IsConvexCombination n m x y → y ∈ C

Theorem 2.2. A subset of Real^n is convex if and only if it contains all the convex combinations of its elements.

def convexHullIntersection (n : ℕ) (S : Set (Fin n → ℝ)) : Set (Fin n → ℝ)

Definition 2.3.10. The intersection of all convex sets containing a subset S ⊆ Real^n is called the convex hull of S and is denoted by conv S.

Equations

• convexHullIntersection n S = ⋂ (C : { C : Set (Fin n → ℝ) // S ⊆ C ∧ Convex ℝ C }), ↑C

theorem convexHullIntersection_eq_convexHull (n : ℕ) (S : Set (Fin n → ℝ)) : convexHullIntersection n S = (convexHull ℝ) S

The book's convex hull definition agrees with mathlib's convexHull.

theorem exists_fin_convexCombination_of_exists_fintype (n : ℕ) (S : Set (Fin n → ℝ)) (y : Fin n → ℝ) : (∃ (ι : Type) (x : Fintype ι) (w : ι → ℝ) (z : ι → Fin n → ℝ), (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ S) ∧ ∑ i : ι, w i • z i = y) → ∃ (m : ℕ) (x : Fin m → Fin n → ℝ), (∀ (i : Fin m), x i ∈ S) ∧ IsConvexCombination n m x y

Convert a Fintype-indexed convex combination into a Fin m-indexed one.

theorem mem_convexHull_iff_exists_fin_isConvexCombination (n : ℕ) (S : Set (Fin n → ℝ)) (y : Fin n → ℝ) : y ∈ (convexHull ℝ) S ↔ ∃ (m : ℕ) (x : Fin m → Fin n → ℝ), (∀ (i : Fin m), x i ∈ S) ∧ IsConvexCombination n m x y

Characterize membership in the convex hull via IsConvexCombination.

theorem convexHull_eq_setOf_convexCombination (n : ℕ) (S : Set (Fin n → ℝ)) : (convexHull ℝ) S = {y : Fin n → ℝ | ∃ (m : ℕ) (x : Fin m → Fin n → ℝ), (∀ (i : Fin m), x i ∈ S) ∧ IsConvexCombination n m x y}

Theorem 2.3. For any S ⊆ Real^n, conv S consists of all the convex combinations of the elements of S.

theorem range_choice_index {n m k : ℕ} (b : Fin (m + 1) → Fin n → ℝ) {x : Fin k → Fin n → ℝ} (hx : ∀ (i : Fin k), x i ∈ Set.range b) : ∃ (f : Fin k → Fin (m + 1)), ∀ (i : Fin k), x i = b (f i)

Choose indices witnessing membership in Set.range.

theorem weights_fiber_sum_eq {k m : ℕ} (f : Fin k → Fin (m + 1)) (w : Fin k → ℝ) (hw : ∀ (i : Fin k), 0 ≤ w i) : (∀ (j : Fin (m + 1)), 0 ≤ ∑ i : Fin k, if f i = j then w i else 0) ∧ (∑ j : Fin (m + 1), ∑ i : Fin k, if f i = j then w i else 0) = ∑ i : Fin k, w i

Summing weights over fibers preserves nonnegativity and total weight.

theorem weighted_sum_fiber_eq {n m k : ℕ} (b : Fin (m + 1) → Fin n → ℝ) (f : Fin k → Fin (m + 1)) (w : Fin k → ℝ) (x : Fin k → Fin n → ℝ) (hx : ∀ (i : Fin k), x i = b (f i)) : ∑ j : Fin (m + 1), (∑ i : Fin k, if f i = j then w i else 0) • b j = ∑ i : Fin k, w i • x i

Summing weights over fibers preserves the weighted sum.

theorem convexHull_range_eq_setOf_weighted_sum (n m : ℕ) (b : Fin (m + 1) → Fin n → ℝ) : (convexHull ℝ) (Set.range b) = {y : Fin n → ℝ | ∃ (w : Fin (m + 1) → ℝ), (∀ (i : Fin (m + 1)), 0 ≤ w i) ∧ ∑ i : Fin (m + 1), w i = 1 ∧ y = ∑ i : Fin (m + 1), w i • b i}

Corollary 2.3.1. The convex hull of a finite subset {b_0, ..., b_m} of Real^n consists of all vectors of the form λ_0 b_0 + ⋯ + λ_m b_m with λ_i ≥ 0 and λ_0 + ⋯ + λ_m = 1.

def IsPolytope (n : ℕ) (P : Set (Fin n → ℝ)) : Prop

Definition 2.3.11. A set which is the convex hull of finitely many points is called a polytope.

Equations

• IsPolytope n P = ∃ (S : Set (Fin n → ℝ)), S.Finite ∧ P = (convexHull ℝ) S

def IsSimplex (n m : ℕ) (P : Set (Fin n → ℝ)) : Prop

Definition 2.3.12. If {b_0, b_1, ..., b_m} is affinely independent, its convex hull is called an m-dimensional simplex and b_0, ..., b_m are the vertices of the simplex.

Equations

• IsSimplex n m P = ∃ (b : Fin (m + 1) → Fin n → ℝ), AffineIndependent ℝ b ∧ P = (convexHull ℝ) (Set.range b)

noncomputable def simplexBarycenter (n m : ℕ) (b : Fin (m + 1) → Fin n → ℝ) : Fin n → ℝ

Definition 2.3.13. For an m-dimensional simplex with vertices b_0, ..., b_m, the point λ_0 b_0 + ⋯ + λ_m b_m with λ_0 = ⋯ = λ_m = 1 / (m + 1) is called the midpoint or barycenter of the simplex.

Equations

• simplexBarycenter n m b = Finset.centroid ℝ Finset.univ b

noncomputable def convexSetDim (n : ℕ) (C : Set (Fin n → ℝ)) : ℕ

Definition 2.4.10. The dimension of a convex set C is the dimension of the affine hull of C.

Equations

• convexSetDim n C = Module.finrank ℝ ↥(affineSpan ℝ C).direction

theorem simplex_dim_le_convexSetDim (n : ℕ) (C : Set (Fin n → ℝ)) (m : ℕ) (P : Set (Fin n → ℝ)) : P ⊆ C → IsSimplex n m P → m ≤ convexSetDim n C

Any simplex contained in C has dimension at most convexSetDim n C.

theorem simplex_of_affineIndependent_finite (n : ℕ) (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) {t : Set (Fin n → ℝ)} (htC : t ⊆ C) (htind : AffineIndependent ℝ Subtype.val) {m : ℕ} [Fintype ↑t] (hcard : Fintype.card ↑t = m + 1) : ∃ P ⊆ C, IsSimplex n m P

Construct a simplex from a finite affinely independent subset of a convex set.

theorem exists_simplex_dim_convexSetDim (n : ℕ) (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) (hCne : C.Nonempty) : ∃ P ⊆ C, IsSimplex n (convexSetDim n C) P

A nonempty convex set contains a simplex of dimension convexSetDim.

theorem convexSetDim_isGreatest_simplex_dim (n : ℕ) (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) (hCne : C.Nonempty) : IsGreatest {m : ℕ | ∃ P ⊆ C, IsSimplex n m P} (convexSetDim n C)

Theorem 2.4. The dimension of a convex set C is the maximum of the dimensions of the simplices contained in C.

def IsConeSet (n : ℕ) (K : Set (Fin n → ℝ)) : Prop

Definition 2.5.9. A subset K of Real^n is a cone if it is closed under positive scalar multiplication, i.e. λ • x ∈ K when x ∈ K and λ > 0.

Equations

• IsConeSet n K = ∀ x ∈ K, ∀ (t : ℝ), 0 < t → t • x ∈ K

def IsConvexCone (n : ℕ) (K : Set (Fin n → ℝ)) : Prop

Definition 2.5.10. A convex cone is a cone which is also a convex set.

Equations

• IsConvexCone n K = (IsConeSet n K ∧ Convex ℝ K)

theorem IsConeSet_iInter_family {ι : Sort u_1} (n : ℕ) (K : ι → Set (Fin n → ℝ)) (hK : ∀ (i : ι), IsConeSet n (K i)) : IsConeSet n (⋂ (i : ι), K i)

The intersection of cone sets is a cone.

theorem convexCone_iInter_family {ι : Sort u_1} (n : ℕ) (K : ι → Set (Fin n → ℝ)) (hK : ∀ (i : ι), IsConvexCone n (K i)) : IsConvexCone n (⋂ (i : ι), K i)

Theorem 2.5. The intersection of an arbitrary collection of convex cones is a convex cone.

theorem IsConeSet_dotProduct_le_zero (n : ℕ) (b : Fin n → ℝ) : IsConeSet n {x : Fin n → ℝ | x ⬝ᵥ b ≤ 0}

A closed half-space through the origin is a cone.

theorem IsConvexCone_dotProduct_le_zero (n : ℕ) (b : Fin n → ℝ) : IsConvexCone n {x : Fin n → ℝ | x ⬝ᵥ b ≤ 0}

A closed half-space through the origin is a convex cone.

theorem iInter_setOf_dotProduct_le_zero {ι : Sort u_1} (n : ℕ) (b : ι → Fin n → ℝ) : ⋂ (i : ι), {x : Fin n → ℝ | x ⬝ᵥ b i ≤ 0} = {x : Fin n → ℝ | ∀ (i : ι), x ⬝ᵥ b i ≤ 0}

Intersections of dot-product half-spaces encode pointwise inequalities.

theorem convexCone_of_dotProduct_le_zero {ι : Sort u_1} (n : ℕ) (b : ι → Fin n → ℝ) : IsConvexCone n {x : Fin n → ℝ | ∀ (i : ι), x ⬝ᵥ b i ≤ 0}

Corollary 2.5.1. Let b i ∈ Real^n for i ∈ I, where I is an arbitrary index set. Then K = {x ∈ Real^n | ⟪x, b i⟫ ≤ 0, i ∈ I} is a convex cone.

def nonNegativeOrthant (n : ℕ) : Set (Fin n → ℝ)

Definition 2.5.11. The non-negative orthant of Real^n is the set of vectors x = (xi_1, ..., xi_n) with xi_i ≥ 0 for all coordinates.

Equations

• nonNegativeOrthant n = {x : Fin n → ℝ | ∀ (i : Fin n), 0 ≤ x i}

def positiveOrthant (n : ℕ) : Set (Fin n → ℝ)

Definition 2.5.12. The positive orthant of Real^n is the set of vectors x = (xi_1, ..., xi_n) with xi_i > 0 for all coordinates.

Equations

• positiveOrthant n = {x : Fin n → ℝ | ∀ (i : Fin n), 0 < x i}

def coordwiseGE (n : ℕ) (x x' : Fin n → ℝ) : Prop

Definition 2.5.13. It is customary to write x ≥ x' if x - x' belongs to the non-negative orthant, i.e. if ξ_j ≥ ξ'_j for j = 1, ..., n.

Equations

• coordwiseGE n x x' = (x - x' ∈ nonNegativeOrthant n)

theorem coordwiseGE_iff_le (n : ℕ) (x x' : Fin n → ℝ) : coordwiseGE n x x' ↔ x' ≤ x

The book's coordinatewise order agrees with the pointwise order on Fin n → Real.

theorem isConvexCone_add_closed (n : ℕ) (K : Set (Fin n → ℝ)) : IsConvexCone n K → ∀ x ∈ K, ∀ y ∈ K, x + y ∈ K

A convex cone is closed under addition.

theorem pos_combo_mem_of_add_closed_and_pos_smul_closed (n : ℕ) (K : Set (Fin n → ℝ)) (hadd : ∀ x ∈ K, ∀ y ∈ K, x + y ∈ K) (hsmul : ∀ x ∈ K, ∀ (t : ℝ), 0 < t → t • x ∈ K) (x : Fin n → ℝ) : x ∈ K → ∀ y ∈ K, ∀ (a b : ℝ), 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ K

Positive scalar closure and add-closure give two-point positive combinations.

theorem convex_of_add_closed_and_pos_smul_closed (n : ℕ) (K : Set (Fin n → ℝ)) (hadd : ∀ x ∈ K, ∀ y ∈ K, x + y ∈ K) (hsmul : ∀ x ∈ K, ∀ (t : ℝ), 0 < t → t • x ∈ K) : Convex ℝ K

Add-closure and positive scalar closure imply convexity.

theorem isConvexCone_iff_add_closed_and_pos_smul_closed (n : ℕ) (K : Set (Fin n → ℝ)) : IsConvexCone n K ↔ (∀ x ∈ K, ∀ y ∈ K, x + y ∈ K) ∧ ∀ x ∈ K, ∀ (t : ℝ), 0 < t → t • x ∈ K

Theorem 2.6. A subset of Real^n is a convex cone if and only if it is closed under addition and positive scalar multiplication.

theorem pos_linear_combo_mem_of_add_closed_and_pos_smul_closed (n : ℕ) (K : Set (Fin n → ℝ)) (hadd : ∀ x ∈ K, ∀ y ∈ K, x + y ∈ K) (hsmul : ∀ x ∈ K, ∀ (t : ℝ), 0 < t → t • x ∈ K) (m : ℕ) (x : Fin (m + 1) → Fin n → ℝ) (w : Fin (m + 1) → ℝ) : (∀ (i : Fin (m + 1)), x i ∈ K) → (∀ (i : Fin (m + 1)), 0 < w i) → ∑ i : Fin (m + 1), w i • x i ∈ K

Finite positive linear combinations from add-closure and positive scalar closure.

theorem pos_smul_closed_of_pos_linear_combinations (n : ℕ) (K : Set (Fin n → ℝ)) (hcomb : ∀ (m : ℕ) (x : Fin (m + 1) → Fin n → ℝ) (w : Fin (m + 1) → ℝ), (∀ (i : Fin (m + 1)), x i ∈ K) → (∀ (i : Fin (m + 1)), 0 < w i) → ∑ i : Fin (m + 1), w i • x i ∈ K) (x : Fin n → ℝ) : x ∈ K → ∀ (t : ℝ), 0 < t → t • x ∈ K

Positive scaling follows from closure under positive linear combinations.

theorem add_closed_of_pos_linear_combinations (n : ℕ) (K : Set (Fin n → ℝ)) (hcomb : ∀ (m : ℕ) (x : Fin (m + 1) → Fin n → ℝ) (w : Fin (m + 1) → ℝ), (∀ (i : Fin (m + 1)), x i ∈ K) → (∀ (i : Fin (m + 1)), 0 < w i) → ∑ i : Fin (m + 1), w i • x i ∈ K) (x : Fin n → ℝ) : x ∈ K → ∀ y ∈ K, x + y ∈ K

Add-closure follows from closure under positive linear combinations.

theorem isConvexCone_iff_contains_pos_linear_combinations (n : ℕ) (K : Set (Fin n → ℝ)) : IsConvexCone n K ↔ ∀ (m : ℕ) (x : Fin (m + 1) → Fin n → ℝ) (w : Fin (m + 1) → ℝ), (∀ (i : Fin (m + 1)), x i ∈ K) → (∀ (i : Fin (m + 1)), 0 < w i) → ∑ i : Fin (m + 1), w i • x i ∈ K

Corollary 2.6.1. A subset of Real^n is a convex cone if and only if it contains all the positive linear combinations of its elements, i.e. sums λ₁ x₁ + ⋯ + λ_m x_m with λ_i > 0.

def IsPosLinearCombination (n : ℕ) (S : Set (Fin n → ℝ)) (y : Fin n → ℝ) : Prop

A point is a positive linear combination of elements of a set.

Equations

• IsPosLinearCombination n S y = ∃ (m : ℕ) (x : Fin (m + 1) → Fin n → ℝ) (w : Fin (m + 1) → ℝ), (∀ (i : Fin (m + 1)), x i ∈ S) ∧ (∀ (i : Fin (m + 1)), 0 < w i) ∧ y = ∑ i : Fin (m + 1), w i • x i

theorem isPosLinearCombination_smul (n : ℕ) (S : Set (Fin n → ℝ)) {y : Fin n → ℝ} (hy : IsPosLinearCombination n S y) {t : ℝ} (ht : 0 < t) : IsPosLinearCombination n S (t • y)

Positive linear combinations are closed under positive scaling.

theorem isPosLinearCombination_add (n : ℕ) (S : Set (Fin n → ℝ)) {y₁ y₂ : Fin n → ℝ} (hy₁ : IsPosLinearCombination n S y₁) (hy₂ : IsPosLinearCombination n S y₂) : IsPosLinearCombination n S (y₁ + y₂)

The sum of two positive linear combinations is a positive linear combination.

theorem positiveLinearCombinationCone_isSmallest (n : ℕ) (S : Set (Fin n → ℝ)) : have K := {y : Fin n → ℝ | ∃ (m : ℕ) (x : Fin (m + 1) → Fin n → ℝ) (w : Fin (m + 1) → ℝ), (∀ (i : Fin (m + 1)), x i ∈ S) ∧ (∀ (i : Fin (m + 1)), 0 < w i) ∧ y = ∑ i : Fin (m + 1), w i • x i}; IsConvexCone n K ∧ S ⊆ K ∧ ∀ (K' : Set (Fin n → ℝ)), IsConvexCone n K' → S ⊆ K' → K ⊆ K'

Corollary 2.6.2. Let S ⊆ Real^n, and let K be the set of all positive linear combinations of elements of S. Then K is the smallest convex cone containing S.

theorem positiveScalarCone_isSmallest (n : ℕ) (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) : have K := {y : Fin n → ℝ | ∃ x ∈ C, ∃ (t : ℝ), 0 < t ∧ y = t • x}; IsConvexCone n K ∧ C ⊆ K ∧ ∀ (K' : Set (Fin n → ℝ)), IsConvexCone n K' → C ⊆ K' → K ⊆ K'

Corollary 2.6.3. Let C be a convex set, and let K = {λ • x | λ > 0, x ∈ C}. Then K is the smallest convex cone which includes C.

def convexConeGenerated (n : ℕ) (S : Set (Fin n → ℝ)) : Set (Fin n → ℝ)

Definition 2.6.10. The convex cone obtained by adjoining the origin to the cone in Corollary 2.6.2 (equivalently, Corollary 2.6.3) is called the convex cone generated by S (or by a convex set C) and is denoted cone S.

Equations

• convexConeGenerated n S = Set.insert 0 ↑(ConvexCone.hull ℝ S)

def rayNonneg (n : ℕ) (S : Set (Fin n → ℝ)) : Set (Fin n → ℝ)

The nonnegative ray generated by a set.

Equations

• rayNonneg n S = {y : Fin n → ℝ | ∃ x ∈ S, ∃ (t : ℝ), 0 ≤ t ∧ y = t • x}

theorem rayNonneg_subset_convexConeGenerated (n : ℕ) (S : Set (Fin n → ℝ)) : rayNonneg n S ⊆ convexConeGenerated n S

Elements of the nonnegative ray lie in the generated cone.

theorem convexConeGenerated_convex (n : ℕ) (S : Set (Fin n → ℝ)) : Convex ℝ (convexConeGenerated n S)

The generated cone is convex.