theorem exists_pos_coeff_repr_vertical_of_feasible {n : ℕ} {Sstar : Set ((Fin n → ℝ) × ℝ)} {x0 : Fin n → ℝ} (hx0 : x0 ∈ intersectionOfHalfspaces Sstar) (v : Fin (n + 1) → (Fin n → ℝ) × ℝ) (a : Fin (n + 1) → ℝ) (hv : ∀ (i : Fin (n + 1)), v i ∈ Sstar) (hEq : verticalVector n = ∑ i : Fin (n + 1), a i • v i) : ∃ (j : Fin (n + 1)), 0 < a j

A feasible cone prevents a nonpositive representation of the vertical vector.

theorem verticalVector_eq_sum_smul_of_linIndep {n : ℕ} (v : Fin (n + 1) → (Fin n → ℝ) × ℝ) (hv : LinearIndependent ℝ v) : ∃ (a : Fin (n + 1) → ℝ), verticalVector n = ∑ i : Fin (n + 1), a i • v i

Express the vertical vector using a linearly independent (n + 1)-tuple.

theorem reduce_linIndep_Sstar_rep_by_vertical_shift {n : ℕ} {Sstar : Set ((Fin n → ℝ) × ℝ)} {x0 : Fin n → ℝ} (hx0 : x0 ∈ intersectionOfHalfspaces Sstar) (v : Fin (n + 1) → (Fin n → ℝ) × ℝ) (hlin : LinearIndependent ℝ v) (hvS : ∀ (i : Fin (n + 1)), v i ∈ Sstar) (c : Fin (n + 1) → ℝ) (hc : ∀ (i : Fin (n + 1)), 0 ≤ c i) : ∃ (δ : ℝ) (c' : Fin (n + 1) → ℝ) (j : Fin (n + 1)), 0 ≤ δ ∧ (∀ (i : Fin (n + 1)), 0 ≤ c' i) ∧ c' j = 0 ∧ ∑ i : Fin (n + 1), c i • v i = δ • verticalVector n + ∑ i : Fin (n + 1), c' i • v i

Shift a linearly independent conic sum along the vertical vector to zero a coefficient.

theorem sum_smul_succAbove_eq_of_zero {n : ℕ} (v : Fin (n + 1) → (Fin n → ℝ) × ℝ) (c : Fin (n + 1) → ℝ) (j : Fin (n + 1)) (hj : c j = 0) : ∑ i : Fin (n + 1), c i • v i = ∑ i : Fin n, c (j.succAbove i) • v (j.succAbove i)

Drop a zero coefficient from a Fin (n + 1) sum via succAbove.

theorem drop_zero_coeff_conicSum {n : ℕ} {Sstar : Set ((Fin n → ℝ) × ℝ)} (v : Fin (n + 1) → (Fin n → ℝ) × ℝ) (c : Fin (n + 1) → ℝ) (j : Fin (n + 1)) (hj : c j = 0) (hv : ∀ (i : Fin (n + 1)), v i ∈ Sstar) (hc : ∀ (i : Fin (n + 1)), 0 ≤ c i) : ∃ (p : Fin n → (Fin n → ℝ) × ℝ) (lam : Fin n → ℝ), (∀ (i : Fin n), p i ∈ Sstar) ∧ (∀ (i : Fin n), 0 ≤ lam i) ∧ ∑ i : Fin (n + 1), c i • v i = ∑ i : Fin n, lam i • p i

If one coefficient is zero, reindex the conic sum over Fin n by skipping that index.

