Documentation

Mathlib.Analysis.Convex.Cone.Dual

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:

References #

source
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)
source
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
    Instances For
      source
      @[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
      source
      @[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 ∅ = ⊤
      source
      @[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 = ⊤
      source
      @[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 = ⊥
      source
      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
      source
      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.

      source
      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
      source
      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
      source
      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)
      source
      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)
      source
      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.

      source
      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.

      source
      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.

      source
      @[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.

      source
      @[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.