theorem smul_rayNonneg_subset (n : ℕ) (S : Set (Fin n → ℝ)) {t : ℝ} (ht : 0 < t) : t • rayNonneg n S ⊆ rayNonneg n S

Positive scaling sends the nonnegative ray into itself.

theorem convexHull_rayNonneg_smul_closed (n : ℕ) (S : Set (Fin n → ℝ)) (x : Fin n → ℝ) : x ∈ (convexHull ℝ) (rayNonneg n S) → ∀ (t : ℝ), 0 < t → t • x ∈ (convexHull ℝ) (rayNonneg n S)

The convex hull of the ray is closed under positive scaling.

theorem convexHull_rayNonneg_add_closed (n : ℕ) (S : Set (Fin n → ℝ)) (x : Fin n → ℝ) : x ∈ (convexHull ℝ) (rayNonneg n S) → ∀ y ∈ (convexHull ℝ) (rayNonneg n S), x + y ∈ (convexHull ℝ) (rayNonneg n S)

The convex hull of the ray is closed under addition.

theorem convexConeGenerated_eq_convexHull_ray (n : ℕ) (S : Set (Fin n → ℝ)) (hS : S.Nonempty) : convexConeGenerated n S = (convexHull ℝ) {y : Fin n → ℝ | ∃ x ∈ S, ∃ (t : ℝ), 0 ≤ t ∧ y = t • x}

Corollary 2.6.11. For any nonempty subset S ⊆ Real^n, the convex cone generated by S satisfies cone S = conv (ray S).

theorem convexCone_smallest_largest_subspace (n : ℕ) (K : Set (Fin n → ℝ)) (hK : IsConvexCone n K) (h0 : 0 ∈ K) : ↑(Submodule.span ℝ K) = {z : Fin n → ℝ | ∃ x ∈ K, ∃ y ∈ K, z = x - y} ∧ ↑(Submodule.span ℝ K) = ↑(affineSpan ℝ K) ∧ ∃ (S : Submodule ℝ (Fin n → ℝ)), ↑S ⊆ K ∧ (∀ (T : Submodule ℝ (Fin n → ℝ)), ↑T ⊆ K → T ≤ S) ∧ ↑S = {x : Fin n → ℝ | x ∈ K ∧ -x ∈ K}

Theorem 2.7. Let K be a convex cone containing 0. Then the smallest subspace containing K is the set of differences {x - y | x ∈ K, y ∈ K}, which coincides with aff K, and the largest subspace contained in K is (-K) ∩ K.

def IsNormalToConvexSet (n : ℕ) (C : Set (Fin n → ℝ)) (a xstar : Fin n → ℝ) : Prop

Definition 2.7.10. A vector x* is normal to a convex set C at a point a ∈ C if ⟪x - a, x*⟫ ≤ 0 for every x ∈ C; the set of all vectors normal to C at a is called the normal cone to C at a.

Equations

• IsNormalToConvexSet n C a xstar = (a ∈ C ∧ ∀ x ∈ C, (x - a) ⬝ᵥ xstar ≤ 0)

def normalConeAt (n : ℕ) (C : Set (Fin n → ℝ)) (a : Fin n → ℝ) : Set (Fin n → ℝ)

Definition 2.7.10. The normal cone to C at a is the set of all vectors normal to C at a.

Equations

• normalConeAt n C a = {xstar : Fin n → ℝ | IsNormalToConvexSet n C a xstar}

def barrierCone (n : ℕ) (C : Set (Fin n → ℝ)) : Set (Fin n → ℝ)

Definition 2.7.11. The barrier cone of a convex set C is the set of all vectors x* such that there exists β ∈ ℝ with ⟪x, x*⟫ ≤ β for every x ∈ C.

Equations

• barrierCone n C = {xstar : Fin n → ℝ | ∃ (β : ℝ), ∀ x ∈ C, x ⬝ᵥ xstar ≤ β}

theorem barrierCone_smul_mem (n : ℕ) (C : Set (Fin n → ℝ)) {xstar : Fin n → ℝ} (hx : xstar ∈ barrierCone n C) {t : ℝ} (ht : 0 < t) : t • xstar ∈ barrierCone n C

The barrier cone is closed under positive scalar multiplication.

