The polyhedral calculus #
The operations that preserve polyhedrality, and the recession cone of a polyhedral set.
Each operation is proved on the side of the description that makes it trivial. Intersections and preimages are trivial for the inequality description — concatenate the systems, or compose each functional with the map — and images and sums are trivial for the generator description — push the generators forward, or add the point sets and unite the direction sets. The Minkowski–Weyl theorem is what lets each proof pick its side.
Main results #
Polyhedral.inter,polyhedral_biInter,polyhedral_iInter,Polyhedral.comap— the inequality side; no finite-dimensionality is needed. The indexed intersections are what a system of constraintsfᵢ x ≤ 0needs.Polyhedral.image,Polyhedral.add— images and sums, through the generator description (Theorem 19.3 in [^1]).recessionCone_polyhedral_system,Polyhedral.polyhedralCone_recessionCone— dropping the right-hand sides of the system gives the recession cone.separatesStrongly_of_polyhedral— two disjoint polyhedral sets are strongly separated, with no closedness or compactness hypothesis to check.finitelyGeneratedCone_hull_of_zero_mem— the convex cone generated by a polyhedral set that contains the origin is finitely generated, with no closure taken.finitelyGenerated_closure_convexHull_union,finitelyGenerated_closure_convexHull_biUnionandfinitelyGeneratedCone_closure_coe_hull— taking the closed convex hull of a union, or the closed convex cone generated by a set, adds exactly the recession cones (Theorems 19.6 and 19.7 in [^1]).
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §19.
The inequality side: intersections and preimages #
An intersection of two polyhedral sets is polyhedral — concatenate the two systems.
polyhedral_biInter and polyhedral_iInter below are the indexed forms.
The intersection of finitely many polyhedral sets is polyhedral (book, line 6817,
unnumbered): the Finset-indexed form, by induction on the index set from polyhedral_univ and
Polyhedral.inter.
Stated over a bare index type: neither the index nor the ambient space needs any structure beyond
the module structure Polyhedral itself is stated over.
The same over a finite index type, which is the shape a family of constraints arrives in.
The preimage of a polyhedral set under a linear map is polyhedral — compose each functional with the map.
The preimage of a polyhedral set under an affine map is polyhedral. The translation is absorbed into the right-hand sides.
A polyhedral cone is a polyhedral set: its system has zero right-hand sides.
A product of polyhedral sets is polyhedral.
In finite dimensions a linear subspace is a polyhedral convex set: it is the preimage of the
origin of E ⧸ S under S.mkQ, and the origin of a finite-dimensional space is a polyhedral
cone. No norm is involved — polyhedralCone_zero needs only a finite basis — which matters,
because E ⧸ S carries no norm unless S is known to be closed.
In finite dimensions a nonempty affine subspace is a polyhedral convex set: translate it to
its direction. This is what makes indicatorFn (affineSpan ℝ (dom g)) a polyhedral convex
function, the device the polyhedral refinement of the exact-sum theorem runs on.
The generator side: images and sums #
An ℝ-linear map read as a map of pointed cones. Constructed by hand rather than by
LinearMap.restrictScalars; see the note on inrₙ.
Equations
- Tdaf.ConvexAnalysis.toNNLinear A = { toFun := ⇑A, map_add' := ⋯, map_smul' := ⋯ }
Instances For
A linear map carries the cone hull of a set to the cone hull of its image.
The cone hull of a linear subspace is the subspace itself.
The cone hull of a union is the sum of the cone hulls.
The cone hull of a finite union is the pointwise sum of the cone hulls: coe_hull_union
iterated over a Finset of indices.
A pointwise Finset sum of subsets of a set that contains the origin and is closed under
addition lands in that set. The two hypotheses are exactly what a cone supplies.
The convex cone generated by a convex set containing the origin is simply the union of its nonnegative multiples: convexity merges any two of them into one, so no sums are left over.
This is the description of PointedCone.hull that lets a hypothesis about the generating set be
transported to the whole cone, provided the property in question is invariant under positive
scaling.
The point generators of a finitely generated set lie in the set.
The direction generators of a finitely generated set are directions of recession of it. Only this inclusion is needed below; the reverse one is the description of the recession cone.
A finitely generated set sits inside the convex cone generated by its own generators.
The sum of two finitely generated cones is finitely generated: concatenate the generators.
Images, sums and differences #
The image of a polyhedral convex set under a linear transformation is polyhedral.
The sum of two polyhedral convex sets is polyhedral.
The negative of a polyhedral set is polyhedral.
The difference of two polyhedral sets is polyhedral.
The convex cone generated by a polyhedral convex set containing the origin is finitely
generated — by the very points and directions that generate the set. A closure is needed in
general; the origin is exactly what makes it unnecessary, since then 0⁺C ⊆ λ C for λ > 0.
A linear subspace of a finite-dimensional space is a finitely generated cone.
A nonnegative multiple of a polyhedral set is polyhedral.
The origin is a polyhedral set.
A singleton is a polyhedral set.
Two disjoint polyhedral convex sets can be separated strongly.
This is cheaper than the general criterion, which asks that the origin miss the closure of
C - D: for polyhedral sets C - D is polyhedral, hence already closed. Neither set has to be
compact, and neither has to be nonempty.
The recession cone #
The recession cone of a nonempty polyhedral set is obtained by dropping the right-hand sides of its system of inequalities.
This is recessionCone_setOf_forall_le (Recession/Cone.lean) with the inequalities turned
around, which is where the two negs come from.
The recession cone of a nonempty polyhedral set is a polyhedral cone: the same statement, in the form that does not name the system.
Closed convex hulls of unions, and generated cones #
Both say the same thing: a construction that generates a non-closed convex set out of polyhedral
ones — the convex hull of a union, the convex cone generated by a set — is repaired by adding the
recession cones, and the repaired set is again polyhedral. The classical statement gives it as a
union over weights λᵢ with 0⁺Cᵢ substituted where λᵢ = 0; adding 0⁺C₁ + 0⁺C₂ to the hull
says the same and needs no convention.
The proof of each is a sandwich between three sets: the closure, the "repaired" set, and the finitely generated set built from the generators of the pieces.
The closed convex hull of the union of two nonempty polyhedral convex sets is finitely generated — hence polyhedral — and is the convex hull of the union with the two recession cones added.
Both sets have to be nonempty: 0⁺∅ is everything. The m-set form is
finitelyGenerated_closure_convexHull_biUnion, proved by the same sandwich rather than by
induction on this one.
The closed convex hull of the union of two nonempty polyhedral convex sets is polyhedral.
The closed convex hull of a union of finitely many nonempty polyhedral convex sets is finitely generated — hence polyhedral — and is obtained from the convex hull of the union by adding the recession cones of the pieces.
Not an induction on finitelyGenerated_closure_convexHull_union. Re-entering the binary statement
at C₁ ∪ cl (conv (⋃ …)) would first have to show that the closed convex hull absorbs an inner
closure, and then that 0⁺ of the inner hull is the sum of the 0⁺ Cᵢ. The binary proof's
three-set sandwich — the closed hull, the repaired set, and the finitely generated set built from
all the generators at once — runs over a Finset of indices with no extra work, so that is what is
done here.
The empty index set needs no side condition: both sides are then ∅.
The closed convex hull of a union of finitely many nonempty polyhedral sets is polyhedral.
The closure of the convex cone generated by a nonempty polyhedral convex set is a finitely generated cone, and is obtained from the cone itself by adding the recession cone of the set.
The closure is genuinely needed: for C the horizontal line at height 1 in ℝ² the cone
generated by C is the open upper half-plane together with the origin, and the missing horizontal
directions are exactly 0⁺C.
The closure of the convex cone generated by a nonempty polyhedral convex set is a polyhedral cone.