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