theorem cor11_6_1_intrinsicInterior_eq_interior_of_affineSpan_eq_top {n : ℕ} (C : Set (Fin n → ℝ)) (hspan : affineSpan ℝ C = ⊤) : intrinsicInterior ℝ C = interior C

If affineSpan ℝ C = ⊤, then intrinsicInterior ℝ C agrees with the usual interior C.

theorem cor11_6_1_exists_normal_of_affineSpan_ne_top {n : ℕ} (hn : 0 < n) {C : Set (Fin n → ℝ)} (hspan : affineSpan ℝ C ≠ ⊤) (x : Fin n → ℝ) : x ∈ C → ∃ (b : Fin n → ℝ), b ≠ 0 ∧ ∀ y ∈ C, y ⬝ᵥ b ≤ x ⬝ᵥ b

If affineSpan ℝ C ≠ ⊤ and 0 < n, then every point of C admits a nonzero normal vector coming from a hyperplane containing C.

theorem cor11_6_1_disjoint_singleton_intrinsicInterior_of_mem_frontier_of_affineSpan_eq_top {n : ℕ} {C : Set (Fin n → ℝ)} (hspan : affineSpan ℝ C = ⊤) {x : Fin n → ℝ} (hxfr : x ∈ frontier C) : Disjoint {x} (intrinsicInterior ℝ C)

If affineSpan ℝ C = ⊤, then a point in the (ambient) boundary of C is disjoint from the intrinsic interior of C (as a singleton set).

theorem cor11_6_1_exists_normal_of_disjoint_singleton_intrinsicInterior {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) {x : Fin n → ℝ} (hxC : x ∈ C) (hdisj : Disjoint {x} (intrinsicInterior ℝ C)) : ∃ (b : Fin n → ℝ), b ≠ 0 ∧ ∀ y ∈ C, y ⬝ᵥ b ≤ x ⬝ᵥ b

From Theorem 11.6 (with D = {x}), extract a nonzero normal vector to C at x.

theorem exists_nonzero_normal_of_mem_frontier_of_convex (n : ℕ) (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) (x : Fin n → ℝ) : x ∈ C → x ∈ frontier C → ∃ (b : Fin n → ℝ), b ≠ 0 ∧ ∀ y ∈ C, y ⬝ᵥ b ≤ x ⬝ᵥ b

Corollary 11.6.1. A convex set has a non-zero normal at each of its boundary points.

theorem cor11_6_2_disjoint_singleton_intrinsicInterior_of_mem_intrinsicFrontier {n : ℕ} {C : Set (Fin n → ℝ)} {x : Fin n → ℝ} (hx : x ∈ intrinsicFrontier ℝ C) : Disjoint {x} (intrinsicInterior ℝ C)

If x ∈ intrinsicFrontier ℝ C, then the singleton {x} is disjoint from intrinsicInterior ℝ C.

theorem cor11_6_2_exists_lt_of_isSupportingHyperplane_of_not_subset {n : ℕ} {C H : Set (Fin n → ℝ)} (hH : IsSupportingHyperplane n C H) (hCnot : ¬C ⊆ H) : ∃ (b : Fin n → ℝ) (β : ℝ), b ≠ 0 ∧ H = {x : Fin n → ℝ | x ⬝ᵥ b = β} ∧ (∀ x ∈ C, x ⬝ᵥ b ≤ β) ∧ ∃ y0 ∈ C, y0 ⬝ᵥ b < β

A nontrivial supporting hyperplane gives a point of C where the defining linear functional is strictly smaller than its boundary value.

theorem cor11_6_2_not_mem_intrinsicInterior_of_isMaxOn_of_exists_lt {n : ℕ} {C : Set (Fin n → ℝ)} {x : Fin n → ℝ} {l : StrongDual ℝ (Fin n → ℝ)} (hexists : ∃ y ∈ C, l y < l x) (hxmax : IsMaxOn (fun (y : Fin n → ℝ) => l y) C x) : x ∉ intrinsicInterior ℝ C

If a linear functional attains a strict maximum over C at x, then x is not in the intrinsic interior of C.

theorem mem_intrinsicFrontier_iff_exists_isMaxOn_linearFunctional (n : ℕ) (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) (x : Fin n → ℝ) : x ∈ C ∧ x ∈ intrinsicFrontier ℝ C ↔ ∃ (l : StrongDual ℝ (Fin n → ℝ)), (∃ y ∈ C, l y < l x) ∧ IsMaxOn (fun (y : Fin n → ℝ) => l y) C x ∧ x ∈ C

Corollary 11.6.2. Let C be a convex set. An x ∈ C is a relative boundary point of C if and only if there exists a linear function h not constant on C such that h achieves its maximum over C at x. (Here "relative boundary" is interpreted as membership in intrinsicFrontier ℝ C.)

theorem hyperplaneSeparatesProperly_comm {n : ℕ} {H C₁ C₂ : Set (Fin n → ℝ)} : HyperplaneSeparatesProperly n H C₁ C₂ → HyperplaneSeparatesProperly n H C₂ C₁

