Documentation

Atlas.AnAlgorithmistsToolkit.code.PolarBody

source
def ConvexGeometry.polarBody {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : Set E) :
Set E
Instances For
    source
    theorem ConvexGeometry.subset_polarBody_polarBody {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : Set E) :
    K ⊆ polarBody (polarBody K)
    source
    theorem ConvexGeometry.polarBody_polarBody_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {K : Set E} (hK_convex : Convex ℝ K) (hK_closed : IsClosed K) (hK_zero : 0 ∈ K) :
    polarBody (polarBody K) = K