Rockafellar, §27: The Minimum of a Convex Function #
The unconstrained minimum of a convex function and its duality with f* at the origin
(Theorem 27.1); existence, compactness and well-posedness of the minimum set under a recession
hypothesis (Theorems 27.2 and 27.3); and the optimality condition 0 ∈ ∂h(x) + N_C(x) for
minimising over a convex set (Theorem 27.4).
All 9 numbered results of §27 are formalized: Theorems 27.1–27.4 — 27.1 with its nine clauses (a)–(i) — and Corollaries 27.2.1, 27.2.2, 27.3.1, 27.3.2 and 27.3.3.
The book's minimum set of f is the backbone's argmin f = {x | ∀ z, f x ≤ f z}, whose unfolded
form is the subgradient inequality at x* = 0; mem_argmin_iff_isMinOn is the bridge to Mathlib's
IsMinOn. The level set lev_α f is written out as {x | f x ≤ (α : EReal)} and inf f is
⨅ x, f x in EReal, so "bounded below", "finite" and "attained" read as ≠ ⊥, ≠ ⊥ ∧ ≠ ⊤ and
(argmin f).Nonempty. The one definition introduced here is IsDirectionOfRecession.
Corollaries 27.2.1 and 27.2.2 are about minimising sequences and are stated that way;
corollary_27_2_1_infDist records the backbone's arbitrary-filter form of the same fact.
References #
- R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §27 (pp. 263–272). Corollary 27.2.1 is stated there with no printed proof, and the polyhedral clause of Theorem 27.3 is proved there from Helly's theorem.
The section's vocabulary #
Rockafellar's direction of recession of f: a nonzero y such that λ ↦ f (x + λ y) is
non-increasing for every x.
Equations
- Rockafellar.IsDirectionOfRecession f y = (y ≠ 0 ∧ ∀ (x : TdafSurface.Rn n), Antitone fun (l : ℝ) => f (x + l • y))
Instances For
A direction of recession is a nonzero element of recessionConeFn f. This is Theorem 8.6
(forall_antitone_iff_recessionFn_nonpos), which needs no hypothesis on f at all.
"f has no direction of recession" is 0⁺f = {0}: the hypothesis of Theorem 27.2 and of the
non-polyhedral case of Theorem 27.3, as the backbone spells it.
"f and C have no direction of recession in common", the hypothesis of Theorem 27.3, against
the backbone's 0⁺f ∩ 0⁺C = {0}.
The section's opening remarks #
The minimum set of a convex f is convex: when nonempty it is a level set of f, which is the
book's reason.
The minimum set is closed when f is closed.
The minimum set contains at most one point when f is strictly convex on dom f: two distinct
minimisers lie in dom f — a minimiser of a proper f has a finite value — and their midpoint
would have a strictly smaller value.
x minimises f exactly when 0 ∈ ∂f(x): argmin f unfolds to the subgradient inequality at
x* = 0.
By Theorem 23.2: 0 ∈ ∂f(x) exactly when f is finite at x and f'(x; y) ≥ 0 for every
y.
One of the most quoted sentences in the subject: a local minimum of a proper convex function
is a global minimum. Rockafellar routes it through Theorem 23.2 — the directional derivatives see
only an arbitrarily small neighbourhood — while the proof here is the underlying convexity estimate
along [x, z].
Theorem 27.1(a): the infimum is -f*(0) #
Theorem 27.1(a). inf f = -f*(0). Needs no hypothesis at all, not even convexity: the
theorem's standing "closed proper convex" is there for the other eight clauses.
Theorem 27.1(a), second sentence: f is bounded below iff 0 ∈ dom f*. Also
hypothesis-free.
Theorem 27.1(b): the minimum set is ∂f*(0) #
Theorem 27.1(b), first sentence: the minimum set of a closed convex f is ∂f*(0), by
Theorem 23.5 at the origin. Properness, which the book assumes throughout, is not needed.
Theorem 27.1(b), second sentence: the infimum of f is attained exactly when f* is
subdifferentiable at the origin.
Theorem 27.1(b), third sentence: 0 ∈ ri (dom f*) is enough for the infimum to be attained.
This is Theorem 23.4 for f* at the origin.
Theorem 27.1(b), last sentence: 0 ∈ ri (dom f*) exactly when every direction of recession
of f is a direction in which f is constant. Corollary 8.6.1 is what makes constancySpace f the
book's phrase.
Theorem 27.1(c): finite but unattained #
Theorem 27.1(c). The infimum of a closed proper convex f is finite but unattained exactly
when f*(0) is finite and f*'(0; y) = -∞ for some y. Only one of the book's two finiteness
bounds carries information on each side; the two that are free are theorem_27_1_c_free.
The two bounds theorem_27_1_c leaves out, so that the reading "finite" can be checked against
the statement: for a proper f, inf f ≠ ⊤ and f*(0) ≠ ⊥ hold unconditionally.
Theorem 27.1(d): a nonempty bounded minimum set #
Theorem 27.1(d), first sentence: the minimum set of a closed proper convex f is nonempty
and bounded exactly when 0 ∈ int (dom f*).
Theorem 27.1(d), second sentence: that holds exactly when f has no direction of
recession.
Theorem 27.1(d) in the form Theorem 30.4(g) uses it: some level set of f is nonempty and
bounded exactly when the minimum set is.
Theorem 27.1(e): a unique minimiser is ∇f*(0) #
Theorem 27.1(e). The minimum set of a closed proper convex f is {x} exactly when f* is
differentiable at the origin with ∇f*(0) = x. Nothing needs reflexivity: ∂f*(0) is a subset of
ℝⁿ, because the pairing is what says what a dual variable of f* is.
Theorem 27.1(e) as existence: the infimum is attained at a unique point iff f* is
differentiable at the origin.
Theorem 27.1(e), the identification x = ∇f*(0): the unique minimiser is computed by
gradientVec (§25).
Theorem 27.1(f): all nonempty level sets share a recession cone #
Theorem 27.1(f): every nonempty level set of a closed proper convex f has the recession
cone of f. This is Theorem 8.7, restated here because clause (f) is where §27 uses it.
Theorem 27.1(f), the parenthesis: the minimum set, when nonempty, is itself a level set, so
it too has the recession cone of f.
Theorem 27.1(f), last sentence: that common recession cone is the polar of the convex cone
generated by dom f* — equivalently, since polarity does not see the cone hull, of dom f*.
Theorem 27.1(g): support functions of the level sets #
Theorem 27.1(g), first sentence: for each real α the support function of lev_α f is the
closure of the positively homogeneous convex function generated by f* + α.
Theorem 27.1(g), second sentence: when f is bounded below, the support function of the
minimum set is the closure of f*'(0; ·). Clause (b) plus Theorem 23.2; "bounded below" enters as
f*(0) ≠ ⊤, which is clause (a).
Theorem 27.1(h): the limit of the support functions #
Theorem 27.1(h). If inf f is finite then lim_{α ↓ inf f} δ*(y | lev_α f) = f*'(0; y) for
every y. The limit is stated as an infimum: the level sets increase with α, so their support
functions do, and the monotone limit is the infimum; no filter is needed.
The identification the proof of Theorem 27.1(h) runs on, unnumbered in the book: the level sets
of f above its infimum are the ε-subdifferentials of f* at the origin.
Theorem 27.1(i): the origin in the closure of dom f* #
Theorem 27.1(i), first sentence: 0 ∈ cl (dom f*) exactly when (f0⁺)(y) ≥ 0 for every
y. This is the origin case of Corollary 13.3.4.
Theorem 27.1(i), second sentence: 0 ∉ cl (dom f*) exactly when f decreases at a uniform
positive rate along some nonzero direction. y ≠ 0 is automatic — at y = 0 the inequality at
λ = 1 would read 0 ≤ -ε on dom f — and restricting x to dom f costs nothing.
Clauses (a) and (i) together, an unnumbered remark of §27: f can recede nowhere at a negative
rate and still be unbounded below, exactly when 0 ∈ cl (dom f*) but 0 ∉ dom f*.
Theorem 27.2: existence, compactness and well-posedness #
Theorem 27.2, first sentence: a closed proper convex function with no direction of recession has a finite infimum. The backbone's proof is the lower-semicontinuous extreme value theorem on a level set, which Theorems 8.7 and 8.4 make compact.
Theorem 27.2, the attainment.
Theorem 27.2, last clause: the minimum set is nonempty, closed, bounded and convex. Closed
and bounded is stated as compact, which in ℝⁿ is the same thing.
Theorem 27.2, well-posedness: for every ε > 0 there is a δ > 0 such that every x with
f x ≤ inf f + δ lies within ε of the minimum set. Rockafellar's nested-compactness argument is
avoided: the extreme value theorem is applied once more, to lev_{inf f + 1} f \ (M + ε · int B).
Corollary 27.2.1 #
Corollary 27.2.1, first assertion: a minimising sequence of a closed proper convex function
with no direction of recession is bounded. The book states this corollary with no proof. The
argument is Theorem 27.2's well-posedness clause at ε = 1, past which the whole sequence lies
within distance 1 of the compact minimum set.
Corollary 27.2.1: every cluster point of a minimising sequence lies in the minimum set.
The substance of Corollary 27.2.1: along any minimising net the distance to the minimum set
tends to 0. Stated for an arbitrary filter, of which the book's atTop is one instance.
Corollary 27.2.2 #
Corollary 27.2.2 — the label is printed in mixed case in the book. If a closed proper convex
function attains its infimum at a unique x, every minimising sequence converges to x. No
recession hypothesis: a one-point minimum set is a level set, so Theorem 8.7 forces 0⁺f = {0}.
Theorem 27.3: minimising over a closed convex set #
Theorem 27.3, the non-polyhedral case: a closed proper convex h attains its infimum over a
nonempty closed convex C as soon as h and C have no direction of recession in common. The
degenerate case dom h ∩ C = ∅, where every point of C minimises, is dispatched separately.
Theorem 27.3, the polyhedral refinement: for polyhedral C it is enough that every common
direction of recession of h and C be one in which h is constant. The book proves this from
Helly's theorem (Theorem 21.5); the proof here projects ℝⁿ along the constancy space of h.
Theorem 27.3 in a form the book does not state but its proof gives: for a general closed
convex C the hypothesis weakens to "every common direction of recession is one in which h is
constant and C is linear". This sits strictly between the book's two clauses.
Corollary 27.3.1 #
Corollary 27.3.1. If every direction of recession of a closed proper convex h is one in
which h is affine, then h attains its infimum relative to any polyhedral convex C on which
it is bounded below. The lower bound cannot be dropped: h(ξ₁, ξ₂) = ξ₁ is affine in every
direction and its infimum over {ξ₂ = 0} is -∞.
The unconstrained case of the polyhedral refinement of Theorem 27.3, which the book does not separate out: a closed proper convex function whose recession cone consists of directions of constancy attains its infimum.
Corollary 27.3.2 #
Corollary 27.3.2. A polyhedral convex function attains its infimum relative to any polyhedral convex set on which it is bounded below. The book derives this from Corollary 27.3.1 and so from Helly's theorem; the proof here needs neither.
Corollary 27.3.2 unconstrained. Neither closedness nor properness is assumed: boundedness below
already excludes -∞, and h ≡ +∞ is minimised everywhere.
Corollary 27.3.3: an arbitrary system of convex inequalities #
Corollary 27.3.3, the non-polyhedral case: a closed proper convex f₀ attains its infimum
subject to a consistent system fᵢ x ≤ 0, i ∈ I, of closed proper convex constraints, provided
f₀ and the fᵢ have no direction of recession in common. The index set is arbitrary.
The polyhedral refinement #
The book splits the index set as I = I₀ ⊔ (I ∖ I₀) with I₀ finite; two index types say the
same thing and keep every DecidableEq out of the statement. ι₀ is the book's I₀.
Corollary 27.3.3, the polyhedral refinement: the infimum is attained if the constraints
split into a finite polyhedral family g₀ and an arbitrary family g₁, and the only common
directions of recession are ones in which f₀ and all the g₁ are constant. The book's own
reduction lands on the polyhedral case of Theorem 27.3, so Helly's theorem is not needed.
Theorem 27.4: the subdifferential optimality condition #
Theorem 27.4, sufficiency: if some x* ∈ ∂h(x) has -x* normal to C at x, then h
attains its infimum relative to C at x. Needs no hypothesis at all — not properness of h,
not convexity of C, not even x ∈ C: the two inequalities simply add.
Theorem 27.4, necessity under the book's first constraint qualification: ri (dom h) meets
ri C. The exactness of the sum h + δ(· | C) comes from Theorem 16.4; Rockafellar's proof cites
Theorem 23.8 for the same step.
Theorem 27.4, necessity under the book's second constraint qualification: C polyhedral and
ri (dom h) meets C — merely C, not ri C, since the polyhedral summand of the IsExactSum of
Theorem 20.1 needs only a point of its effective domain.
The headline application of Theorem 27.4, and the projection theorem: x is the point of a
nonempty convex C nearest to a exactly when a - x is normal to C at x. Closedness of C
is not needed for the characterisation, only for the existence of a nearest point.