Documentation

Mathlib.Analysis.Convex.Cone.Dual

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 #

source
def Set.innerDualCone {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (s : Set H) :
ConvexCone ℝ H

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

Instances For
    source
    @[simp]
    theorem mem_innerDualCone {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (y : H) (s : Set H) :
    y ∈ Set.innerDualCone s ↔ ∀ (x : H), x ∈ s → 0 ≤ inner x y
    source
    @[simp]
    theorem innerDualCone_empty {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace ℝ H] :
    Set.innerDualCone ∅ = ⊤
    source
    @[simp]
    theorem innerDualCone_zero {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace ℝ H] :
    Set.innerDualCone 0 = ⊤

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

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

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

    source
    theorem innerDualCone_le_innerDualCone {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (s : Set H) (t : Set H) (h : t ⊆ s) :
    Set.innerDualCone s ≤ Set.innerDualCone t
    source
    theorem pointed_innerDualCone {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (s : Set H) :
    ConvexCone.Pointed (Set.innerDualCone s)
    source
    theorem innerDualCone_singleton {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (x : H) :
    Set.innerDualCone {x} = ConvexCone.comap (↑(innerₛₗ ℝ) x) (ConvexCone.positive ℝ ℝ)

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

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

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

    source
    theorem isClosed_innerDualCone {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (s : Set H) :
    IsClosed ↑(Set.innerDualCone s)
    source
    theorem ConvexCone.pointed_of_nonempty_of_isClosed {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (K : ConvexCone ℝ H) (ne : Set.Nonempty ↑K) (hc : IsClosed ↑K) :
    ConvexCone.Pointed K
    source
    theorem ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_nmem {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (K : ConvexCone ℝ H) (ne : Set.Nonempty ↑K) (hc : IsClosed ↑K) {b : H} (disj : ¬b ∈ K) :
    ∃ y, (∀ (x : H), x ∈ K → 0 ≤ inner x y) ∧ inner 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.

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

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