innerDualCone_zero
theorem innerDualCone_zero :
∀ {H : Type u_5} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℝ H], Set.innerDualCone 0 = ⊤
The theorem `innerDualCone_zero` states that for any type `H` that is a normed add commutative group and has an inner product space over the real numbers, the dual cone of the convex cone consisting only of the zero vector is the whole space `H`. In other words, any point `y` in space `H` satisfies the condition that the inner product of `y` and `0` is nonnegative, hence all points `y` in `H` belong to the dual cone of the zero vector.
More concisely: The dual cone of the zero vector in a real inner product space over a normed additive commutative group equals the entire space.
|
innerDualCone_singleton
theorem innerDualCone_singleton :
∀ {H : Type u_5} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℝ H] (x : H),
{x}.innerDualCone = ConvexCone.comap ((innerₛₗ ℝ) x) (ConvexCone.positive ℝ ℝ)
The theorem `innerDualCone_singleton` states that for any vector space `H`, which is a normed additive commutative group and an inner product space over the real numbers, and for any vector `x` in `H`, the inner dual cone of `{x}` (the set containing only `x`) is equivalent to the preimage of the positive cone in the real numbers under the linear map that takes a vector `y` to the inner product of `x` and `y`.
In simpler terms, this theorem describes a relationship between the inner dual cone of a singleton set and the positive cone in the real numbers. The positive cone is a set of non-negative elements, and the inner dual cone is a set derived from a given set (in this case a singleton set) by a specific operation involving the inner product operation. The theorem states that this inner dual cone can be obtained by mapping each element from the positive cone under a specific linear map and then looking at its inverse images. The linear map is defined by the inner product with the vector `x`.
More concisely: The inner dual cone of a singleton set {x} in a real inner product space H is equal to the preimage of the positive real numbers under the linear map taking a vector y to the inner product of x and y.
|
innerDualCone_univ
theorem innerDualCone_univ :
∀ {H : Type u_5} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℝ H], Set.univ.innerDualCone = 0 := by
sorry
This theorem states that for any type `H` that has a normed additive commutative group structure and an inner product space structure over the real numbers, the dual cone of the universal set (which contains all elements of type `H`) is the convex cone {0}. In other words, when you apply the operation of "inner dual cone" to the universal set in this context, you always get the convex cone consisting only of the zero element.
More concisely: For any normed additive commutative group `H` with an inner product space structure over the real numbers, the dual cone of its universal set is the trivial cone consisting only of the origin.
|
ConvexCone.innerDualCone_of_innerDualCone_eq_self
theorem ConvexCone.innerDualCone_of_innerDualCone_eq_self :
∀ {H : Type u_5} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℝ H] [inst_2 : CompleteSpace H]
(K : ConvexCone ℝ H), (↑K).Nonempty → IsClosed ↑K → (↑(↑K).innerDualCone).innerDualCone = K
This theorem states that for any non-empty, closed convex cone `K` in a complete inner product space over the real numbers with a normed add comm group structure, the inner dual of the inner dual of `K` is equal to `K` itself. In other words, applying the inner dual operation twice on `K` results in the original cone `K`.
More concisely: The inner dual of a non-empty, closed, convex cone in a complete inner product space over the real numbers is equal to the original cone.
|
innerDualCone_eq_iInter_innerDualCone_singleton
theorem innerDualCone_eq_iInter_innerDualCone_singleton :
∀ {H : Type u_5} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℝ H] (s : Set H),
↑s.innerDualCone = ⋂ i, ↑{↑i}.innerDualCone
The theorem `innerDualCone_eq_iInter_innerDualCone_singleton` states that for any set `s` of elements from a type `H`, where `H` forms a normed commutative additive group and an inner product space over the real numbers (`ℝ`), the dual cone of `s` (represented by `s.innerDualCone`) is identical to the intersection of the dual cones of the individual points in `s` (represented by `⋂ i, ↑{↑i}.innerDualCone`). In simple terms, the dual cone of the set is the intersection of the dual cones of its elements.
More concisely: For any set `s` of elements in a normed commutative additive group and inner product space over the real numbers, the dual cone of `s` equals the intersection of the dual cones of its elements.
|
ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_nmem
theorem ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_nmem :
∀ {H : Type u_5} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℝ H] [inst_2 : CompleteSpace H]
(K : ConvexCone ℝ H),
(↑K).Nonempty → IsClosed ↑K → ∀ {b : H}, b ∉ K → ∃ y, (∀ x ∈ K, 0 ≤ ⟪x, y⟫_ℝ) ∧ ⟪y, b⟫_ℝ < 0
The theorem `ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_nmem` states that, given a convex cone `K` in a complete inner product space over the real numbers, if `K` is nonempty and closed, and if a point `b` is not in `K`, then there exists a hyperplane that separates `b` from `K`. More formally, there exists a vector `y` such that for all `x` in `K`, the inner product of `x` and `y` is nonnegative, while the inner product of `y` and `b` is negative. This theorem is a stronger version of the Hahn-Banach separation theorem for closed convex cones and represents the geometric interpretation of Farkas' lemma.
More concisely: Given a nonempty and closed convex cone K in a complete inner product space over the real numbers, if there exists a point b not in K, then there exists a hyperplane separating b from K.
|