theorem exists_supportFunctionEReal_eq_convexFunctionClosure_of_epigraph_eq_closure_coneK {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (hC_ne : intersectionOfHalfspaces Sstar ≠ ∅) {g : (Fin n → ℝ) → EReal} (hcone : epigraph Set.univ g = closure (coneK Sstar)) : ∃ (D : Set (Fin n → ℝ)), D.Nonempty ∧ Convex ℝ D ∧ g = supportFunctionEReal D

Represent g as a support function when its epigraph is the closed cone closure coneK.

theorem support_set_subset_intersectionOfHalfspaces_of_epigraph_contains_Sstar {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) {D : Set (Fin n → ℝ)} {g : (Fin n → ℝ) → EReal} (hg : g = supportFunctionEReal D) (hSstar : Sstar ⊆ epigraph Set.univ g) : D ⊆ intersectionOfHalfspaces Sstar

If the epigraph of a support function contains Sstar, then the support set lies in C.

theorem epigraph_supportFunctionEReal_subset_epigraph_convexFunctionClosure {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (hC_ne : intersectionOfHalfspaces Sstar ≠ ∅) {g : (Fin n → ℝ) → EReal} (hcone : epigraph Set.univ g = closure (coneK Sstar)) : epigraph Set.univ (supportFunctionEReal (intersectionOfHalfspaces Sstar)) ⊆ epigraph Set.univ g

The epigraph of supportFunctionEReal C is contained in the epigraph of g.

theorem epigraph_supportFunction_eq_epigraph_convexFunctionClosure_eq_closure_epigraph_eq_closure_coneK {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (hC_ne : intersectionOfHalfspaces Sstar ≠ ∅) : have C := intersectionOfHalfspaces Sstar; have f := fun (xStar : Fin n → ℝ) => match infMuInCone Sstar xStar with | some μ => ↑μ | none => ⊤; epigraph Set.univ (supportFunctionEReal C) = epigraph Set.univ (convexFunctionClosure f) ∧ epigraph Set.univ (convexFunctionClosure f) = closure (epigraph Set.univ f) ∧ closure (epigraph Set.univ f) = closure (coneK Sstar)

Proposition 17.2.8 (Epigraph of the support function as the closure of K), LaTeX label prop:epi_clK. Assume C ≠ ∅, where C = intersectionOfHalfspaces S* as in Definition 17.2.5, and let f, K be as in Definition 17.2.7. Then

epi (supportFunction · C) = epi (cl f) = closure (epi f) = closure K.

In this formalization, cl f is modeled as convexFunctionClosure applied to the function f : ℝⁿ → (ℝ ∪ {+∞}) embedded into EReal.

theorem coneK_add_mem {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) {a b : (Fin n → ℝ) × ℝ} (ha : a ∈ coneK Sstar) (hb : b ∈ coneK Sstar) : a + b ∈ coneK Sstar

Addition preserves membership in coneK.

theorem coneK_smul_mem_of_nonneg {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) {t : ℝ} (ht : 0 ≤ t) {a : (Fin n → ℝ) × ℝ} (ha : a ∈ coneK Sstar) : t • a ∈ coneK Sstar

Nonnegative scaling preserves membership in coneK.

theorem conicCombination_mem_coneK {n m : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (p : Fin m → (Fin n → ℝ) × ℝ) (lam0 : ℝ) (lam : Fin m → ℝ) (hp : ∀ (i : Fin m), p i ∈ Sstar) (hlam0 : 0 ≤ lam0) (hlam : ∀ (i : Fin m), 0 ≤ lam i) : lam0 • verticalVector n + ∑ i : Fin m, lam i • p i ∈ coneK Sstar

Conic combinations of the vertical vector and points of Sstar lie in coneK.

theorem conicRep_add {n m1 m2 : ℕ} (p1 : Fin m1 → (Fin n → ℝ) × ℝ) (p2 : Fin m2 → (Fin n → ℝ) × ℝ) (lam01 lam02 : ℝ) (lam1 : Fin m1 → ℝ) (lam2 : Fin m2 → ℝ) : lam01 • verticalVector n + ∑ i : Fin m1, lam1 i • p1 i + (lam02 • verticalVector n + ∑ i : Fin m2, lam2 i • p2 i) = (lam01 + lam02) • verticalVector n + ∑ i : Fin (m1 + m2), Fin.append lam1 lam2 i • Fin.append p1 p2 i

Combine two conic representations by concatenating coefficients.

theorem conicRep_smul_pos {n m : ℕ} (t : ℝ) (p : Fin m → (Fin n → ℝ) × ℝ) (lam0 : ℝ) (lam : Fin m → ℝ) : t • (lam0 • verticalVector n + ∑ i : Fin m, lam i • p i) = (t * lam0) • verticalVector n + ∑ i : Fin m, (t * lam i) • p i

Scaling a conic representation scales all coefficients.

theorem adjoinVertical_subset_conicRep {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) {q : (Fin n → ℝ) × ℝ} (hq : q ∈ adjoinVertical Sstar) : ∃ (m : ℕ) (p : Fin m → (Fin n → ℝ) × ℝ) (lam0 : ℝ) (lam : Fin m → ℝ), (∀ (i : Fin m), p i ∈ Sstar) ∧ 0 ≤ lam0 ∧ (∀ (i : Fin m), 0 ≤ lam i) ∧ q = lam0 • verticalVector n + ∑ i : Fin m, lam i • p i

Elements of adjoinVertical admit a conic representation.

theorem mem_hull_adjoinVertical_imp_exists_conicCombination {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) {q : (Fin n → ℝ) × ℝ} (hq : q ∈ ↑(ConvexCone.hull ℝ (adjoinVertical Sstar))) : ∃ (m : ℕ) (p : Fin m → (Fin n → ℝ) × ℝ) (lam0 : ℝ) (lam : Fin m → ℝ), (∀ (i : Fin m), p i ∈ Sstar) ∧ 0 ≤ lam0 ∧ (∀ (i : Fin m), 0 ≤ lam i) ∧ q = lam0 • verticalVector n + ∑ i : Fin m, lam i • p i

Membership in the hull of adjoinVertical yields a conic representation.

theorem mem_coneK_iff_exists_conicCombination {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (xStar : Fin n → ℝ) (muStar : ℝ) : (xStar, muStar) ∈ coneK Sstar ↔ ∃ (m : ℕ) (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

Lemma 17.2.9 (Membership in K via conic combinations), LaTeX label lem:K_conic.

Let K be the convex cone generated by S* ∪ {(0, 1)} (here: K = coneK Sstar). Then (x*, μ*) ∈ K if and only if there exist finitely many points (xᵢ*, μᵢ*) ∈ S* and coefficients λ₀, λ₁, …, λₘ ≥ 0 such that

(x*, μ*) = λ₀ (0, 1) + ∑ i, λᵢ (xᵢ*, μᵢ*).

In that case, x* = ∑ i, λᵢ xᵢ* and μ* ≥ ∑ i, λᵢ μᵢ*.

theorem conicCombination_components {n m : ℕ} (xStar : Fin n → ℝ) (muStar : ℝ) (p : Fin m → (Fin n → ℝ) × ℝ) (lam0 : ℝ) (lam : Fin m → ℝ) (hlam0 : 0 ≤ lam0) (hEq : (xStar, muStar) = lam0 • verticalVector n + ∑ i : Fin m, lam i • p i) : xStar = ∑ i : Fin m, lam i • (p i).1 ∧ muStar ≥ ∑ i : Fin m, lam i * (p i).2

Lemma 17.2.9 (Membership in K via conic combinations), consequences: from a conic representation of (x*, μ*) using the vertical vector (0, 1) and points of S*, one obtains x* = ∑ i, λᵢ xᵢ* and μ* ≥ ∑ i, λᵢ μᵢ*.

theorem mem_coneK_imp_exists_nonnegLinearCombination_adjoinVertical_le {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (xStar : Fin n → ℝ) (muStar : ℝ) : (xStar, muStar) ∈ coneK Sstar → ∃ k ≤ n + 1, ∃ (v : Fin k → (Fin n → ℝ) × ℝ) (c : Fin k → ℝ), (∀ (i : Fin k), v i ∈ adjoinVertical Sstar) ∧ (∀ (i : Fin k), 0 ≤ c i) ∧ (xStar, muStar) = ∑ i : Fin k, c i • v i

Carathéodory bound for conic combinations over adjoinVertical.

theorem mem_coneK_imp_exists_linIndep_nonnegLinearCombination_adjoinVertical_le {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (xStar : Fin n → ℝ) (muStar : ℝ) : (xStar, muStar) ∈ coneK Sstar → ∃ k ≤ n + 1, ∃ (v : Fin k → (Fin n → ℝ) × ℝ) (c : Fin k → ℝ), (∀ (i : Fin k), v i ∈ adjoinVertical Sstar) ∧ (∀ (i : Fin k), 0 ≤ c i) ∧ (xStar, muStar) = ∑ i : Fin k, c i • v i ∧ LinearIndependent ℝ v

Extract a linearly independent subfamily from a conic representation over adjoinVertical.

theorem split_adjoinVertical_conicCombination {n k : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (v : Fin k → (Fin n → ℝ) × ℝ) (c : Fin k → ℝ) (hv : ∀ (i : Fin k), v i ∈ adjoinVertical Sstar) (hc : ∀ (i : Fin k), 0 ≤ c i) : ∃ m ≤ k, ∃ (p : Fin m → (Fin n → ℝ) × ℝ) (lam0 : ℝ) (lam : Fin m → ℝ), (∀ (i : Fin m), p i ∈ Sstar) ∧ 0 ≤ lam0 ∧ (∀ (i : Fin m), 0 ≤ lam i) ∧ ∑ i : Fin k, c i • v i = lam0 • verticalVector n + ∑ i : Fin m, lam i • p i

Split a conic combination over adjoinVertical into vertical and Sstar parts.

theorem mem_coneK_imp_exists_conicCombination_le_add_one {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (xStar : Fin n → ℝ) (muStar : ℝ) : (xStar, muStar) ∈ coneK Sstar → ∃ m ≤ n + 1, ∃ (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

Corollary 17.2.10 (Carath'eodory bounds for conic representations), LaTeX label cor:caratheodory_bounds.

In the conic representation from Lemma 17.2.9 (mem_coneK_iff_exists_conicCombination), one can choose:

(1) m ≤ n + 1 (by Carath'eodory's theorem in ℝ^{n+1}); (2) m ≤ n (via the "bottoms of simplices" argument, as in Corollary 17.1.3).

theorem conicSum_snd_nonneg_of_mem_intersectionOfHalfspaces {n m : ℕ} {Sstar : Set ((Fin n → ℝ) × ℝ)} {x0 : Fin n → ℝ} (hx0 : x0 ∈ intersectionOfHalfspaces Sstar) (p : Fin m → (Fin n → ℝ) × ℝ) (lam : Fin m → ℝ) (hp : ∀ (i : Fin m), p i ∈ Sstar) (hlam : ∀ (i : Fin m), 0 ≤ lam i) : x0 ⬝ᵥ ∑ i : Fin m, lam i • (p i).1 ≤ ∑ i : Fin m, lam i * (p i).2

Feasibility bounds the vertical component of a conic sum over Sstar.