Convex cones in inner product spaces #
Set.innerDualCone to be the cone consisting of all points
y such that for
x in a given set
0 ≤ ⟪ x, y ⟫.
Main statements #
We prove the following theorems:
The dual cone #
The inner dual cone of a singleton is given by the preimage of the positive cone under the
fun y ↦ ⟪x, y⟫.
This is a stronger version of the Hahn-Banach separation theorem for closed convex cones. This is also the geometric interpretation of Farkas' lemma.
The inner dual of inner dual of a non-empty, closed convex cone is itself.