The topological dual of a cone and Farkas' lemma #
Given a continuous bilinear pairing p
between two R
-modules M
and N
and a set s
in M
,
we define ProperCone.dual p C
to be the proper cone in N
consisting of all points y
such that
0 ≤ p x y
for all x ∈ s
.
When the pairing is perfect, this gives us the algebraic dual of a cone.
See Mathlib/Geometry/Convex/Cone/Dual.lean
for that case.
When the pairing is continuous and perfect (as a continuous pairing), this gives us the topological
dual instead. This is developed here.
We prove Farkas' lemma, which says that a proper cone C
in a locally convex topological real
vector space E
and a point x₀
not in C
can be separated by a hyperplane. This is a geometric
interpretation of the Hahn-Banach separation theorem.
As a corollary, we prove that the double dual of a proper cone is itself.
Main statements #
We prove the following theorems:
ProperCone.hyperplane_separation
,ProperCone.hyperplane_separation_point
: Farkas lemma.ProperCone.dual_dual_flip
,ProperCone.dual_flip_dual
: The double dual of a proper cone.
References #
- https://en.wikipedia.org/wiki/Hyperplane_separation_theorem
- https://en.wikipedia.org/wiki/Farkas%27_lemma#Geometric_interpretation
The dual cone of a set s
with respect to a perfect pairing p
is the cone consisting of all
points y
such that for all points x ∈ s
we have 0 ≤ p x y
.
Equations
- ProperCone.dual p s = { toSubmodule := PointedCone.dual p s, isClosed' := ⋯ }
Instances For
The inner dual cone of a singleton is given by the preimage of the positive cone under the
linear map p x
.
Any set is a subset of its double dual cone.
Geometric interpretation of Farkas' lemma. Also stronger version of the Hahn-Banach separation theorem for proper cones.
Geometric interpretation of Farkas' lemma. Also stronger version of the Hahn-Banach separation theorem for proper cones.
The double dual of a proper cone is itself.
The double dual of a proper cone is itself.