def Set.orthogonalSet {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (C : Set E) : Set E

The orthogonal set of a subset of a real inner product space, corresponding to the textbook notation C^⊥.

def Set.«term_^⊥» : Lean.TrailingParserDescr

theorem Set.mem_orthogonalSet {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {C : Set E} {u : E} : u ∈ C.orthogonalSet ↔ ∀ x ∈ C, inner ℝ x u = 0

Membership in the orthogonal set means being orthogonal to every point of the original set.

@[reducible, inline]

abbrev Set.positivePolar {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (C : Set E) : Set E

The positive polar cone of a subset of a real Hilbert space, corresponding to the textbook notation C^⊕.

@[reducible, inline]

abbrev Set.negativePolar {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (C : Set E) : Set E

The negative polar cone of a subset of a real Hilbert space, corresponding to the textbook notation C^⊖.

theorem Set.mem_positivePolar {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {C : Set E} {u : E} : u ∈ C.positivePolar ↔ ∀ x ∈ C, 0 ≤ inner ℝ x u

Membership in the positive polar cone means having nonnegative inner product with every point of the original set.

theorem Set.mem_negativePolar {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {C : Set E} {u : E} : u ∈ C.negativePolar ↔ ∀ x ∈ C, inner ℝ x u ≤ 0

Membership in the negative polar cone means having nonpositive inner product with every point of the original set.

theorem Set.negativePolar_subset_of_subset {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {C D : Set E} (hDC : D ⊆ C) : C.negativePolar ⊆ D.negativePolar

Proposition 6.24 (1): textbook clause (i) for the negative polar cone. If D ⊆ C, then C^⊖ ⊆ D^⊖.

theorem Set.positivePolar_subset_of_subset {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {C D : Set E} (hDC : D ⊆ C) : C.positivePolar ⊆ D.positivePolar

Proposition 6.24 (2): textbook clause (i) for the positive polar cone. If D ⊆ C, then C^⊕ ⊆ D^⊕.

theorem Set.negativePolar_nonempty {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (C : Set E) : C.negativePolar.Nonempty

Proposition 6.24 (3): textbook clause (ii). The negative polar cone is nonempty.

theorem Set.positivePolar_nonempty {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (C : Set E) : C.positivePolar.Nonempty

Proposition 6.24 (4): textbook clause (ii). The positive polar cone is nonempty.

theorem Set.negativePolar_isClosed {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (C : Set E) : IsClosed C.negativePolar

Proposition 6.24 (5): textbook clause (ii). The negative polar cone is closed.

theorem Set.positivePolar_isClosed {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (C : Set E) : IsClosed C.positivePolar

Proposition 6.24 (6): textbook clause (ii). The positive polar cone is closed.

theorem Set.negativePolar_convex {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (C : Set E) : Convex ℝ C.negativePolar

Proposition 6.24 (7): textbook clause (ii). The negative polar cone is convex.

theorem Set.positivePolar_convex {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (C : Set E) : Convex ℝ C.positivePolar

Proposition 6.24 (8): textbook clause (ii). The positive polar cone is convex.

theorem Set.negativePolar_isCone {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (C : Set E) : IsCone C.negativePolar

Proposition 6.24 (9): textbook clause (ii). The negative polar cone is a cone.

theorem Set.positivePolar_isCone {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (C : Set E) : IsCone C.positivePolar

Proposition 6.24 (10): textbook clause (ii). The positive polar cone is a cone.

theorem Set.negativePolar_cone_eq {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (C : Set E) : C.cone.negativePolar = C.negativePolar

Proposition 6.24 (11): textbook clause (iii) for the conical hull. The negative polar cone is unchanged by replacing C with cone C.

theorem Set.negativePolar_convexHull_eq {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (C : Set E) : ((convexHull ℝ) C).negativePolar = C.negativePolar

Proposition 6.24 (12): textbook clause (iii) for the convex hull. The negative polar cone is unchanged by replacing C with conv C, represented in Lean by convexHull ℝ C.

theorem Set.negativePolar_closure_eq {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (C : Set E) : (closure C).negativePolar = C.negativePolar

Proposition 6.24 (13): textbook clause (iii) for the closure. The negative polar cone is unchanged by replacing C with closure C.

theorem Set.negativePolar_inter_positivePolar_eq_orthogonalSet {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (C : Set E) : C.negativePolar ∩ C.positivePolar = C.orthogonalSet

Proposition 6.24 (14): textbook clause (iv). The intersection of the negative and positive polar cones is the orthogonal set of C.

theorem Set.negativePolar_eq_positivePolar_of_closure_cone_eq_neg {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {C : Set E} (hC_symm : closure C.cone = -closure C.cone) : C.negativePolar = C.positivePolar

Proposition 6.24 (15): textbook clause (v). If closure (cone C) is symmetric, then the negative and positive polar cones of C coincide.

theorem Set.positivePolar_eq_orthogonalSet_of_closure_cone_eq_neg {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {C : Set E} (hC_symm : closure C.cone = -closure C.cone) : C.positivePolar = C.orthogonalSet

Proposition 6.24 (16): textbook clause (v). If closure (cone C) is symmetric, then the positive polar cone of C equals the orthogonal set of C.