Rockafellar, §14: Polars of Convex Sets #
The polar K° of a convex cone and the polar C° of a convex set, the bipolar theorems, and the
duality between gauges and support functions that polarity carries. All 11 numbered results of §14
are formalized.
The section's definitions #
- The polar of a convex cone
K° = {x* | ⟨x, x*⟩ ≤ 0 for every x ∈ K}is the backbone'spolarCone (pairing n), unfolded here asmem_polarCone_rn. - The polar of a convex set
C° = {x* | ⟨x, x*⟩ ≤ 1 for every x ∈ C}ispolarSet (pairing n), unfolded asmem_polarSet_rn. The two agree on cones (polarCone_eq_polarSet_rn, the remark following Corollary 14.5.1). - Rank of a convex set is
rankSet C = dim C - lineality C, defined here because Corollary 14.6.1 is its first consumer among sets; §13'srankFnis the companion for functions. - The triples of
ℝⁿ⁺²that Theorem 14.4 is stated in aretriple λ x μ, the concatenation(λ, x, μ), andendsReflectionis the book's(λ*, x*, μ*) ↦ (-μ*, x*, -λ*)read through it.
Theorems 14.1 and 14.5 carry no Proof. paragraph in the book, each summarising the running text
before it; both arguments are recovered here. polarCone_polarCone is proved by the separation
route the book mentions as an alternative (Corollary 11.7.1), and C°° = C by the same argument
with the constant normalised to 1.
The unnumbered running text is recorded too: (cl K)° = K° and K°° = cl K for an arbitrary
bundled cone; the polar of a subspace as its orthogonal complement, of the non-negative orthant as
the non-positive orthant, and of a generated cone as the solution set of ⟨aᵢ, x*⟩ ≤ 0; that
polarity is order-inverting; and that C° = D° for D = cl (conv (C ∪ {0})), whence
C°° = cl (conv (C ∪ {0})) — which is what makes Theorem 14.5's hypotheses exactly the right ones.
References #
- R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §14.
The two polars of §14 #
Rockafellar's polar of a convex cone (§14, p. 121):
K° = {x* | ⟨x, x*⟩ ≤ 0 for every x ∈ K}. This is the backbone's polarCone (pairing n), and the
equation is the definition unfolded.
Rockafellar's polar of a convex set (§14, p. 125):
C° = {x* | ⟨x, x*⟩ ≤ 1 for every x ∈ C}.
Polarity is order-inverting (§14): C₁ ⊆ C₂ implies C₂° ⊆ C₁°.
Order-inversion for cones. Specialises polarCone_anti.
The polar of a convex cone as a cone and as a set coincide (§14): the half-space
{x | ⟨x, x*⟩ ≤ 1} contains K if and only if {x | ⟨x, x*⟩ ≤ 0} does. The hypothesis is
Rockafellar's "cone", closure under positive scalar multiplication.
The bipolar of a set, with the .flip the backbone statement carries rewritten away;
flip_pairing says that ⟨·, ·⟩ on ℝⁿ is its own flip.
Theorem 14.1 #
The polarity correspondence for convex cones. The book prints no proof; see the module docstring.
Theorem 14.1, first assertion: the polar of a convex cone is non-empty — it always
contains the origin. No hypothesis on K is needed.
Theorem 14.1, first assertion: the polar of a convex cone is convex. No hypothesis on
K is needed.
Theorem 14.1, first assertion: the polar of a convex cone is a cone in Rockafellar's
sense, a K° = K° for every a > 0. No hypothesis on K is needed.
Theorem 14.1, first assertion: the polar of a convex cone is closed, being an
intersection of homogeneous closed half-spaces — which is Rockafellar's own remark that the first
assertion could also be derived from Corollary 11.7.1. No hypothesis on K is needed.
Theorem 14.1, second assertion: K°° = K for a non-empty closed convex cone.
A non-empty closed cone in Rockafellar's sense contains the origin, so it is a PointedCone, and
the bundled polarCone_polarCone_pointedCone supplies convexity, positive homogeneity and
non-emptiness at once.
Theorem 14.1, third assertion: the indicator functions of K and K° are
conjugate to each other. This direction is the computation §14 opens with, and needs no closedness.
Specialises conj_indicatorFn_eq_indicatorFn_polarCone, with the hypothesis triple supplied by the
bundling.
Theorem 14.1, third assertion, in the remaining direction: δ(· | K°)* is
δ(· | K) for a non-empty closed convex cone.
(cl K)° = K° (§14), the invariance that lets Theorem 14.1 be stated for closed
cones without loss. Specialises polarCone_closure.
K°° = cl K (§14) for a convex cone that need not be closed.
The examples of §14 (pp. 122–123) #
The polar of a subspace is the orthogonally complementary subspace (§14). For the Euclidean
pairing the annihilator of L is Mathlib's Submodule.orthogonal.
The polar of the non-negative orthant is the non-positive orthant (§14).
nonnegOrthant is §12's.
The polar of the convex cone generated by a family {aᵢ} is the solution set of the
homogeneous inequalities ⟨aᵢ, x*⟩ ≤ 0 (§14).
Dually (§14): the polar of {y | ⟨aᵢ, y⟩ ≤ 0 for every i} is the closure of the
convex cone generated by the aᵢ.
Theorem 14.2 #
Theorem 14.2, first assertion. Let f be a proper convex function. The polar
of the convex cone generated by dom f is the recession cone of f*.
The backbone's second properness hypothesis is discharged by Theorem 12.2 (theorem_12_2_proper),
which is available on ℝⁿ.
Theorem 14.2, second assertion. If f is closed, the polar of the recession
cone of f is the closure of the convex cone generated by dom f*.
Corollary 14.2.1. The polar of the barrier cone of a non-empty closed convex
set C is the recession cone of C.
barrierCone is §13's.
Corollary 14.2.2. Let f be a closed proper convex function. In order that
{x | f x ≤ α} be bounded for every α ∈ ℝ, it is necessary and sufficient that
0 ∈ int (dom f*).
Theorem 14.3 #
Rockafellar's hypothesis f(0) > 0 > inf f is self-dual: f*(0) = -inf f and inf f* = -f(0)
(conj_apply_zero, iInf_conj_eq_neg_apply_zero), so f*(0) > 0 > inf f* as well.
Theorem 14.3. Let f be a closed proper convex function with
f(0) > 0 > inf f. The closed convex cones generated by {x | f x ≤ 0} and by
{x* | f*(x*) ≤ 0} are polar to each other; this is one of the two directions.
Theorem 14.3, in the remaining direction: the polar of the closed convex cone
generated by {x* | f*(x*) ≤ 0} is the closed convex cone generated by {x | f x ≤ 0}.
Theorem 14.3 rewrites the inner cone as a polar, and the bipolar theorem
(polarCone_polarCone_rn) closes it.
Theorem 14.4 #
K is the convex cone in ℝⁿ⁺² generated by the (1, x, μ) with μ ≥ f(x), and K* the same
cone built from f*. The theorem reads the conjugate of f off the polar of K — conjugacy from
polarity, the direction opposite to the rest of §14. The mathematics lives in ℝ × ℝⁿ × ℝ, where
the cone is homCone f; triple concatenates that space into ℝⁿ⁺².
The vector (λ, x, μ) ∈ ℝⁿ⁺²: a scalar, a vector of ℝⁿ and a scalar, concatenated.
Equations
- Rockafellar.triple l x m = (Tdaf.ConvexAnalysis.euclideanTripleEquiv n) ((l, x), m)
Instances For
Rockafellar's mapping (λ*, x*, μ*) ↦ (-μ*, x*, -λ*) of ℝⁿ⁺² (§14, the display in the
proof of Theorem 14.4).
Equations
Instances For
The inner product of ℝⁿ⁺² read through the concatenation is the pairing the backbone's cone
theory is stated against.
The generating vectors (1, x, μ) with μ ≥ g(x), read through the concatenation: they are
the epigraph of the level-one lift of g.
The book's reflection and the backbone's are the same map, read through the concatenation.
Theorem 14.4. Let f be a closed proper convex function on ℝⁿ, let K be
the convex cone generated by the vectors (1, x, μ) ∈ ℝⁿ⁺² with μ ≥ f(x), and let K* be the
convex cone generated by the (1, x*, μ*) with μ* ≥ f*(x*). Then
cl K* = {(λ*, x*, μ*) | (-μ*, x*, -λ*) ∈ K°}.
Closedness of f is used in one place only, to give dom f* ≠ ∅.
Theorem 14.5 #
The polarity correspondence for closed convex sets containing the origin. The book prints no proof; see the module docstring.
Theorem 14.5, first assertion: C° is closed.
Specialises isClosed_polarSet; no hypothesis on C is needed.
Theorem 14.5, first assertion: C° is convex.
Specialises convex_polarSet; no hypothesis on C is needed.
Theorem 14.5, first assertion: C° contains the origin.
Specialises zero_mem_polarSet; no hypothesis on C is needed.
Theorem 14.5, first assertion: C°° = C for a closed convex set containing
the origin. Specialises polarSet_polarSet.
Theorem 14.5, second assertion: the gauge function of C is the support
function of C°.
Obtained from gaugeFn_polarSet at C° together with C°° = C; the backbone records that only
0 ∈ C° — which is automatic — is needed for that step.
Theorem 14.5, third assertion: dually, the gauge function of C° is the support function of
C. It needs only 0 ∈ C.
C° = D° where D = cl(conv(C ∪ {0})) (§14): a half-space {x | ⟨x, x*⟩ ≤ 1}
contains C if and only if it contains D, because such a half-space is closed and convex and
contains the origin.
C°° = cl(conv(C ∪ {0})) (§14), the identity that makes Theorem 14.5's
hypotheses exactly the right ones: the bipolar of an arbitrary set is the smallest closed convex
set containing it and the origin.
Corollary 14.5.1. Let C be a closed convex set containing the origin. Then
C° is bounded if and only if 0 ∈ int C.
Corollary 14.5.1, dual form: C is bounded if and only if 0 ∈ int C°. This is Corollary
14.5.1 applied to C° together with C°° = C.
Theorem 14.6 #
Theorem 14.6, first assertion: the polar of the recession cone of C is the
closure of the convex cone generated by C°.
Theorem 14.6, first assertion, in the other direction: the polar of the closed
convex cone generated by C° is the recession cone of C. With theorem_14_6_recession this is
the book's "polar to each other".
Theorem 14.6, second assertion: the lineality space of C and the subspace
generated by C° are orthogonally complementary — here in the form "the lineality space of C is
the annihilator of C°".
Theorem 14.6, second assertion, dual form: the polar of the lineality space of
C is the closed subspace generated by C°.
Corollary 14.6.1 #
Rockafellar's rank of a convex set (§8, p. 70): rank C = dim C - lineality C. §13's
rankFn is the companion for convex functions.
Equations
Instances For
Corollary 14.6.1, first relation: dim C° = n - lineality C for a closed
convex set C containing the origin.
dim is §1's, and the affine hull of C° is a subspace because 0 ∈ C°.
Corollary 14.6.1, second relation: lineality C° = n - dim C.
Corollary 14.6.1, third relation: rank C° = rank C. It is the difference of the other two,
both of which read n.
Theorem 14.7 #
Theorem 14.7, first assertion: if f is non-negative and vanishes at the origin, then
f* is likewise non-negative.
Theorem 14.7, first assertion: f* vanishes at the origin.
Theorem 14.7, first inclusion: {x | f x ≤ α}° ⊆ α⁻¹ {x* | f* x* ≤ α} for
0 < α < ∞.
Stated without the closedness the book assumes: one inclusion is a rescaling into the level set, the other is Fenchel's inequality, and neither uses it.
Theorem 14.7, second inclusion:
α⁻¹ {x* | f* x* ≤ α} ⊆ 2 {x | f x ≤ α}°.