Documentation

Mathlib.Analysis.Convex.Cone.InnerDual

Convex cones in inner product spaces #

We define Set.innerDualCone to be the cone consisting of all points y such that for all points x in a given set 0 ≤ ⟪ x, y ⟫.

Main statements #

We prove the following theorems:

The dual cone #

The dual cone is the cone consisting of all points y such that for all points x in a given set 0 ≤ ⟪ x, y ⟫.

Equations
  • s.innerDualCone = { carrier := {y : H | xs, 0 x, y⟫_}, smul_mem' := , add_mem' := }
Instances For
    @[simp]
    theorem mem_innerDualCone {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace H] (y : H) (s : Set H) :
    y s.innerDualCone xs, 0 x, y⟫_
    @[simp]
    theorem innerDualCone_empty {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace H] :
    .innerDualCone =
    @[simp]

    Dual cone of the convex cone {0} is the total space.

    @[simp]
    theorem innerDualCone_univ {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace H] :
    Set.univ.innerDualCone = 0

    Dual cone of the total space is the convex cone {0}.

    theorem innerDualCone_le_innerDualCone {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace H] (s : Set H) (t : Set H) (h : t s) :
    s.innerDualCone t.innerDualCone
    theorem pointed_innerDualCone {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace H] (s : Set H) :
    s.innerDualCone.Pointed

    The inner dual cone of a singleton is given by the preimage of the positive cone under the linear map fun y ↦ ⟪x, y⟫.

    theorem innerDualCone_union {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace H] (s : Set H) (t : Set H) :
    (s t).innerDualCone = s.innerDualCone t.innerDualCone
    theorem innerDualCone_insert {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace H] (x : H) (s : Set H) :
    (insert x s).innerDualCone = {x}.innerDualCone s.innerDualCone
    theorem innerDualCone_iUnion {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace H] {ι : Sort u_6} (f : ιSet H) :
    (⋃ (i : ι), f i).innerDualCone = ⨅ (i : ι), (f i).innerDualCone
    theorem innerDualCone_sUnion {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace H] (S : Set (Set H)) :
    (⋃₀ S).innerDualCone = sInf (Set.innerDualCone '' S)
    theorem innerDualCone_eq_iInter_innerDualCone_singleton {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace H] (s : Set H) :
    s.innerDualCone = ⋂ (i : s), {i}.innerDualCone

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

    theorem isClosed_innerDualCone {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace H] (s : Set H) :
    IsClosed s.innerDualCone
    theorem ConvexCone.pointed_of_nonempty_of_isClosed {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace H] (K : ConvexCone H) (ne : (K).Nonempty) (hc : IsClosed K) :
    K.Pointed
    theorem ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_nmem {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace H] [CompleteSpace H] (K : ConvexCone H) (ne : (K).Nonempty) (hc : IsClosed K) {b : H} (disj : bK) :
    ∃ (y : H), (xK, 0 x, y⟫_) y, b⟫_ < 0

    This is a stronger version of the Hahn-Banach separation theorem for closed convex cones. This is also the geometric interpretation of Farkas' lemma.

    theorem ConvexCone.innerDualCone_of_innerDualCone_eq_self {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace H] [CompleteSpace H] (K : ConvexCone H) (ne : (K).Nonempty) (hc : IsClosed K) :
    ((K).innerDualCone).innerDualCone = K

    The inner dual of inner dual of a non-empty, closed convex cone is itself.