Polar sets

DefinitionPolar of a set#✓fully proved

Let \(E\) be a real inner product space. The polar of a set \(A \subseteq E\) is the set \(A^\circ = \{y \in E : \langle x, y \rangle \le 1 \text{ for all } x \in A\}\). This uses the one-sided bound \(\langle x, y \rangle \le 1\), not \(|\langle x, y \rangle| \le 1\).

def polarSet (A : Set E) : Set E := {y | ∀ x ∈ A, inner ℝ x y ≤ 1}

Used by 7

Used byMembership in the polar · The closed unit ball is self-polar · The polar of the cube is the \(\ell^1\) unit ball · Polar of the empty set · Polar of a linear image · The polar reverses inclusion · The origin lies in every polar

TheoremMembership in the polar#✓fully proved

Let \(E\) be a real inner product space, \(A \subseteq E\) and \(y \in E\). Then \(y\) lies in the polar \(A^\circ\) of \(A\) if and only if \(\langle x, y \rangle \le 1\) for every \(x \in A\).

theorem mem_polarSet {A : Set E} {y : E} :
    y ∈ polarSet A ↔ ∀ x ∈ A, inner ℝ x y ≤ 1

Uses 1

Statement usesPolar of a set

TheoremPolar of the empty set#✓fully proved

In a real inner product space \(E\), the polar of the empty set is all of \(E\), since the defining condition is vacuous.

@[simp] theorem polarSet_empty : polarSet (∅ : Set E) = Set.univ

Uses 1

Statement usesPolar of a set

TheoremThe origin lies in every polar#✓fully proved

In a real inner product space \(E\), for every set \(A \subseteq E\) the origin \(0\) lies in the polar \(A^\circ\) of \(A\), since \(\langle x, 0 \rangle = 0 \le 1\) for every \(x \in A\).

@[simp] theorem zero_mem_polarSet (A : Set E) : (0 : E) ∈ polarSet A

Uses 1

Statement usesPolar of a set

TheoremThe polar reverses inclusion#✓fully proved

Let \(A\) and \(B\) be subsets of a real inner product space. If \(A \subseteq B\), then the polar \(B^\circ\) of \(B\) is contained in the polar \(A^\circ\) of \(A\).

theorem polarSet_subset_polarSet {A B : Set E} (h : A ⊆ B) :
    polarSet B ⊆ polarSet A

Uses 1

Statement usesPolar of a set

TheoremThe closed unit ball is self-polar#✓fully proved

In a real inner product space \(E\), the polar of the closed unit ball \(\{x \in E : \|x\| \le 1\}\) is the closed unit ball itself.

theorem polarSet_closedUnitBall :
    polarSet (Metric.closedBall (0 : E) 1) = Metric.closedBall 0 1

Uses 1

Statement usesPolar of a set

TheoremThe polar of the cube is the \(\ell^1\) unit ball#✓fully proved

For every \(n\), the polar of the coordinate cube \([-1, 1]^n\) in the Euclidean space \(\mathbb{R}^n\), that is the set of all \(y\) with \(\langle x, y \rangle \le 1\) for every \(x\) in the cube, is the closed \(\ell^1\) unit ball \(\{y \in \mathbb{R}^n : \sum_i |y_i| \le 1\}\).

theorem polarSet_coordinateCube (n : ℕ) :
    polarSet (ConvexCovering.coordinateCube n) =
      {y : EuclideanSpace ℝ (Fin n) | ∑ i, |y i| ≤ 1}

Uses 3

Statement usesCoordinate cube · Polar of a set

Proof usesThe coordinate cube as an absolute-value box

TheoremPolar of a linear image#✓fully proved

Let \(E\) and \(F\) be finite-dimensional real inner product spaces, let \(f : E \to F\) be a linear map with adjoint \(f^* : F \to E\), and let \(K \subseteq E\). Writing \(S^\circ\) for the polar of a set \(S\), we have \((f(K))^\circ = (f^*)^{-1}(K^\circ)\), that is, \(y \in F\) lies in the polar of \(f(K)\) if and only if \(f^*(y)\) lies in the polar of \(K\).

This is the set-theoretic transformation used by the Mahler volume product.

theorem polarSet_image_eq_preimage_adjoint (f : E →ₗ[ℝ] F) (K : Set E) :
    polarSet (f '' K) = f.adjoint ⁻¹' polarSet K

Uses 1

Statement usesPolar of a set

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.