HyperplaneSeparatesProperly is symmetric in the two sets.

theorem bddAbove_image_dotProduct_of_forall_le {n : ℕ} {C : Set (Fin n → ℝ)} (b : Fin n → ℝ) (β : ℝ) (h : ∀ x ∈ C, x ⬝ᵥ b ≤ β) : BddAbove ((fun (x : Fin n → ℝ) => x ⬝ᵥ b) '' C)

If x ⬝ᵥ b ≤ β for all x ∈ C, then ((fun x ↦ x ⬝ᵥ b) '' C) is bounded above.

theorem thm11_7_dotProduct_le_zero_of_isConeSet_of_bddAbove {n : ℕ} {C : Set (Fin n → ℝ)} (hcone : IsConeSet n C) {b : Fin n → ℝ} (hbdd : BddAbove ((fun (x : Fin n → ℝ) => x ⬝ᵥ b) '' C)) (x : Fin n → ℝ) : x ∈ C → x ⬝ᵥ b ≤ 0

On a cone, a dot-product bounded above must be nonpositive everywhere.

theorem thm11_7_sSup_image_dotProduct_eq_zero_of_isConeSet {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hcone : IsConeSet n C) (b : Fin n → ℝ) (hbdd : BddAbove ((fun (x : Fin n → ℝ) => x ⬝ᵥ b) '' C)) : sSup ((fun (x : Fin n → ℝ) => x ⬝ᵥ b) '' C) = 0

For a nonempty cone, a bounded-above dot-product has supremum 0.

theorem exists_hyperplaneSeparatesProperly_through_origin_of_isConeSet (n : ℕ) (C₁ C₂ : Set (Fin n → ℝ)) (hC₁ne : C₁.Nonempty) (hC₂ne : C₂.Nonempty) (hcone : IsConeSet n C₁ ∨ IsConeSet n C₂) : (∃ (H : Set (Fin n → ℝ)), HyperplaneSeparatesProperly n H C₁ C₂) → ∃ (H : Set (Fin n → ℝ)), HyperplaneSeparatesProperly n H C₁ C₂ ∧ 0 ∈ H

Theorem 11.7. Let C₁ and C₂ be non-empty subsets of ℝ^n, at least one of which is a cone. If there exists a hyperplane which separates C₁ and C₂ properly, then there exists a hyperplane which separates C₁ and C₂ properly and passes through the origin.

theorem cor11_7_1_exists_strict_dotProduct_separator_of_not_mem {n : ℕ} {K : Set (Fin n → ℝ)} (hKne : K.Nonempty) (hKclosed : IsClosed K) (hKconv : Convex ℝ K) {a : Fin n → ℝ} (ha : a ∉ K) : ∃ (b : Fin n → ℝ) (β : ℝ), b ≠ 0 ∧ (∀ x ∈ K, x ⬝ᵥ b ≤ β) ∧ β < a ⬝ᵥ b

If a ∉ K for a nonempty closed convex set K, then there is a dot-product functional strictly separating a from K in the sense x ⬝ᵥ b ≤ β < a ⬝ᵥ b.

theorem cor11_7_1_exists_homogeneous_halfspace_superset_excluding_of_not_mem {n : ℕ} {K : Set (Fin n → ℝ)} (hKne : K.Nonempty) (hKclosed : IsClosed K) (hK : IsConvexCone n K) {a : Fin n → ℝ} (ha : a ∉ K) : ∃ (b : Fin n → ℝ), b ≠ 0 ∧ K ⊆ {x : Fin n → ℝ | x ⬝ᵥ b ≤ 0} ∧ 0 < a ⬝ᵥ b

If a ∉ K for a nonempty closed convex cone K, then some homogeneous closed half-space contains K but excludes a.

theorem isClosed_convexCone_eq_iInter_homogeneous_closedHalfspaces (n : ℕ) (K : Set (Fin n → ℝ)) (hKne : K.Nonempty) (hKclosed : IsClosed K) (hK : IsConvexCone n K) : ⋂ (b : Fin n → ℝ), ⋂ (_ : b ≠ 0), ⋂ (_ : K ⊆ {x : Fin n → ℝ | x ⬝ᵥ b ≤ 0}), {x : Fin n → ℝ | x ⬝ᵥ b ≤ 0} = K

Corollary 11.7.1: A non-empty closed convex cone K ⊆ ℝ^n is the intersection of the homogeneous closed half-spaces which contain it (a homogeneous half-space being one with the origin on its boundary).

theorem cor11_7_2_isConeSet_closure {n : ℕ} {K : Set (Fin n → ℝ)} (hK : IsConeSet n K) : IsConeSet n (closure K)

The closure of a cone set (closed under positive scalar multiplication) is again a cone set.

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

A homogeneous closed half-space {x | x ⬝ᵥ b ≤ 0} is closed.

