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 #

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)

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
    @[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 s0 (p x) y
    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

    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 sdual 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.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[] ), (∀ xC, 0 f x) xK, 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[] ), (∀ xC, 0 f x) f x₀ < 0

    Geometric interpretation of Farkas' lemma. Also stronger version of the Hahn-Banach separation theorem for proper cones.

    @[simp]

    The double dual of a proper cone is itself.

    @[simp]

    The double dual of a proper cone is itself.