theorem mem_coneK_imp_exists_conicCombination_le {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (xStar : Fin n → ℝ) (muStar : ℝ) (hC_ne : intersectionOfHalfspaces Sstar ≠ ∅) : (xStar, muStar) ∈ coneK Sstar → ∃ m ≤ n, ∃ (p : Fin m → (Fin n → ℝ) × ℝ) (lam0 : ℝ) (lam : Fin m → ℝ), (∀ (i : Fin m), p i ∈ Sstar) ∧ 0 ≤ lam0 ∧ (∀ (i : Fin m), 0 ≤ lam i) ∧ (xStar, muStar) = lam0 • verticalVector n + ∑ i : Fin m, lam i • p i

theorem intersectionOfHalfspaces_ne_empty_of_full_dim {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (hC_dim : Module.finrank ℝ ↥(affineSpan ℝ (intersectionOfHalfspaces Sstar)).direction = n) (r : HalfspaceRep n) : intersectionOfHalfspaces Sstar ≠ ∅

Full dimensionality and a nonzero normal force the intersection of half-spaces to be nonempty.

theorem halfspace_contains_intersectionOfHalfspaces_imp_mem_closure_coneK {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (hC_ne : intersectionOfHalfspaces Sstar ≠ ∅) (r : HalfspaceRep n) : r.set ⊇ intersectionOfHalfspaces Sstar → (r.xStar, r.muStar) ∈ closure (coneK Sstar)

Containment in a half-space gives membership in the closure of coneK.

theorem exists_mem_interior_intersectionOfHalfspaces_of_full_dim {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (hC_ne : intersectionOfHalfspaces Sstar ≠ ∅) (hC_dim : Module.finrank ℝ ↥(affineSpan ℝ (intersectionOfHalfspaces Sstar)).direction = n) : ∃ (x : Fin n → ℝ), x ∈ interior (intersectionOfHalfspaces Sstar)

Full-dimensionality of C forces a point in the interior.

theorem mem_interior_halfspace_le_imp_dot_lt {n : ℕ} {v : Fin n → ℝ} {μ : ℝ} {x : Fin n → ℝ} (hv : v ≠ 0) (hx : x ∈ interior {y : Fin n → ℝ | y ⬝ᵥ v ≤ μ}) : x ⬝ᵥ v < μ

Interior points of a closed halfspace satisfy the strict inequality.

theorem strict_dot_lt_of_mem_interior_intersectionOfHalfspaces {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (hC_ne : intersectionOfHalfspaces Sstar ≠ ∅) {xbar : Fin n → ℝ} (hxbar : xbar ∈ interior (intersectionOfHalfspaces Sstar)) (hSstar0 : 0 ∉ Sstar) (p : (Fin n → ℝ) × ℝ) : p ∈ Sstar → xbar ⬝ᵥ p.1 < p.2

Interior points give strict inequalities for defining halfspaces.

theorem zero_not_mem_conv_adjoinVertical_of_interior {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (hC_ne : intersectionOfHalfspaces Sstar ≠ ∅) (hSstar0 : 0 ∉ Sstar) (hxbar : ∃ (xbar : Fin n → ℝ), xbar ∈ interior (intersectionOfHalfspaces Sstar)) : 0 ∉ (convexHull ℝ) (adjoinVertical Sstar)

An interior point excludes the origin from conv (adjoinVertical Sstar).

theorem convexHull_image_linearEquiv {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (e : E ≃ₗ[ℝ] F) (D : Set E) : ⇑e '' (convexHull ℝ) D = (convexHull ℝ) (⇑e '' D)

Linear equivalences commute with convexHull.

theorem convexCone_hull_image_linearEquiv {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (e : E ≃ₗ[ℝ] F) (D : Set E) : ⇑e '' ↑(ConvexCone.hull ℝ D) = ↑(ConvexCone.hull ℝ (⇑e '' D))

Linear equivalences commute with ConvexCone.hull on the level of sets.

theorem convexCone_hull_convexHull_eq {E : Type u_1} [AddCommGroup E] [Module ℝ E] (D : Set E) : ↑(ConvexCone.hull ℝ ((convexHull ℝ) D)) = ↑(ConvexCone.hull ℝ D)

Taking the cone hull after convexHull does not change the cone.

theorem image_coneK_eq_convexConeGenerated {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) : have e := prodLinearEquiv_append_coord n; have T := ⇑e '' adjoinVertical Sstar; ⇑e '' coneK Sstar = convexConeGenerated (n + 1) ((convexHull ℝ) T)

The prodLinearEquiv_append_coord image of coneK is a generated cone.

theorem isClosed_coneK_of_closed_bounded_full_dim {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (hSstar_ne : Sstar.Nonempty) (hSstar_closed : IsClosed Sstar) (hSstar_bdd : Bornology.IsBounded Sstar) (hSstar0 : 0 ∉ Sstar) (hC_ne : intersectionOfHalfspaces Sstar ≠ ∅) (hC_dim : Module.finrank ℝ ↥(affineSpan ℝ (intersectionOfHalfspaces Sstar)).direction = n) : IsClosed (coneK Sstar)

Full-dimensionality and compactness of Sstar make coneK closed.

theorem halfspaceRep_set_superset_intersectionOfHalfspaces_iff_exists_dual_caratheodory {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (hSstar_ne : Sstar.Nonempty) (hSstar_closed : IsClosed Sstar) (hSstar_bdd : Bornology.IsBounded Sstar) (hSstar0 : 0 ∉ Sstar) (hC_dim : Module.finrank ℝ ↥(affineSpan ℝ (intersectionOfHalfspaces Sstar)).direction = n) (r : HalfspaceRep n) : r.set ⊇ intersectionOfHalfspaces Sstar ↔ ∃ m ≤ n, ∃ (p : Fin m → (Fin n → ℝ) × ℝ) (lam : Fin m → ℝ), (∀ (i : Fin m), p i ∈ Sstar) ∧ (∀ (i : Fin m), 0 ≤ lam i) ∧ ∑ i : Fin m, lam i • (p i).1 = r.xStar ∧ ∑ i : Fin m, lam i * (p i).2 ≤ r.muStar

Theorem 17.2.11 (Dual Carath'eodory for half-spaces (Theorem 17.3 / 2.10)), LaTeX label thm:dual_caratheodory.

Let S* ⊆ ℝ^{n+1} be nonempty, closed, and bounded, and let C := intersectionOfHalfspaces S* as in Definition 17.2.5 (def:C). Suppose C is n-dimensional (i.e. finrank (affineSpan ℝ C).direction = n).

Fix (x*, μ*) ∈ ℝ^{n+1} with x* ≠ 0 and consider the half-space H = {x ∈ ℝⁿ | ⟪x, x*⟫ ≤ μ*}. Then H ⊇ C if and only if there exist (xᵢ*, μᵢ*) ∈ S* and coefficients λᵢ ≥ 0 for i = 1, …, m, with m ≤ n, such that

∑ i, λᵢ • xᵢ* = x* and ∑ i, λᵢ * μᵢ* ≤ μ*.

theorem dualCaratheodory_halfspace_contains_intersectionOfHalfspaces_iff {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (hSstar_ne : Sstar.Nonempty) (hSstar_closed : IsClosed Sstar) (hSstar_bdd : Bornology.IsBounded Sstar) (hSstar0 : 0 ∉ Sstar) (hC_dim : Module.finrank ℝ ↥(affineSpan ℝ (intersectionOfHalfspaces Sstar)).direction = n) (r : HalfspaceRep n) : r.set ⊇ intersectionOfHalfspaces Sstar ↔ ∃ m ≤ n, ∃ (p : Fin m → (Fin n → ℝ) × ℝ) (lam : Fin m → ℝ), (∀ (i : Fin m), p i ∈ Sstar) ∧ (∀ (i : Fin m), 0 ≤ lam i) ∧ ∑ i : Fin m, lam i • (p i).1 = r.xStar ∧ ∑ i : Fin m, lam i * (p i).2 ≤ r.muStar

Theorem 17.3. Let S* ⊆ ℝ^{n+1} be nonempty, closed, and bounded, and let

C = {x ∈ ℝⁿ | ∀ (x*, μ*) ∈ S*, ⟪x, x*⟫ ≤ μ*}.

Assume the convex set C is n-dimensional (here: finrank (affineSpan ℝ C).direction = n). Fix a half-space H = {x ∈ ℝⁿ | ⟪x, x*⟫ ≤ μ*} with x* ≠ 0 (represented as r : HalfspaceRep n).

Then H ⊇ C if and only if there exist points (xᵢ*, μᵢ*) ∈ S* and coefficients λᵢ ≥ 0, i = 1, …, m, with m ≤ n, such that ∑ i, λᵢ • xᵢ* = x* and ∑ i, λᵢ * μᵢ* ≤ μ*.

theorem iInter_halfspaces_subset_halfspaceRep_of_conicCombination {n m : ℕ} (r : HalfspaceRep n) (p : Fin m → (Fin n → ℝ) × ℝ) (lam : Fin m → ℝ) (hlam : ∀ (i : Fin m), 0 ≤ lam i) (hx : ∑ i : Fin m, lam i • (p i).1 = r.xStar) (hmu : ∑ i : Fin m, lam i * (p i).2 ≤ r.muStar) : ⋂ (i : Fin m), {x : Fin n → ℝ | x ⬝ᵥ (p i).1 ≤ (p i).2} ⊆ r.set

A conic-combination certificate forces a finite intersection to lie in the target half-space.

theorem exists_fin_n_family_padding_iInter_subset {n m : ℕ} {α β : Type} (hm : m ≤ n) (p : Fin m → α) (a0 : α) (P : α → Prop) (H : α → Set β) (R : Set β) (hp : ∀ (i : Fin m), P (p i)) (ha0 : P a0) (hsubset : ⋂ (i : Fin m), H (p i) ⊆ R) : ∃ (q : Fin n → α), (∀ (i : Fin n), P (q i)) ∧ ⋂ (i : Fin n), H (q i) ⊆ R

Pad a finite family of half-spaces without changing the intersection inclusion.

theorem intersectionOfHalfspaces_subset_iInter_of_mem {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (p : Fin n → (Fin n → ℝ) × ℝ) (hp : ∀ (i : Fin n), p i ∈ Sstar) : intersectionOfHalfspaces Sstar ⊆ ⋂ (i : Fin n), {x : Fin n → ℝ | x ⬝ᵥ (p i).1 ≤ (p i).2}

The full intersection of half-spaces is contained in any finite sub-intersection.

theorem halfspaceRep_set_superset_intersectionOfHalfspaces_iff_exists_fin_n_halfspaces_iInter_subset {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (hSstar_ne : Sstar.Nonempty) (hSstar_closed : IsClosed Sstar) (hSstar_bdd : Bornology.IsBounded Sstar) (hSstar0 : 0 ∉ Sstar) (hC_dim : Module.finrank ℝ ↥(affineSpan ℝ (intersectionOfHalfspaces Sstar)).direction = n) (r : HalfspaceRep n) : r.set ⊇ intersectionOfHalfspaces Sstar ↔ ∃ (p : Fin n → (Fin n → ℝ) × ℝ), (∀ (i : Fin n), p i ∈ Sstar) ∧ ⋂ (i : Fin n), {x : Fin n → ℝ | x ⬝ᵥ (p i).1 ≤ (p i).2} ⊆ r.set

Corollary 17.2.12 (Equivalent intersection formulation), LaTeX label cor:intersection_form.

In the setting of Theorem 17.2.11 (thm:dual_caratheodory), the condition intersectionOfHalfspaces S* ⊆ H is equivalent to the existence of n (not necessarily distinct) half-spaces

Hᵢ = {x ∈ ℝⁿ | ⟪x, xᵢ*⟫ ≤ μᵢ*} with (xᵢ*, μᵢ*) ∈ S*

such that H₁ ∩ ··· ∩ Hₙ ⊆ H.

theorem halfspaceRep_set_superset_intersectionOfHalfspaces_iff_exists_fin_n_halfspaces_iInter_subset_page11 {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (hSstar_ne : Sstar.Nonempty) (hSstar_closed : IsClosed Sstar) (hSstar_bdd : Bornology.IsBounded Sstar) (hSstar0 : 0 ∉ Sstar) (hC_dim : Module.finrank ℝ ↥(affineSpan ℝ (intersectionOfHalfspaces Sstar)).direction = n) (r : HalfspaceRep n) : r.set ⊇ intersectionOfHalfspaces Sstar ↔ ∃ (p : Fin n → (Fin n → ℝ) × ℝ), (∀ (i : Fin n), p i ∈ Sstar) ∧ ⋂ (i : Fin n), {x : Fin n → ℝ | x ⬝ᵥ (p i).1 ≤ (p i).2} ⊆ r.set

Corollary 17.3.1 (Equivalent intersection formulation), LaTeX label cor:intersection_form_page11.

Assume the hypotheses of Theorem 17.3 (thm:dual_caratheodory). Then the condition that the intersection intersectionOfHalfspaces S* is contained in the half-space under consideration H = r.set is equivalent to the existence of n (not necessarily distinct) half-spaces H i = {x | ⟪x, x i*⟫ ≤ μ i*} with (x i*, μ i*) ∈ S* such that ⋂ i, H i ⊆ H.