def cor11_7_2_homogeneousClosedHalfspaceCone {n : ℕ} (b : Fin n → ℝ) : ConvexCone ℝ (Fin n → ℝ)

The homogeneous closed half-space {x | x ⬝ᵥ b ≤ 0} as a bundled ConvexCone.

Equations

• cor11_7_2_homogeneousClosedHalfspaceCone b = { carrier := {x : Fin n → ℝ | x ⬝ᵥ b ≤ 0}, smul_mem' := ⋯, add_mem' := ⋯ }

theorem cor11_7_2_closure_hull_subset_halfspace_of_subset {n : ℕ} (S : Set (Fin n → ℝ)) (b : Fin n → ℝ) (hSb : S ⊆ {x : Fin n → ℝ | x ⬝ᵥ b ≤ 0}) : closure ↑(ConvexCone.hull ℝ S) ⊆ {x : Fin n → ℝ | x ⬝ᵥ b ≤ 0}

If a homogeneous closed half-space {x | x ⬝ᵥ b ≤ 0} contains S, then it contains the closure of the convex cone hull of S.

theorem cor11_7_2_intersections_over_S_vs_over_closure_hull (n : ℕ) (S : Set (Fin n → ℝ)) : ⋂ (b : Fin n → ℝ), ⋂ (_ : b ≠ 0), ⋂ (_ : S ⊆ {x : Fin n → ℝ | x ⬝ᵥ b ≤ 0}), {x : Fin n → ℝ | x ⬝ᵥ b ≤ 0} = ⋂ (b : Fin n → ℝ), ⋂ (_ : b ≠ 0), ⋂ (_ : closure ↑(ConvexCone.hull ℝ S) ⊆ {x : Fin n → ℝ | x ⬝ᵥ b ≤ 0}), {x : Fin n → ℝ | x ⬝ᵥ b ≤ 0}

For K = closure (ConvexCone.hull ℝ S), intersecting all homogeneous closed half-spaces containing S is the same as intersecting those containing K.

theorem closure_convexConeHull_eq_iInter_homogeneous_closedHalfspaces (n : ℕ) (S : Set (Fin n → ℝ)) (hSne : S.Nonempty) : closure ↑(ConvexCone.hull ℝ S) = ⋂ (b : Fin n → ℝ), ⋂ (_ : b ≠ 0), ⋂ (_ : S ⊆ {x : Fin n → ℝ | x ⬝ᵥ b ≤ 0}), {x : Fin n → ℝ | x ⬝ᵥ b ≤ 0}

Corollary 11.7.2: Let S be any subset of ℝ^n, and let K be the closure of the convex cone generated by S. Then K is the intersection of all homogeneous closed half-spaces containing S (a homogeneous closed half-space is one of the form {x | x ⬝ᵥ b ≤ 0} with b ≠ 0).

theorem cor11_7_3_exists_nonzero_vector_of_pos {n : ℕ} (hn : 0 < n) : ∃ (b : Fin n → ℝ), b ≠ 0

In positive dimension, there exists a nonzero vector in ℝ^n (as functions Fin n → ℝ).

theorem cor11_7_3_exists_subset_halfspace_of_empty {n : ℕ} (hn : 0 < n) (K : Set (Fin n → ℝ)) (hKempty : K = ∅) : ∃ (b : Fin n → ℝ), b ≠ 0 ∧ K ⊆ {x : Fin n → ℝ | x ⬝ᵥ b ≤ 0}

If K = ∅ in positive dimension, then K lies in a homogeneous closed half-space {x | x ⬝ᵥ b ≤ 0} with b ≠ 0.

theorem cor11_7_3_extract_homogeneous_halfspace_of_sep_through_origin {n : ℕ} {K : Set (Fin n → ℝ)} {a : Fin n → ℝ} {H : Set (Fin n → ℝ)} (hsep : HyperplaneSeparatesProperly n H {a} K) (h0 : 0 ∈ H) : ∃ (b : Fin n → ℝ), b ≠ 0 ∧ K ⊆ {x : Fin n → ℝ | x ⬝ᵥ b ≤ 0}

From a proper separating hyperplane through the origin between {a} and K, extract a nonzero normal b for a homogeneous closed half-space containing K.

theorem exists_subset_homogeneous_closedHalfspace_of_isConvexCone_ne_univ (n : ℕ) (hn : 0 < n) (K : Set (Fin n → ℝ)) (hK : IsConvexCone n K) (hKne : K ≠ Set.univ) : ∃ (b : Fin n → ℝ), b ≠ 0 ∧ K ⊆ {x : Fin n → ℝ | x ⬝ᵥ b ≤ 0}

Corollary 11.7.3: Let K be a convex cone in ℝ^n other than ℝ^n itself. Then K is contained in some homogeneous closed half-space of ℝ^n. In other words, there exists some vector b ≠ 0 such that x ⬝ᵥ b ≤ 0 for every x ∈ K.