theorem barrierCone_add_mem (n : ℕ) (C : Set (Fin n → ℝ)) {xstar1 : Fin n → ℝ} (hx1 : xstar1 ∈ barrierCone n C) {xstar2 : Fin n → ℝ} (hx2 : xstar2 ∈ barrierCone n C) : xstar1 + xstar2 ∈ barrierCone n C

The barrier cone is closed under addition.

theorem normalConeAt_add_mem (n : ℕ) (C : Set (Fin n → ℝ)) (a : Fin n → ℝ) {xstar1 : Fin n → ℝ} (hx1 : xstar1 ∈ normalConeAt n C a) {xstar2 : Fin n → ℝ} (hx2 : xstar2 ∈ normalConeAt n C a) : xstar1 + xstar2 ∈ normalConeAt n C a

The normal cone at a is closed under addition.

theorem normalConeAt_smul_mem (n : ℕ) (C : Set (Fin n → ℝ)) (a : Fin n → ℝ) {xstar : Fin n → ℝ} (hx : xstar ∈ normalConeAt n C a) {t : ℝ} (ht : 0 < t) : t • xstar ∈ normalConeAt n C a

The normal cone at a is closed under positive scalar multiplication.

theorem normalConeAt_isConvexCone (n : ℕ) (C : Set (Fin n → ℝ)) (a : Fin n → ℝ) (_hC : Convex ℝ C) (_ha : a ∈ C) : IsConvexCone n (normalConeAt n C a)

Proposition 2.7.12. For a convex set C ⊆ ℝ^n and a point a ∈ C, the normal cone to C at a is a convex cone.

theorem barrierCone_isConvexCone (n : ℕ) (C : Set (Fin n → ℝ)) (_hC : Convex ℝ C) : IsConvexCone n (barrierCone n C)

Proposition 2.7.13. For a convex set C ⊆ ℝ^n, the barrier cone of C is a convex cone.

theorem convex_closedHalfSpaceLE_dotProduct (n : ℕ) (b : Fin n → ℝ) (β : ℝ) : Convex ℝ (closedHalfSpaceLE n b β)

The ≤ dot-product half-space is convex.

theorem convex_closedHalfSpaceGE_dotProduct (n : ℕ) (b : Fin n → ℝ) (β : ℝ) : Convex ℝ (closedHalfSpaceGE n b β)

The ≥ dot-product half-space is convex.

theorem convex_openHalfSpaces_dotProduct (n : ℕ) (b : Fin n → ℝ) (β : ℝ) : Convex ℝ (openHalfSpaceLT n b β) ∧ Convex ℝ (openHalfSpaceGT n b β)

The strict dot-product half-spaces (< and >) are convex.

theorem convex_halfSpaces_dotProduct (n : ℕ) (b : Fin n → ℝ) (hb : b ≠ 0) (β : ℝ) : Convex ℝ (closedHalfSpaceLE n b β) ∧ Convex ℝ (closedHalfSpaceGE n b β) ∧ Convex ℝ (openHalfSpaceLT n b β) ∧ Convex ℝ (openHalfSpaceGT n b β)

Corollary 2.0.4. For non-zero b ∈ Real^n and β ∈ Real, each of the four half-spaces {x | ⟪x, b⟫ ≤ β}, {x | ⟪x, b⟫ ≥ β}, {x | ⟪x, b⟫ < β}, {x | ⟪x, b⟫ > β} is a convex subset of Real^n.

theorem isAffineSet_imp_convex (n : ℕ) (M : Set (Fin n → ℝ)) (hM : IsAffineSet n M) : Convex ℝ M

Proposition 2.0.5. Every affine subset of ℝ^n (including ∅ and ℝ^n itself) is convex.

theorem dotProduct_self_pos_of_ne_zero {n : ℕ} {b : Fin n → ℝ} (hb : b ≠ 0) : 0 < b ⬝ᵥ b

A nonzero vector has positive dot product with itself.

theorem exists_dotProduct_eq_of_ne_zero (n : ℕ) (b : Fin n → ℝ) (β : ℝ) (hb : b ≠ 0) : ∃ (x0 : Fin n → ℝ), x0 ⬝ᵥ b = β

For nonzero b, there is a vector with prescribed dot product with b.

