Polars of convex sets and convex cones #
The polar of a convex cone K is K° = {y ∣ ∀ x ∈ K, ⟨x, y⟩ ≤ 0}, and the polar of a convex
set C containing the origin is C° = {y ∣ ∀ x ∈ C, ⟨x, y⟩ ≤ 1}. Polarity is what conjugacy
becomes on indicator functions: the indicator of a cone is positively homogeneous, so its conjugate
is again an indicator, and the set it indicates is the polar. The bipolar theorem K°° = cl K
follows from that together with separation. The further polarity theorems need the recession
function or the gauge and are proved in Recession/Conjugate.lean, Duality/HomConePolar.lean,
Duality/Level.lean, Duality/Gauge.lean and Duality/PolarBounded.lean.
Main definitions #
polarCone B K,polarSet B C— the two polars above;polarPointedCone B Kbundles the first as aPointedCone ℝ FandpolarSubmodule B Mbundles the polar of a subspace.gc_polarCone_polarCone,polarConeClosure— polarity as an antitone Galois connection betweenSet EandSet F, and the closure operatorK ↦ K°°it induces; likewisegc_polarSet_polarSetandpolarSetClosure.
Main results #
isClosed_polarCone,polarPointedCone,polarCone_polarCone,conj_indicatorFn_eq_indicatorFn_polarCone— the three assertions of the bipolar theorem (Theorem 14.1 in [^1]):K°is a nonempty closed convex cone for anyK;K°° = cl Kfor a nonempty convex cone; and the indicator functions ofKandK°are conjugate.neg_polarCone_neg_polarConeisK** = Kfor the dual coneK* = -K°.polarSet_polarSet—C°° = Cfor a closed convexCcontaining the origin (Theorem 14.5 in [^1]).polarCone_eq_setOf_supportFn_le_zero— the polar is the zero sublevel set of the support function, for an arbitrary set: this is what turns a theorem computing a support function into a theorem computing a polar.polarSet_closure,polarSet_union,polarSet_convexHull,polarSet_smul,polarCone_add— the lattice and scaling identities. A polar is an intersection of closed half-spaces, so polarity does not see the convex hull.polarCone_coe_submodule,polarCone_hull_range,polarCone_setOf_forall_le_zero,polarCone_nonnegOrthant— the standard examples: the polar of a subspace is its annihilator, the polar of a generated cone is the solution set of the corresponding homogeneous inequalities and conversely, and the polar of the nonnegative orthant is the nonpositive orthant.conj_partialAffineFn— the conjugate of a partial affine function,(δ(· ∣ L + a) + ⟨·, a*⟩ + α)* = δ(· ∣ L^⊥ + a*) + ⟨a, ·⟩ + α*.
Implementation notes #
Every bipolar statement takes Convex ℝ K, ∀ a > 0, a • K = K and K.Nonempty separately,
because that is the generality in which the separation argument runs; a PointedCone ℝ E supplies
all three, and each statement has a _pointedCone companion. K°° = cl K, not K°° = K, is the
theorem, and nonemptiness of K is genuinely needed: ∅° = F, and F° is the kernel of the
pairing rather than cl ∅ = ∅. The adjunction L ⊆ K° ↔ K ⊆ L° makes K ↦ K°° a
ClosureOperator (Set E), with the OrderDual on the codomain rather than the domain because
the indicator embedding s ↦ δ(· ∣ s) is antitone.
Two Mathlib objects are close but different. PointedCone.dual is the inner dual, so
K° = -(Kᵛ) (polarPointedCone_eq_dual_neg); the bipolar theorem proved here asks for
IsCompatiblePairing rather than a perfect pairing, and closedness of the polar needs only
IsContinuousPairing. LinearMap.polar is the absolute polar, which agrees with polarSet
exactly on balanced sets (polarSet_eq_polar_of_balanced).
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §14.
Definitions #
The polar of a convex cone: K° = {y | ∀ x ∈ K, ⟨x, y⟩ ≤ 0}. This is a one-sided polar,
neither Mathlib's absolute polar LinearMap.polar nor its inner dual cone, of which it is the
negative (polarPointedCone_eq_dual_neg).
Instances For
For a cone the two polars coincide, because the half-space {x | ⟨x, y⟩ ≤ 1} contains a
cone exactly when {x | ⟨x, y⟩ ≤ 0} does.
Polarity as a Galois connection #
Polarity of cones is an antitone Galois connection between Set E and Set F.
Polarity of sets is an antitone Galois connection between Set E and Set F.
The bipolar operator K ↦ K°° as a ClosureOperator on Set E. Its closed elements are, by
polarCone_polarCone_of_isClosed, the nonempty closed convex cones.
Equations
Instances For
The bipolar operator C ↦ C°° as a ClosureOperator on Set E. Its closed elements are, by
polarSet_polarSet, the closed convex sets containing the origin.
Equations
Instances For
Polarity is unchanged by taking the bipolar first — the triangle identity of the
adjunction, and Rockafellar's (cl K)° = K° in its purely algebraic form.
Polarity is an order anti-isomorphism between the bipolar-closed sets. The bipolar theorem
with its order structure and with no topology; once E and F carry compatible topologies the
bipolar-closed sets are exactly the closed convex cones containing the origin.
Equations
Instances For
The polar cone as a PointedCone #
The polar of an arbitrary set is a pointed convex cone — the first assertion of the
bipolar theorem, before any topology enters. Bundling it makes the PointedCone API available.
Equations
- Tdaf.ConvexAnalysis.polarPointedCone B K = { carrier := Tdaf.ConvexAnalysis.polarCone B K, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Instances For
A closed half-space of the pairing is convex, in the real-valued form that cuts out a polar
set; convex_setOf_pairing_le is the EReal form.
Polarity does not see the convex hull: the polar is cut out by the convex half-spaces
{x | ⟨x, y⟩ ≤ 1}. The polarCone counterpart is polarCone_hull.
The polar of a sum is the intersection of the polars, for sets containing the origin —
the additive counterpart of polarCone_union.
Negating the cone negates its polar: (-K)° = -(K°). With the bipolar theorem this makes
the dual cone K* = -K° an involution (neg_polarCone_neg_polarCone).
Bridges to Mathlib #
Mathlib's dual cone is the inner one. PointedCone.dual B s = {y | ∀ x ∈ s, 0 ≤ ⟨x, y⟩}, so
Rockafellar's polar is its negative — equivalently, the dual of -K.
Mathlib's LinearMap.polar is the absolute polar {y | ∀ x ∈ C, ‖⟨x, y⟩‖ ≤ 1}. It agrees
with Rockafellar's one-sided polar exactly on balanced sets, where x ∈ C implies -x ∈ C.
The polar cone and the conjugate of an indicator #
This computation needs no topology: the indicator of a
cone is positively homogeneous, so its conjugate is again an indicator
(conj_eq_indicatorFn_of_posHomogeneous), and the set it indicates is the polar.
The indicator functions of a nonempty convex cone and of its polar are conjugate to each other.
The support function of a nonempty convex cone is the indicator of its polar.
The polar is the zero sublevel set of the support function: ⟨x, y⟩ ≤ 0 for every x ∈ K
says exactly that δ*(y | K) ≤ 0. Holds for an arbitrary set K, and is what turns a theorem
computing a support function into a theorem computing a polar.
Closedness of the polar #
The polar of any set is closed, being an intersection of homogeneous closed half-spaces.
The polar does not see the closure: (cl K)° = K°.
The polar does not see the closure, in the polarSet sense — the companion of
polarCone_closure.
The bipolar theorem #
Separation supplies the only nontrivial half.
The bipolar of a nonempty convex cone is its closure.
A point outside cl K is strongly separated from it by a continuous linear functional; because
cl K is a nonempty cone, that functional is ≤ 0 on it and the separating constant is
nonnegative, so the y representing it lies in K° and detects the point.
For a nonempty closed convex cone the polarity correspondence is an involution:
K°° = K.
The same for a bundled cone: for a closed PointedCone, K°° = K. All three hypotheses of
the previous statement are supplied by the bundling.
The bipolar theorem in its dual-cone form: K** = K for a nonempty closed convex cone, where
K* = -K° is the dual cone.
The conjugacy of indicators in the remaining direction: for a nonempty closed convex cone the
indicator of K° conjugates back to the indicator of K.
The bipolar of a set containing the origin #
C°° = C for a closed convex set containing the origin. The separation argument is the same as for
cones, with the constant normalised to 1 instead of 0.
The polar of a closed convex set containing the origin is another such set, and C°° = C.
Containment of the origin is what makes the separating constant positive, so that the separating
functional can be rescaled to have value exactly 1.
Examples #
The polar of a subspace is its annihilator — the book's "orthogonally complementary
subspace". Under the pairing this is Submodule.dualAnnihilator pulled back along B.flip.
The polar of a subspace, bundled as a submodule of F: the annihilator of M pulled back
along B.flip. Its carrier is polarCone B M (polarCone_coe_submodule).
Equations
Instances For
The polar of the convex cone generated by a family aᵢ is the solution set of the
homogeneous inequalities ⟨aᵢ, y⟩ ≤ 0.
Partial affine functions #
A partial affine function is a proper convex function whose effective domain is an affine set and
which is affine on it; every such function is δ(· | L + a) + ⟨·, a*⟩ + α for a subspace L.
Conjugacy exchanges L with its polar, a with a*, and α with -α - ⟨a, a*⟩, so partial
affine functions, like subspaces, come in dual pairs. The formula is the conjugacy rule for
h(Ax) + ⟨x, b⟩ + α at h = δ(· | L), fed by conj_indicatorFn_eq_indicatorFn_polarCone.
A partial affine function in Rockafellar's normal form: δ(· | L + a) + ⟨·, b⟩ + α, for a
subspace L, vectors a and b, and a real α.
Equations
- Tdaf.ConvexAnalysis.partialAffineFn B L a b α x = Tdaf.ConvexAnalysis.indicatorFn (a +ᵥ ↑L) x + ↑((B x) b) + ↑α
Instances For
The conjugate of a partial affine function:
(δ(· | L + a) + ⟨·, a*⟩ + α)* = δ(· | L^⊥ + a*) + ⟨a, ·⟩ + α*, where α* is -α - ⟨a, a*⟩.
Dually: the polar of the solution set of the homogeneous inequalities ⟨aᵢ, y⟩ ≤ 0 is the
closure of the convex cone generated by the aᵢ.
The nonnegative orthant #
The book's second example, for a real inner-product space paired with itself.