Documentation

LeanPool.Polytopes.Polar

Polar duals and their compactness properties.

noncomputable def pointDualLin {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (p : { p : E // p ≠ 0 }) :

{ f : StrongDual ℝ E // ‖f‖ = 1 }

The unit dual functional in the direction of a nonzero vector p.

Equations

pointDualLin p = ⟨(InnerProductSpace.toDual ℝ E) (‖↑p‖⁻¹ • ↑p), ⋯⟩

Instances For

noncomputable def pointDual {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (p : { p : E // p ≠ 0 }) :

Given a nonzero vector p, the halfspace {x | inner p x ≤ 1}.

Equations

pointDual p = { f := pointDualLin p, α := ‖↑p‖⁻¹ }

Instances For

theorem pointDual.α {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (p : { p : E // p ≠ 0 }) :

(pointDual p).α = ‖↑p‖⁻¹

theorem pointDual.h {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (p : { p : E // p ≠ 0 }) :

↑(pointDual p) = ⇑((InnerProductSpace.toDual ℝ E) (‖↑p‖⁻¹ • ↑p)) ⁻¹' {x : ℝ | x ≤ ‖↑p‖⁻¹ }

theorem pointDual_origin {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (p : { p : E // p ≠ 0 }) :

0 ∈ ↑(pointDual p)

theorem mem_pointDual {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (p : { p : E // p ≠ 0 }) (x : E) :

x ∈ ↑(pointDual p) ↔ inner ℝ (↑p) x ≤ 1

theorem pointDual_comm {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (p q : { p : E // p ≠ 0 }) :

↑p ∈ ↑(pointDual q) ↔ ↑q ∈ ↑(pointDual p)

noncomputable def polarDual {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (X : Set E) :

The polar dual of a set X: {v | ∀ x ∈ X, inner x v ≤ 1}.

Equations

polarDual X = ⋂₀ (SetLike.coe '' pointDual '' Subtype.val ⁻¹' X)

Instances For

theorem polarDual_closed {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (X : Set E) :

IsClosed (polarDual X)

theorem polarDual_convex {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (X : Set E) :

Convex ℝ (polarDual X)

theorem polarDual_origin {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (X : Set E) :

0 ∈ polarDual X

theorem mem_polarDual {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {X : Set E} {v : E} :

v ∈ polarDual X ↔ ∀ x ∈ X, inner ℝ x v ≤ 1

theorem mem_polarDual' {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {X : Set E} {v : E} :

v ∈ polarDual X ↔ ∀ x ∈ X, inner ℝ v x ≤ 1

theorem polarDual_comm_half {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (X Y : Set E) :

X ⊆ polarDual Y → Y ⊆ polarDual X

theorem polarDual_comm {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (X Y : Set E) :

X ⊆ polarDual Y ↔ Y ⊆ polarDual X

theorem doublePolarDual_self {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {X : Set E} (hXcl : IsClosed X) (hXcv : Convex ℝ X) (hX0 : 0 ∈ X) :

polarDual (polarDual X) = X

theorem polarDual_empty {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] :

polarDual ∅ = Set.univ

theorem polarDual_zero {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] :

polarDual {0} = Set.univ

theorem compact_polarDual_iff {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {X : Set E} (hXcl : IsClosed X) :

0 ∈ interior (polarDual X) ↔ IsCompact X

theorem polarDual_compact_if {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {X : Set E} (hXcl : IsClosed X) (hXcv : Convex ℝ X) :

0 ∈ interior X → IsCompact (polarDual X)