theorem dotProduct_shift_by_b (n : ℕ) (b x : Fin n → ℝ) : (x + b) ⬝ᵥ b = x ⬝ᵥ b + b ⬝ᵥ b ∧ (x - b) ⬝ᵥ b = x ⬝ᵥ b - b ⬝ᵥ b

Dot products with b after shifting by ± b in the left argument.

theorem halfSpaces_dotProduct_nonempty (n : ℕ) (b : Fin n → ℝ) (hb : b ≠ 0) (β : ℝ) : (closedHalfSpaceLE n b β).Nonempty ∧ (closedHalfSpaceGE n b β).Nonempty ∧ (openHalfSpaceLT n b β).Nonempty ∧ (openHalfSpaceGT n b β).Nonempty

Proposition 2.0.6. For any non-zero b ∈ Real^n and any β ∈ Real, each of the four half-spaces {x | ⟪x, b⟫ ≤ β}, {x | ⟪x, b⟫ ≥ β}, {x | ⟪x, b⟫ < β}, {x | ⟪x, b⟫ > β} is non-empty.

inductive LinearComparison : Type

A comparison symbol for linear inequalities/equations.

• le : LinearComparison
• ge : LinearComparison
• lt : LinearComparison
• gt : LinearComparison
• eq : LinearComparison

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

Interpret ⟪x, b⟫ (rel) β as a subset of Real^n.

Equations

• linearComparisonSet n b β LinearComparison.le = closedHalfSpaceLE n b β
• linearComparisonSet n b β LinearComparison.ge = closedHalfSpaceGE n b β
• linearComparisonSet n b β LinearComparison.lt = openHalfSpaceLT n b β
• linearComparisonSet n b β LinearComparison.gt = openHalfSpaceGT n b β
• linearComparisonSet n b β LinearComparison.eq = {x : Fin n → ℝ | x ⬝ᵥ b = β}

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

The hyperplane {x | ⟪x, b⟫ = β} is convex, as an intersection of the two closed half-spaces {x | ⟪x, b⟫ ≤ β} and {x | ⟪x, b⟫ ≥ β}.

theorem convex_linearComparisonSet (n : ℕ) (b : Fin n → ℝ) (β : ℝ) (r : LinearComparison) : Convex ℝ (linearComparisonSet n b β r)

Each of the five comparison relations (≤, ≥, <, >, =) defines a convex subset of Real^n via linearComparisonSet.

theorem solutionSet_linearComparison_eq_iInter {ι : Sort u_1} (n : ℕ) (b : ι → Fin n → ℝ) (β : ι → ℝ) (rel : ι → LinearComparison) : {x : Fin n → ℝ | ∀ (i : ι), x ∈ linearComparisonSet n (b i) (β i) (rel i)} = ⋂ (i : ι), linearComparisonSet n (b i) (β i) (rel i)

The solution set of a family of linear comparisons is the intersection of the individual constraint sets.

theorem convex_solutionSet_linearComparison {ι : Sort u_1} (n : ℕ) (b : ι → Fin n → ℝ) (β : ι → ℝ) (rel : ι → LinearComparison) : Convex ℝ {x : Fin n → ℝ | ∀ (i : ι), x ∈ linearComparisonSet n (b i) (β i) (rel i)}

Corollary 2.1.2. Given any system of simultaneous linear inequalities and equations in n variables, obtained by combining relations of the form ⟪x, b i⟫ ≤ β i, ⟪x, b i⟫ ≥ β i, ⟪x, b i⟫ < β i, ⟪x, b i⟫ > β i, and ⟪x, b i⟫ = β i (with b i ∈ Real^n and β i ∈ Real), the set of all solutions C ⊆ Real^n is convex.

theorem convexSetDim_le_finrank_direction_of_subset_affineSubspace {n : ℕ} {D : Set (Fin n → ℝ)} {A : AffineSubspace ℝ (Fin n → ℝ)} (hDA : D ⊆ ↑A) : convexSetDim n D ≤ Module.finrank ℝ ↥A.direction

If D lies in an affine subspace A, then the dimension of D is at most the finrank of A.direction.

theorem two_le_convexSetDim_of_exists_simplex_two {n : ℕ} {D : Set (Fin n → ℝ)} (hsimplex : ∃ P ⊆ D, IsSimplex n 2 P) : 2 ≤ convexSetDim n D

If D contains a 2-simplex, then the dimension of D is at least 2.

