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)) : IsClosed ↑(dual p s)

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' := ⋯ }

@[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} : y ∈ dual p s ↔ ∀ ⦃x : M⦄, x ∈ s → 0 ≤ (p x) y

@[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] : dual p ∅ = ⊤

@[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] : dual p 0 = ⊤

@[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] : dual p Set.univ = ⊥

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) : dual p s ≤ dual p t

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) : dual p {x} = comap (p.toContPerfPair x) (positive R R)

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) : dual p (s ∪ t) = dual p s ⊓ dual p t

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) : dual p (insert x s) = dual p {x} ⊓ dual p s

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) : dual p (⋃ (i : ι), f i) = ⨅ (i : ι), dual p (f i)

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)) : dual p (⋃₀ S) = sInf (dual p '' S)

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} : s ⊆ ↑(dual p.flip ↑(dual p s))

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 : E →L[ℝ] ℝ), (∀ 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 : E →L[ℝ] ℝ), (∀ 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) : dual p.flip ↑(dual p ↑C) = C

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) : dual p ↑(dual p.flip ↑C) = C

The double dual of a proper cone is itself.