Documentation

Mathlib.Geometry.Convex.Cone.Dual

The algebraic dual of a cone #

Given a bilinear pairing p between two R-modules M and N and a set s in M, we define PointedCone.dual p C to be the pointed 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. This is developed here. When the pairing is continuous and perfect (as a continuous pairing), this gives us the topological dual instead. See Mathlib/Analysis/Convex/Cone/Dual.lean for that case.

Implementation notes #

We do not provide a ConvexCone-valued version of PointedCone.dual since the dual cone of any set always contains 0, ie is a pointed cone. Furthermore, the strict version {y | ∀ x ∈ s, 0 < p x y} is a candidate to the name ConvexCone.dual.

TODO #

Deduce from dual_flip_dual_dual_flip that polyhedral cones are invariant under taking double duals

source
def PointedCone.dual {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (p : M →ₗ[R] N →ₗ[R] R) (s : Set M) :
PointedCone R N

The dual cone of a set s with respect to a bilinear 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 PointedCone.mem_dual {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} {s : Set M} {y : N} :
    y ∈ dual p s ↔ ∀ ⦃x : M⦄, x ∈ s → 0 ≤ (p x) y
    source
    @[simp]
    theorem PointedCone.dual_empty {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} :
    dual p ∅ = ⊤
    source
    @[simp]
    theorem PointedCone.dual_zero {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} :
    dual p 0 = ⊤
    source
    theorem PointedCone.dual_univ {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} (hp : Function.Injective ⇑p.flip) :
    dual p Set.univ = 0
    source
    theorem PointedCone.dual_le_dual {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} {s t : Set M} (h : t ⊆ s) :
    dual p s ≤ dual p t
    source
    theorem PointedCone.dual_singleton {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} (x : M) :
    dual p {x} = comap (p 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 PointedCone.dual_union {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} (s t : Set M) :
    dual p (s ∪ t) = dual p s ⊓ dual p t
    source
    theorem PointedCone.dual_insert {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} (x : M) (s : Set M) :
    dual p (insert x s) = dual p {x} ⊓ dual p s
    source
    theorem PointedCone.dual_iUnion {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} {ι : Sort u_4} (f : ι → Set M) :
    dual p (⋃ (i : ι), f i) = ⨅ (i : ι), dual p (f i)
    source
    theorem PointedCone.dual_sUnion {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} (S : Set (Set M)) :
    dual p (⋃₀ S) = sInf (dual p '' S)
    source
    theorem PointedCone.dual_eq_iInter_dual_singleton {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} (s : Set M) :
    ↑(dual p s) = ⋂ (i : ↑s), ↑(dual p {↑i})

    The dual cone of s equals the intersection of dual cones of the points in s.

    source
    theorem PointedCone.subset_dual_dual {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} {s : Set M} :
    s ⊆ ↑(dual p.flip ↑(dual p s))

    Any set is a subset of its double dual cone.

    source
    @[simp]
    theorem PointedCone.dual_dual_flip_dual {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} (s : Set M) :
    dual p ↑(dual p.flip ↑(dual p s)) = dual p s
    source
    @[simp]
    theorem PointedCone.dual_flip_dual_dual_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} (s : Set N) :
    dual p.flip ↑(dual p ↑(dual p.flip s)) = dual p.flip s
    source
    @[simp]
    theorem PointedCone.dual_span {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {p : M →ₗ[R] N →ₗ[R] R} (s : Set M) :
    dual p ↑(Submodule.span { c : R // 0 ≤ c } s) = dual p s