The barrier cone and the recession cone #
The barrier cone of a set C is dom (δ*(· ∣ C)), the set of directions in which the pairing
is bounded above on C. For a nonempty closed convex set it is polar to the recession cone.
Main results #
polarCone_dom_supportFn— the polar of the barrier cone of a nonempty closed convex set is its recession cone (Corollary 14.2.1 in [^1]).
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §14.
theorem
Tdaf.ConvexAnalysis.polarCone_dom_supportFn
{E : Type u_1}
{F : Type u_2}
[AddCommGroup E]
[Module ℝ E]
[AddCommGroup F]
[Module ℝ F]
[TopologicalSpace E]
[IsTopologicalAddGroup E]
[ContinuousSMul ℝ E]
[LocallyConvexSpace ℝ E]
{B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ}
{C : Set E}
[IsCompatiblePairing B]
(hC : Convex ℝ C)
(hCcl : IsClosed C)
(hCne : C.Nonempty)
:
The polar of the barrier cone of a nonempty closed convex set is its recession cone.
Nonemptiness matters: for C = ∅ the barrier cone is all of F and its polar is the kernel of the
pairing, while 0⁺∅ is everything.