Rockafellar, §16: Dual Operations #
The dual-operations dictionary: every operation of §5 has a dual operation, and conjugacy exchanges the two. All 15 numbered results of §16 are formalized.
The uniform shape of the section #
Each of the four theorems is really three statements, and this module keeps them apart:
- the identity, valid for arbitrary functions with no hypothesis and no closure
(
theorem_16_1_left,theorem_16_3_image,theorem_16_4_infConv,theorem_16_5_convFn); - the closure form,
(op of closures)* = cl (dual op of conjugates), which is the honest general statement (theorem_16_3_closure,theorem_16_4_closure,theorem_16_5_closure); - the exact form, in which a relative-interior qualification removes the closure and makes the
infimum attained (
theorem_16_3_exact,theorem_16_3_attained,theorem_16_4_exact,theorem_16_4_attained), together with the polyhedral form of the same qualification, which Rockafellar states here as a remark and proves only in §19 (theorem_16_3_polyhedral).
Notation #
A* is LinearMap.adjoint A throughout: isAdjointPair_adjoint says that Mathlib's adjoint is
Rockafellar's, so no statement here carries an IsAdjointPair hypothesis even though every
backbone statement it specialises does. λf is fun x => (l : EReal) * f x and fλ is
smulRight f l, both from §5.
References #
- R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §16.
The conjugate of the zero function #
Rockafellar's proof of Theorem 16.1 at λ = 0 is the single sentence "the constant function 0
is conjugate to the indicator function δ(· | 0)". Both halves of that sentence are used below.
Rockafellar, §16, p. 141: the conjugate of the constant function 0 is δ(· | 0).
Rn n is a SeparatingDual, asserted in the shared header.
The conjugate of δ(· | 0) is the constant function 0, the other half of the same sentence.
Specialises conj_indicatorFn_zero.
The half-space {x | ⟨x, x*⟩ ≤ 1} cutting out a polar set is convex, which is why polarity
does not see a convex hull.
Theorem 16.1: scalar multiplication #
Theorem 16.1. For any proper convex function f one has (λf)* = f*λ,
0 ≤ λ < ∞. This is the case λ > 0, where no hypothesis on f is needed at all.
Theorem 16.1, the other formula: (fλ)* = λf*, 0 < λ < ∞.
Theorem 16.1 at λ = 0: (0f)* = f*0. Left multiplication by 0 sends any
f to the constant function 0, right multiplication by 0 sends f* to δ(· | 0), and the two
are conjugate. This is the clause the book's proof singles out.
Theorem 16.1 at λ = 0, the other formula: (f0)* = 0f*.
Corollary 16.1.1. For any non-empty convex set C,
δ*(x* | λC) = λ δ*(x* | C) for 0 ≤ λ < ∞.
Convexity is not used: the identity is the indicator instance of Theorem 16.1 and holds for any
non-empty C. Specialises supportFn_smul, with the λ = 0 case read off 0 • C = {0}.
Corollary 16.1.2. For any non-empty convex set C, (λC)° = λ⁻¹C° for
0 < λ < ∞.
The book derives it from Corollary 16.1.1 through C° = {x* | δ*(x* | C) ≤ 1}; here it is one
unfolding of polarSet, since ⟨λx, x*⟩ = ⟨x, λx*⟩.
Lemma 16.2: the constraint qualifications of §9, dualized #
Lemma 16.2. Let L be a subspace of ℝⁿ and let f be a proper convex
function. Then L meets ri (dom f) if and only if there exists no vector x* ∈ Lᗮ such that
(f* 0⁺)(x*) ≤ 0 and (f* 0⁺)(-x*) > 0.
Lᗮ is the annihilator of L for the pairing, definitionally.
Corollary 16.2.1. Let A be a linear transformation from ℝⁿ to ℝᵐ and let g be a
proper convex function on ℝᵐ. In order that there exist no vector y* ∈ ℝᵐ with A*y* = 0,
(g* 0⁺)(y*) ≤ 0 and (g* 0⁺)(-y*) > 0, it is necessary and sufficient that Ax ∈ ri (dom g) for
at least one x ∈ ℝⁿ. Lemma 16.2 for the subspace L = range A, whose orthogonal complement is
ker A*.
Corollary 16.2.2. Let f₁, …, fₘ be proper convex functions on ℝⁿ. In
order that there exist no vectors x₁*, …, xₘ* with
x₁* + ⋯ + xₘ* = 0,
(f₁* 0⁺)(x₁*) + ⋯ + (fₘ* 0⁺)(xₘ*) ≤ 0,
(f₁* 0⁺)(-x₁*) + ⋯ + (fₘ* 0⁺)(-xₘ*) > 0,
it is necessary and sufficient that ri (dom f₁) ∩ ⋯ ∩ ri (dom fₘ) ≠ ∅.
This is Lemma 16.2 inside ℝᵐⁿ for the diagonal subspace L = {x | x₁ = ⋯ = xₘ}, whose
orthogonal complement is {x* | x₁* + ⋯ + xₘ* = 0}.
Theorem 16.3: linear transformations #
Theorem 16.3, first formula: for a linear transformation A from ℝⁿ to
ℝᵐ and any convex function f on ℝⁿ, (Af)* = f*A*.
Unconditional: no convexity, no properness, no closure. Specialises conj_mapLin, whose only
input is the adjointness datum, supplied by isAdjointPair_adjoint.
Theorem 16.3, second formula: ((cl g)A)* = cl(A*g*) for any convex g
on ℝᵐ.
Specialises conj_compLin_eq_clFn_mapLin, applied to cl g (which is closed convex) and read
back through (cl g)* = g*.
Theorem 16.3, the exact half: if there is an x with Ax ∈ ri (dom g), the closure
operation can be omitted and (gA)* = A*g*. The book's hypotheses are g proper convex, not
closed.
Theorem 16.3, the attainment: under the same qualification, for each x* the infimum
inf {g*(y*) | A*y* = x*} is attained (or is +∞ vacuously). The backbone's guard < ⊤ is exactly
the book's "or is +∞ vacuously".
Rockafellar, §16, the unnumbered remark: when g is polyhedral, the
qualification Ax ∈ ri (dom g) of Theorem 16.3 weakens to Ax ∈ dom g, and the conclusion is
unchanged.
Rockafellar states this as a remark just after Corollary 16.3.1 and defers the proof to
Corollary 19.3.1: g* is polyhedral by Theorem 19.2, so A*g* is polyhedral and hence closed,
and the closure in the second formula has nothing left to close.
Rockafellar, §16, the same remark, attainment clause under the weakened
qualification: for a polyhedral g the infimum inf {g*(y*) | A*y* = x*} is still attained
wherever it is finite.
Corollary 16.3.1, first formula: δ*(y* | AC) = δ*(A*y* | C) for any convex set C in
ℝⁿ. The indicator instance of theorem_16_3_image, via mapLin_indicatorFn. Convexity is not
used.
Corollary 16.3.1, second formula: for any convex set D in ℝᵐ,
δ*(· | A⁻¹(cl D)) = cl(A* δ*(· | D)).
The indicator instance of theorem_16_3_closure, via clFn_indicatorFn and
compLin_indicatorFn.
Corollary 16.3.1, the exact half: if some Ax ∈ ri D, the closure operation
can be omitted and δ*(x* | A⁻¹D) = inf {δ*(y* | D) | A*y* = x*}, the infimum being attained.
Corollary 16.3.2, first formula: (AC)° = A*⁻¹(C°) for any convex set C in ℝⁿ. One
unfolding of polarSet through the adjointness ⟨Ax, y*⟩ = ⟨x, A*y*⟩.
Corollary 16.3.2, the unconditional half of the second formula:
A*(D°) ⊆ (A⁻¹D)°. Equality holds after a closure, and without one under Corollary 16.3.1's
qualification; see the module docstring for why the closed form is not here.
Theorem 16.4: addition and infimal convolution #
Theorem 16.4, first formula, in the book's own m-ary form:
(f₁ □ ⋯ □ fₘ)* = f₁* + ⋯ + fₘ*.
The □-product is the AddCommMonoid sum of InfConvFn. Properness is not needed, and must
not be assumed at the intermediate stages, since □ does not preserve it.
Theorem 16.4, first formula for m = 2: (f □ g)* = f* + g*.
Theorem 16.4, second formula: (cl f + cl g)* = cl(f* □ g*). Specialises
conj_add_eq_clFn_infConv, applied to the closures.
Theorem 16.4, the exact half: if ri (dom f) and ri (dom g) have a point in common, the
closure operation can be omitted and (f + g)* = f* □ g*. Closedness is not assumed, as in the
book.
Theorem 16.4, the attainment: under the same qualification, for each x* the
infimum inf {f*(x₁*) + g*(x₂*) | x₁* + x₂* = x*} is attained.
Corollary 16.4.1, first formula for m = 2:
δ*(· | C₁ + C₂) = δ*(· | C₁) + δ*(· | C₂).
Unlike the function statement this needs no qualification: two suprema over sets never interact
through an ∞ - ∞.
Corollary 16.4.1, first formula in the book's m-ary form:
δ*(· | C₁ + ⋯ + Cₘ) = δ*(· | C₁) + ⋯ + δ*(· | Cₘ).
Corollary 16.4.1, second formula: δ*(· | cl C₁ ∩ cl C₂) = cl(δ*(· | C₁) □ δ*(· | C₂)). The
indicator instance of theorem_16_4_closure: adding indicators intersects the sets.
Corollary 16.4.1, the exact half: if ri C₁ and ri C₂ have a point in
common, δ*(x* | C₁ ∩ C₂) = inf {δ*(x₁* | C₁) + δ*(x₂* | C₂) | x₁* + x₂* = x*}, the infimum being
attained.
Corollary 16.4.2, first formula: (K₁ + K₂)° = K₁° ∩ K₂° for non-empty
convex cones.
The support function of a cone is the indicator of its polar, adding indicators intersects, and an indicator determines its set. Only the cone property is used, not convexity.
Theorem 16.4, the exact half in the book's own m-ary form: if the sets
ri (dom fᵢ), i = 1, …, m, have a point in common, the closure operation can be omitted from
the second formula and (f₁ + ⋯ + fₘ)* = f₁* □ ⋯ □ fₘ*.
The family is indexed by a Finset rather than by Fin m, so m = 0 is the vacuous empty
family and the book's m ≥ 1 is hs.
Theorem 16.4, the attainment for m summands: under the same qualification,
for each x* the infimum inf {f₁*(x₁*) + ⋯ + fₘ*(xₘ*) | x₁* + ⋯ + xₘ* = x*} is attained.
Corollary 16.4.1, the exact half in the book's m-ary form: if the sets
ri Cᵢ have a point in common, the closure operation can be omitted and
δ*(· | C₁ ∩ ⋯ ∩ Cₘ) = δ*(· | C₁) □ ⋯ □ δ*(· | Cₘ).
Non-emptiness of the Cᵢ is not a hypothesis here although it is in the book: a common point of
the relative interiors already supplies it.
Corollary 16.4.1, the attainment for m sets: under the same qualification,
for each x* the infimum inf {δ*(x₁* | C₁) + ⋯ + δ*(xₘ* | Cₘ) | x₁* + ⋯ + xₘ* = x*} is
attained.
Theorem 16.5: pointwise suprema and convex hulls #
Theorem 16.5, first formula: (conv {fᵢ | i ∈ I})* = sup {fᵢ* | i ∈ I} for an arbitrary
index set I. Unconditional; the empty family is not an exception. Specialises conj_convFn.
Theorem 16.5, second formula: (sup {cl fᵢ | i ∈ I})* = cl (conv {fᵢ* | i ∈ I}).
Specialises conj_iSup_eq_clFn_convFn, applied to the closures.
Corollary 16.5.1, first formula: the support function of the convex hull D
of the union of the sets Cᵢ is sup {δ*(· | Cᵢ) | i ∈ I}.
Corollary 16.5.1, second formula: the support function of the intersection of
the sets cl Cᵢ is cl (conv {δ*(· | Cᵢ) | i ∈ I}).
The indicator instance of theorem_16_5_closure. The index set must be non-empty: over an empty
family the book's ⋂ cl Cᵢ is all of ℝⁿ while sup {δ(· | Cᵢ)} is -∞.
Corollary 16.5.2, first formula:
(conv {Cᵢ | i ∈ I})° = ⋂ {Cᵢ° | i ∈ I}.
Polarity is order-inverting and {x | ⟨x, x*⟩ ≤ 1} is convex, so the convex hull is invisible to
it; this is the book's own second proof.
Corollary 16.5.2, the unconditional half of the second formula: each Cᵢ° is
contained in (⋂ Cⱼ)°, hence so is the convex hull of their union. Equality with the polar of
⋂ cl Cⱼ holds after a closure; see the module docstring.