The recession cone of a polyhedral set, read off its generators

The recession cone of a nonempty finitely generated convex set conv P + cone D is cone D itself — the generator side of the description Polyhedral/Ops.lean proves on the inequality side. The consequence, Polyhedral.recessionCone_image, is that a linear map commutes with 0⁺ on polyhedral sets with no hypothesis on the map. The general recession calculus cannot supply that: it computes 0⁺(A '' C) only when A kills no direction of recession of C.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §19.

theorem Tdaf.ConvexAnalysis.recessionCone_of_finitelyGenerated {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : Set E} {P D : Finset E} (hPD : C = (convexHull ℝ) ↑P + ↑(PointedCone.hull ℝ ↑D)) (hne : C.Nonempty) : recessionCone C = ↑(PointedCone.hull ℝ ↑D)

The recession cone of a nonempty finitely generated convex set conv P + cone D is cone D itself. The inclusion ⊇ needs nothing; ⊆ is the recession cone of a sum, whose hypothesis is vacuous because conv P is compact.

theorem Tdaf.ConvexAnalysis.Polyhedral.recessionCone_image {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {C : Set E} (hC : Polyhedral C) (hne : C.Nonempty) (A : E →ₗ[ℝ] F) : recessionCone (⇑A '' C) = ⇑A '' recessionCone C

A linear map commutes with 0⁺ on polyhedral sets: 0⁺(A '' C) = A '' 0⁺C, with no hypothesis whatever on A. For a general closed convex C this fails — the image need not even be closed — and the general criterion repairs it only under 0⁺C ∩ ker A = {0}.