The bipolar theorem

The bipolar of a nonempty absolutely convex set in a real or complex locally convex space is its closure. Equivalently, continuous linear functionals bounded by one on the set characterize its closure. No completeness or Hausdorff hypothesis is needed.

For an arbitrary set, the bipolar is the closed absolutely convex hull after adjoining zero. Adjoining zero matters for the empty set, since Mathlib's absolutely convex hull of the empty set is empty, whereas a bipolar always contains zero.

The pairing and both polars are Mathlib's topDualPairing, StrongDual.polar, and LinearMap.polar; no separate bipolar carrier is introduced. The separation argument uses RCLike.geometric_hahn_banach_closed_point and rotates each value of a functional by RCLike.exists_norm_eq_mul_self to pass from real-part bounds to absolute bounds.

References

• R. E. Megginson, An Introduction to Banach Space Theory, §2.6 (the bipolar theorem).
• Christopher Hoskin, Mathlib PR #26345, for the formulation for bilinear pairings with their weak topology.

theorem AbsConvex.exists_mem_polar_norm_apply_gt_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] {s : Set E} (hs : AbsConvex 𝕜 s) (hne : s.Nonempty) {x : E} (hx : x ∉ _root_.closure s) : ∃ f ∈ StrongDual.polar 𝕜 s, 1 < ‖f x‖

A point outside the closure of a nonempty absolutely convex set is separated by a continuous linear functional whose absolute value is at most one on the set and strictly greater than one at the point.

theorem AbsConvex.bipolar_eq_closure {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] {s : Set E} (hs : AbsConvex 𝕜 s) (hne : s.Nonempty) : (topDualPairing 𝕜 E).polar (StrongDual.polar 𝕜 s) = _root_.closure s

The bipolar theorem: the bipolar of a nonempty absolutely convex set equals its closure in the original locally convex topology.

theorem StrongDual.bipolar_eq_closedAbsConvexHull (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] (s : Set E) : (topDualPairing 𝕜 E).polar (polar 𝕜 s) = (closedAbsConvexHull 𝕜) (insert 0 s)

The bipolar theorem for an arbitrary set. Its bipolar is the closed absolutely convex hull of the set together with zero, including when the set is empty.

theorem StrongDual.mem_closedAbsConvexHull_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] {s : Set E} (hne : s.Nonempty) {x : E} : x ∈ (closedAbsConvexHull 𝕜) s ↔ ∀ f ∈ polar 𝕜 s, ‖f x‖ ≤ 1

Membership in a closed absolutely convex hull is tested by continuous linear functionals bounded by one on the original nonempty set.