Polars of absolutely convex hulls

The absolute polar for a bilinear pairing is unchanged by taking an absolutely convex hull. For the continuous dual pairing, taking the closed absolutely convex hull also leaves the polar unchanged. These identities let separation arguments pass between a generating set and its closed disked hull.

The results use Mathlib's LinearMap.polar_AbsConvex for the opposite polar and continuity of the functionals for closure.

@[simp]

theorem LinearMap.polar_absConvexHull {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E) : B.polar ((absConvexHull 𝕜) s) = B.polar s

Taking the absolutely convex hull does not change the absolute polar of a bilinear pairing.

@[simp]

theorem StrongDual.polar_closedAbsConvexHull {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] (s : Set E) : polar 𝕜 ((closedAbsConvexHull 𝕜) s) = polar 𝕜 s

Taking the closed absolutely convex hull does not change the absolute polar.