theorem convexDisk_convexSetDim_eq_two (n : ℕ) (D : Set (Fin n → ℝ)) (hconv : Convex ℝ D) (hsub : ∃ (A : AffineSubspace ℝ (Fin n → ℝ)), D ⊆ ↑A ∧ Module.finrank ℝ ↥A.direction = 2) (hsimplex : ∃ P ⊆ D, IsSimplex n 2 P) : convexSetDim n D = 2

Proposition 2.4.11. Every convex disk in ℝ^n has dimension 2, independently of the ambient dimension n.

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

Rewrite ∀ i, 0 ≤ ⟪x, b i⟫ as ∀ i, ⟪x, -b i⟫ ≤ 0.

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

Corollary 2.5.2. 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.

theorem add_mem_setOf_forall_dotProduct_pos {ι : Sort u_1} {n : ℕ} {b : ι → Fin n → ℝ} {x y : Fin n → ℝ} : (∀ (i : ι), 0 < x ⬝ᵥ b i) → (∀ (i : ι), 0 < y ⬝ᵥ b i) → ∀ (i : ι), 0 < (x + y) ⬝ᵥ b i

Pointwise add-closure for {x | ∀ i, 0 < x ⬝ᵥ b i}.

theorem smul_mem_setOf_forall_dotProduct_pos {ι : Sort u_1} {n : ℕ} {b : ι → Fin n → ℝ} {x : Fin n → ℝ} {t : ℝ} : (∀ (i : ι), 0 < x ⬝ᵥ b i) → 0 < t → ∀ (i : ι), 0 < t • x ⬝ᵥ b i

Pointwise positive-scalar closure for {x | ∀ i, 0 < x ⬝ᵥ b i}.

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

Corollary 2.5.3. 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.

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

Rewrite ∀ i, ⟪x, b i⟫ < 0 as ∀ i, 0 < ⟪x, -b i⟫.

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

Corollary 2.5.4. 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.

theorem add_mem_setOf_forall_dotProduct_eq_zero {ι : Sort u_1} {n : ℕ} {b : ι → Fin n → ℝ} {x y : Fin n → ℝ} : (∀ (i : ι), x ⬝ᵥ b i = 0) → (∀ (i : ι), y ⬝ᵥ b i = 0) → ∀ (i : ι), (x + y) ⬝ᵥ b i = 0

Pointwise add-closure for {x | ∀ i, x ⬝ᵥ b i = 0}.

theorem smul_mem_setOf_forall_dotProduct_eq_zero {ι : Sort u_1} {n : ℕ} {b : ι → Fin n → ℝ} {x : Fin n → ℝ} {t : ℝ} : (∀ (i : ι), x ⬝ᵥ b i = 0) → ∀ (i : ι), t • x ⬝ᵥ b i = 0

Pointwise scalar closure for {x | ∀ i, x ⬝ᵥ b i = 0}.

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

Corollary 2.5.5. 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.

theorem convexCone_linearComparisonSet_zero (n : ℕ) (b : Fin n → ℝ) (r : LinearComparison) : IsConvexCone n (linearComparisonSet n b 0 r)

Each homogeneous linear comparison set ⟪x, b⟫ (rel) 0 is a convex cone.

theorem convexCone_solutionSet_homogeneous_linearComparison {ι : Sort u_1} (n : ℕ) (b : ι → Fin n → ℝ) (rel : ι → LinearComparison) : IsConvexCone n {x : Fin n → ℝ | ∀ (i : ι), x ∈ linearComparisonSet n (b i) 0 (rel i)}

Corollary 2.5.6. Let b i ∈ Real^n for i ∈ I, where I is an arbitrary index set, and consider a system of homogeneous linear relations of the form ⟪x, b i⟫ ≤ 0, ⟪x, b i⟫ ≥ 0, ⟪x, b i⟫ < 0, ⟪x, b i⟫ > 0, and ⟪x, b i⟫ = 0 for various indices i ∈ I. Then the set K of all solutions x ∈ Real^n is a convex cone.

theorem submodule_add_closed (n : ℕ) (S : Submodule ℝ (Fin n → ℝ)) (x : Fin n → ℝ) : x ∈ ↑S → ∀ y ∈ ↑S, x + y ∈ ↑S

A submodule (linear subspace) is closed under addition.

