Boundedness of a polar

Over a dual pair of finite-dimensional spaces, the polar C° of a closed convex set containing the origin is bounded exactly when the origin is interior to C: polarity trades boundedness on one side for interiority on the other.

Main results

• isBounded_polarSet_iff_zero_mem_interior — C° is bounded if and only if 0 ∈ int C (Corollary 14.5.1 in [^1]). isBounded_iff_zero_mem_interior_polarSet is the dual statement.

References

[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §14.

theorem Tdaf.ConvexAnalysis.isBounded_polarSet_iff_zero_mem_interior {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] {C : Set E} (hconv : Convex ℝ C) (hcl : IsClosed C) (h0 : 0 ∈ C) : Bornology.IsBounded (polarSet B C) ↔ 0 ∈ interior C

For a closed convex set C containing the origin, the polar C° is bounded if and only if the origin is interior to C.

Finite dimension is genuine: it is what isBounded_iff_recessionCone_eq_zero costs, and what turns "the cone generated by C° is dense" into "it is everything".

theorem Tdaf.ConvexAnalysis.isBounded_iff_zero_mem_interior_polarSet {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] {C : Set E} (hconv : Convex ℝ C) (hcl : IsClosed C) (h0 : 0 ∈ C) : Bornology.IsBounded C ↔ 0 ∈ interior (polarSet B C)

The dual form: C is bounded if and only if the origin is interior to C°.