Rockafellar, §19: Polyhedral Convex Sets and Functions #
The Minkowski–Weyl theorem and the polyhedral calculus, over Rn n = ℝⁿ.
All seventeen numbered results of §19 are formalized: Theorems 19.1–19.7 and Corollaries 19.1.1,
19.1.2, 19.2.1, 19.2.2, 19.3.1–19.3.4, 19.5.1, 19.7.1, together with the unnumbered normal form
f = h + δ(· | C).
The section's five notions are the backbone's. A polyhedral convex set is Polyhedral, the
solution set of finitely many weak linear inequalities; a polyhedral convex cone is
PolyhedralCone; a finitely generated convex set is FinitelyGenerated, that is convexHullPD
of a finite set of points and directions; a polytope is IsPolytope, a bounded set of either
kind; and a polyhedral convex function is PolyhedralFn f := Polyhedral (epi f), with
FinitelyGeneratedFn its generated twin.
Theorems 19.6 and 19.7 and Corollary 19.5.1 use Rockafellar's extended coefficient λ ≥ 0⁺,
modelled by §9's ExtCoeff: ExtCoeff.smulSet sends 0⁺ to the recession cone and
ExtCoeff.smulFn to the recession function.
Every statement of §19 is correct as printed; two of its proofs are not. Theorem 19.1's
(b) ⇒ (a) reduces without justification to the n-dimensional case, and is proved here through
clause (c) instead; Theorem 19.6 is printed with no proof paragraph at all.
References #
- R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §19.
The book's spellings of the two definitions #
§19: a polytope is a bounded finitely generated convex set — equivalently
(isPolytope_iff) a bounded polyhedral convex set.
Equations
- Rockafellar.IsPolytope C = ∃ (P : Finset (TdafSurface.Rn n)), C = (convexHull ℝ) ↑P
Instances For
§19: a convex function is finitely generated when its epigraph is a finitely generated
convex set in ℝⁿ⁺¹. The book defines it by an infimum formula and then observes, before Corollary
19.1.2, that this says f x = inf {μ | (x, μ) ∈ F} for F the hull of the points (aᵢ, αᵢ),
their directions and the direction (0, 1); the generator (0, 1) is absorbed here into the
requirement that the generated set be an epigraph.
Equations
Instances For
A polytope is exactly a bounded polyhedral convex set.
Theorem 19.1 #
Theorem 19.1 (Minkowski–Weyl), clauses (a) and (c): a convex set is polyhedral — an intersection of finitely many closed half-spaces — iff it is finitely generated, the convex hull of a finite set of points and directions.
Theorem 19.1, clause (a) in the book's notation: C is polyhedral exactly when it solves a
finite system ⟨x, bᵢ⟩ ≤ βᵢ in vectors bᵢ. The backbone quantifies over linear functionals,
which the pairing represents on ℝⁿ.
Theorem 19.1, clause (c) in the book's notation: C is finitely generated exactly when
C = conv S for a finite set S of points and directions.
Theorem 19.1, first half of clause (b): a polyhedral convex set is closed.
Theorem 19.1, second half of clause (b): a polyhedral convex set has finitely many faces.
Theorem 19.1, (b) ⇒ (c): a closed convex set with finitely many faces is finitely generated.
Theorem 19.1, (b) ⇒ (a): a closed convex set with finitely many faces is polyhedral.
The book's proof of this implication has a hole: it writes "it suffices to treat the case where
C is n-dimensional in Rⁿ" with no justification, then runs the tangent half-spaces of Theorem
18.8 over that case. The route taken here avoids the reduction — (b) ⇒ (c) ⇒ (a) — and never uses
Theorem 18.8 or counts a dimension.
Theorem 19.1, clauses (a) and (b): a convex set is polyhedral iff it is closed and has
finitely many faces. With theorem_19_1 this completes the three-way statement.
§19, the remark after Theorem 19.1: a face of a polyhedral convex set is polyhedral.
Corollary 19.1.1 #
Corollary 19.1.1, the points half: a polyhedral convex set has finitely many extreme points.
Corollary 19.1.1, the directions half: a polyhedral convex set has finitely many extreme
directions. This cannot read (extremeDirections C).Finite: a direction is recorded by a
generating vector, so extremeDirections C is closed under positive rescaling and is infinite as
soon as it is non-empty. The finiteness is stated up to positive scaling, which is what the book
means.
Corollary 19.1.2 #
Corollary 19.1.2, first sentence: a convex function is polyhedral iff it is finitely generated. Both sides are Theorem 19.1 applied to the epigraph.
Corollary 19.1.2, second sentence: a proper polyhedral convex function is closed.
Properness cannot be dropped: f ≡ ⊥ has epigraph ℝⁿ⁺¹, polyhedral by the empty system, and is
not closed in the ClosedFn sense.
Corollary 19.1.2, third sentence: the infimum defining a finitely generated convex function is attained wherever it is finite.
Theorem 19.2 and its corollaries #
Theorem 19.2. The conjugate of a polyhedral convex function is polyhedral. No properness is assumed, and none is needed.
Corollary 19.2.1. A closed convex set is polyhedral iff its support function is polyhedral.
Corollary 19.2.2. The polar of a polyhedral convex set is polyhedral.
Theorem 19.3 and its corollaries #
Theorem 19.3, first half: the image AC of a polyhedral convex set under a linear
transformation A : ℝⁿ → ℝᵐ is polyhedral.
Theorem 19.3, second half: the preimage A⁻¹D of a polyhedral convex set is
polyhedral.
Corollary 19.3.1, first half: the image Af of a polyhedral convex function is
polyhedral.
Corollary 19.3.1, the attainment clause: the infimum defining (Af)(y) is attained
wherever it is finite.
Corollary 19.3.1, second half: gA is polyhedral for g polyhedral.
Corollary 19.3.2. A sum of two polyhedral convex sets is polyhedral.
Corollary 19.3.3. Two disjoint polyhedral convex sets can be separated strongly. The
book's non-emptiness hypotheses are kept because the book has them, but are not used: C₁ - C₂ is
polyhedral hence closed, and Theorem 11.4 applies.
Corollary 19.3.4. The infimal convolute f₁ □ f₂ of two polyhedral convex functions is
polyhedral. Properness, which the book assumes, is not needed.
Corollary 19.3.4, the attainment clause: the infimum defining (f₁ □ f₂)(x) is attained
wherever it is finite.
Theorem 19.4 #
Theorem 19.4. A sum of two proper polyhedral convex functions is polyhedral. Properness
enters only as ∀ x, fᵢ x ≠ ⊥, which is what makes the EReal splitting
f₁ x + f₂ x ≤ μ ↔ ∃ α β, f₁ x ≤ α ∧ f₂ x ≤ β ∧ α + β = μ valid; ⊤ + ⊥ would break it.
The normal form f = h + δ(· | C) #
§19, the unnumbered normal form: f is polyhedral convex iff
f x = h x + δ(x | C), with h x = max {⟨x, b₁⟩ - β₁, …, ⟨x, bₖ⟩ - βₖ} and
C = {x | ⟨x, bₖ₊₁⟩ ≤ βₖ₊₁, …, ⟨x, bₘ⟩ ≤ βₘ}.
The two families are the two kinds of closed half-space that can bound epi f in ℝⁿ⁺¹: epigraphs
of affine functions, and "vertical" ones. ∀ x, f x ≠ ⊥ cannot be dropped: since ⊥ + ⊤ = ⊥ in
EReal, a right-hand side of this shape takes the value ⊥ only inside C, whereas the function
that is ⊥ on a non-empty polyhedral C and ⊤ outside is convex with polyhedral epigraph.
Theorem 19.5 and its corollary #
Theorem 19.5, first assertion: λC is polyhedral for every scalar λ. One statement
covers λ > 0, λ = 0 and λ < 0, so the book's three-way case split is not reproduced.
Theorem 19.5, second assertion: the recession cone of a non-empty polyhedral convex set is a polyhedral convex cone.
Theorem 19.5, third assertion: if C = conv S for a finite set S of points and
directions, then 0⁺C = conv S₀ for S₀ the origin together with the directions of S, which is
the cone PointedCone.hull ℝ ↑D they generate.
Corollary 19.5.1. For f a proper polyhedral convex function, fλ is polyhedral for
λ ≥ 0 and for λ = 0⁺, the λ ≥ 0⁺ convention being §9's ExtCoeff.smulFn.
Theorems 19.6 and 19.7 #
Theorem 19.6 for m = 2: cl (conv (C₁ ∪ C₂)) is polyhedral for C₁, C₂ non-empty
polyhedral. The book prints Theorem 19.6 with no proof paragraph; the argument formalized here
is the one in its running text.
Theorem 19.6 for m = 2, the formula
cl (conv (C₁ ∪ C₂)) = ⋃ {λ₁C₁ + λ₂C₂ | λᵢ ≥ 0, λ₁ + λ₂ = 1},
with 0⁺Cᵢ substituted for 0Cᵢ when λᵢ = 0. The union is indexed by ExtCoeff, exactly as in
Theorem 9.8.
Theorem 19.6 for general m: cl (conv (C₁ ∪ ⋯ ∪ Cₘ)) is polyhedral. Indexed by a
Finset, which also allows the empty family, where both sides are ∅.
Theorem 19.6 for general m, in convention-free form:
cl (conv (C₁ ∪ ⋯ ∪ Cₘ)) = conv (C₁ ∪ ⋯ ∪ Cₘ) + (0⁺C₁ + ⋯ + 0⁺Cₘ).
Adding the recession cones says what the book's union over weights says, with no convention.
The λ ≥ 0⁺ convention for a single set. For convex C, Rockafellar's
⋃ {λC | λ > 0 or λ = 0⁺} is exactly cone C + 0⁺C. Theorem 19.7 asks C non-empty; the identity
does not, both sides collapsing to 0⁺∅ when C = ∅.
Theorem 19.7. For C a non-empty polyhedral convex set, the closure of the convex cone
generated by C is a polyhedral convex cone. The closure is needed: for C the horizontal line at
height 1 in ℝ² the cone generated is the open upper half-plane with the origin, and the missing
horizontal directions are exactly 0⁺C.
Theorem 19.7, the formula K = ⋃ {λC | λ > 0 or λ = 0⁺}, converted by
iUnion_extCoeff_pos into the backbone's cone C + 0⁺C.
Corollary 19.7.1. If a polyhedral convex set C contains the origin, the convex cone
generated by C is polyhedral, with no closure needed.