theorem submodule_pos_smul_closed (n : ℕ) (S : Submodule ℝ (Fin n → ℝ)) (x : Fin n → ℝ) : x ∈ ↑S → ∀ (t : ℝ), 0 < t → t • x ∈ ↑S

A submodule (linear subspace) is closed under positive scalar multiplication.

theorem submodule_isConvexCone (n : ℕ) (S : Submodule ℝ (Fin n → ℝ)) : IsConvexCone n ↑S

Proposition 2.5.14. Every linear subspace of Real^n is a convex cone.

theorem nonNegativeOrthant_add_mem (n : ℕ) (x : Fin n → ℝ) : x ∈ nonNegativeOrthant n → ∀ y ∈ nonNegativeOrthant n, x + y ∈ nonNegativeOrthant n

The nonnegative orthant is closed under addition.

theorem nonNegativeOrthant_pos_smul_mem (n : ℕ) (x : Fin n → ℝ) : x ∈ nonNegativeOrthant n → ∀ (t : ℝ), 0 < t → t • x ∈ nonNegativeOrthant n

The nonnegative orthant is closed under positive scalar multiplication.

theorem positiveOrthant_add_mem (n : ℕ) (x : Fin n → ℝ) : x ∈ positiveOrthant n → ∀ y ∈ positiveOrthant n, x + y ∈ positiveOrthant n

The positive orthant is closed under addition.

theorem positiveOrthant_pos_smul_mem (n : ℕ) (x : Fin n → ℝ) : x ∈ positiveOrthant n → ∀ (t : ℝ), 0 < t → t • x ∈ positiveOrthant n

The positive orthant is closed under positive scalar multiplication.

theorem orthants_isConvexCone (n : ℕ) : IsConvexCone n (nonNegativeOrthant n) ∧ IsConvexCone n (positiveOrthant n)

Proposition 2.5.15. The non-negative orthant and the positive orthant of Real^n are convex cones.

theorem halfSpaces_through_origin_isConvexCone (n : ℕ) (b : Fin n → ℝ) : IsConvexCone n (closedHalfSpaceLE n b 0) ∧ IsConvexCone n (closedHalfSpaceGE n b 0) ∧ IsConvexCone n (openHalfSpaceLT n b 0) ∧ IsConvexCone n (openHalfSpaceGT n b 0)

Proposition 2.5.16. The open and closed half-spaces corresponding to a hyperplane through the origin are convex cones. Concretely, for b : Real^n, the hyperplane {x | ⟪x, b⟫ = 0} has associated closed half-spaces {x | ⟪x, b⟫ ≤ 0}, {x | ⟪x, b⟫ ≥ 0} and open half-spaces {x | ⟪x, b⟫ < 0}, {x | ⟪x, b⟫ > 0}.

theorem convexConeSection_sum_weights_eq_one_of_cons_eq {n m : ℕ} {y : Fin n → ℝ} {x : Fin (m + 1) → Fin n → ℝ} {w : Fin (m + 1) → ℝ} (h : Fin.cons 1 y = ∑ i : Fin (m + 1), w i • Fin.cons 1 (x i)) : ∑ i : Fin (m + 1), w i = 1

Reading off the 0-th coordinate of a Fin.cons equality gives the normalization ∑ w = 1.

theorem convexConeSection_tail_eq_sum_smul_of_cons_eq {n m : ℕ} {y : Fin n → ℝ} {x : Fin (m + 1) → Fin n → ℝ} {w : Fin (m + 1) → ℝ} (h : Fin.cons 1 y = ∑ i : Fin (m + 1), w i • Fin.cons 1 (x i)) : y = ∑ i : Fin (m + 1), w i • x i

Reading off the tail coordinates of a Fin.cons equality gives the corresponding weighted-sum identity in Fin n → ℝ.

theorem exists_convexCone_section_eq (n : ℕ) (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) : ∃ (K : Set (Fin (n + 1) → ℝ)), IsConvexCone (n + 1) K ∧ C = {x : Fin n → ℝ | Fin.cons 1 x ∈ K}

Proposition 2.6.12. Every convex set C ⊆ ℝ^n can be realized as a cross-section of a convex cone in a higher-dimensional space: there exists a convex cone K ⊆ ℝ^{n+1} such that C = {x ∈ ℝ^n | (1, x) ∈ K}.