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
theorem
PointedCone.isClosed_dual
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommRing R]
[PartialOrder R]
[TopologicalSpace R]
[ClosedIciTopology R]
[IsOrderedRing R]
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
[TopologicalSpace N]
{p : M →ₗ[R] N →ₗ[R] R}
{s : Set M}
(hp : ∀ (x : M), Continuous ⇑(p x))
:
def
ProperCone.dual
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommRing R]
[PartialOrder R]
[IsOrderedRing R]
[TopologicalSpace R]
[ClosedIciTopology R]
[AddCommGroup M]
[Module R M]
[TopologicalSpace M]
[AddCommGroup N]
[Module R N]
[TopologicalSpace N]
(p : M →ₗ[R] N →ₗ[R] R)
[p.IsContPerfPair]
(s : Set M)
:
ProperCone R N
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
@[simp]
theorem
ProperCone.mem_dual
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommRing R]
[PartialOrder R]
[IsOrderedRing R]
[TopologicalSpace R]
[ClosedIciTopology R]
[AddCommGroup M]
[Module R M]
[TopologicalSpace M]
[AddCommGroup N]
[Module R N]
[TopologicalSpace N]
{p : M →ₗ[R] N →ₗ[R] R}
[p.IsContPerfPair]
{s : Set M}
{y : N}
:
@[simp]
theorem
ProperCone.dual_empty
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommRing R]
[PartialOrder R]
[IsOrderedRing R]
[TopologicalSpace R]
[ClosedIciTopology R]
[AddCommGroup M]
[Module R M]
[TopologicalSpace M]
[AddCommGroup N]
[Module R N]
[TopologicalSpace N]
{p : M →ₗ[R] N →ₗ[R] R}
[p.IsContPerfPair]
:
@[simp]
theorem
ProperCone.dual_zero
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommRing R]
[PartialOrder R]
[IsOrderedRing R]
[TopologicalSpace R]
[ClosedIciTopology R]
[AddCommGroup M]
[Module R M]
[TopologicalSpace M]
[AddCommGroup N]
[Module R N]
[TopologicalSpace N]
{p : M →ₗ[R] N →ₗ[R] R}
[p.IsContPerfPair]
:
@[simp]
theorem
ProperCone.dual_univ
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommRing R]
[PartialOrder R]
[IsOrderedRing R]
[TopologicalSpace R]
[ClosedIciTopology R]
[AddCommGroup M]
[Module R M]
[TopologicalSpace M]
[AddCommGroup N]
[Module R N]
[TopologicalSpace N]
{p : M →ₗ[R] N →ₗ[R] R}
[p.IsContPerfPair]
[IsTopologicalRing R]
[T1Space N]
:
theorem
ProperCone.dual_le_dual
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommRing R]
[PartialOrder R]
[IsOrderedRing R]
[TopologicalSpace R]
[ClosedIciTopology R]
[AddCommGroup M]
[Module R M]
[TopologicalSpace M]
[AddCommGroup N]
[Module R N]
[TopologicalSpace N]
{p : M →ₗ[R] N →ₗ[R] R}
[p.IsContPerfPair]
{s t : Set M}
(h : t ⊆ s)
:
theorem
ProperCone.dual_singleton
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommRing R]
[PartialOrder R]
[IsOrderedRing R]
[TopologicalSpace R]
[ClosedIciTopology R]
[AddCommGroup M]
[Module R M]
[TopologicalSpace M]
[AddCommGroup N]
[Module R N]
[TopologicalSpace N]
{p : M →ₗ[R] N →ₗ[R] R}
[p.IsContPerfPair]
[IsTopologicalRing R]
[OrderClosedTopology R]
(x : M)
:
The inner dual cone of a singleton is given by the preimage of the positive cone under the
linear map p x.
theorem
ProperCone.dual_union
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommRing R]
[PartialOrder R]
[IsOrderedRing R]
[TopologicalSpace R]
[ClosedIciTopology R]
[AddCommGroup M]
[Module R M]
[TopologicalSpace M]
[AddCommGroup N]
[Module R N]
[TopologicalSpace N]
{p : M →ₗ[R] N →ₗ[R] R}
[p.IsContPerfPair]
(s t : Set M)
:
theorem
ProperCone.dual_insert
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommRing R]
[PartialOrder R]
[IsOrderedRing R]
[TopologicalSpace R]
[ClosedIciTopology R]
[AddCommGroup M]
[Module R M]
[TopologicalSpace M]
[AddCommGroup N]
[Module R N]
[TopologicalSpace N]
{p : M →ₗ[R] N →ₗ[R] R}
[p.IsContPerfPair]
(x : M)
(s : Set M)
:
theorem
ProperCone.dual_iUnion
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommRing R]
[PartialOrder R]
[IsOrderedRing R]
[TopologicalSpace R]
[ClosedIciTopology R]
[AddCommGroup M]
[Module R M]
[TopologicalSpace M]
[AddCommGroup N]
[Module R N]
[TopologicalSpace N]
{p : M →ₗ[R] N →ₗ[R] R}
[p.IsContPerfPair]
{ι : Sort u_4}
(f : ι → Set M)
:
theorem
ProperCone.dual_sUnion
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommRing R]
[PartialOrder R]
[IsOrderedRing R]
[TopologicalSpace R]
[ClosedIciTopology R]
[AddCommGroup M]
[Module R M]
[TopologicalSpace M]
[AddCommGroup N]
[Module R N]
[TopologicalSpace N]
{p : M →ₗ[R] N →ₗ[R] R}
[p.IsContPerfPair]
(S : Set (Set M))
:
theorem
ProperCone.subset_dual_dual
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommRing R]
[PartialOrder R]
[IsOrderedRing R]
[TopologicalSpace R]
[ClosedIciTopology R]
[AddCommGroup M]
[Module R M]
[TopologicalSpace M]
[AddCommGroup N]
[Module R N]
[TopologicalSpace N]
{p : M →ₗ[R] N →ₗ[R] R}
[p.IsContPerfPair]
{s : Set M}
:
Any set is a subset of its double dual cone.
theorem
ProperCone.hyperplane_separation
{E : Type u_1}
[TopologicalSpace E]
[AddCommGroup E]
[IsTopologicalAddGroup E]
[Module ℝ E]
[ContinuousSMul ℝ E]
[LocallyConvexSpace ℝ E]
{K : Set E}
(C : ProperCone ℝ E)
(hKconv : Convex ℝ K)
(hKcomp : IsCompact K)
(hKC : Disjoint K ↑C)
:
∃ (f : StrongDual ℝ E), (∀ x ∈ C, 0 ≤ f x) ∧ ∀ x ∈ K, f x < 0
Geometric interpretation of Farkas' lemma. Also stronger version of the Hahn-Banach separation theorem for proper cones.
theorem
ProperCone.hyperplane_separation_point
{E : Type u_1}
[TopologicalSpace E]
[AddCommGroup E]
[IsTopologicalAddGroup E]
[Module ℝ E]
[ContinuousSMul ℝ E]
[LocallyConvexSpace ℝ E]
{x₀ : E}
(C : ProperCone ℝ E)
(hx₀ : x₀ ∉ C)
:
∃ (f : StrongDual ℝ E), (∀ x ∈ C, 0 ≤ f x) ∧ f x₀ < 0
Geometric interpretation of Farkas' lemma. Also stronger version of the Hahn-Banach separation theorem for proper cones.
@[simp]
theorem
ProperCone.dual_flip_dual
{E : Type u_1}
{F : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[IsTopologicalAddGroup E]
[TopologicalSpace F]
[AddCommGroup F]
[Module ℝ E]
[ContinuousSMul ℝ E]
[LocallyConvexSpace ℝ E]
[Module ℝ F]
(p : E →ₗ[ℝ] F →ₗ[ℝ] ℝ)
[p.IsContPerfPair]
(C : ProperCone ℝ E)
:
The double dual of a proper cone is itself.
@[simp]
theorem
ProperCone.dual_dual_flip
{E : Type u_1}
{F : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[IsTopologicalAddGroup E]
[TopologicalSpace F]
[AddCommGroup F]
[Module ℝ E]
[ContinuousSMul ℝ E]
[LocallyConvexSpace ℝ E]
[Module ℝ F]
(p : F →ₗ[ℝ] E →ₗ[ℝ] ℝ)
[p.IsContPerfPair]
(C : ProperCone ℝ E)
:
The double dual of a proper cone is itself.