The minimum of a convex function #
A point x minimises f exactly when 0 ∈ ∂f x, the subgradient inequality read at y = 0; that
is why subgradients are the engine here. Dually inf f = -f*(0) with no hypothesis at all, and for
closed proper convex f the minimum set is ∂f*(0), so every question about minimisers becomes
one about the conjugate near the origin. Existence comes from recession: a closed proper convex
function with no direction of recession has compact level sets and attains its infimum; that
relaxes to a constrained problem, with a further weakening when the constraint set is
polyhedral.
Main definitions #
argmin f— the minimum set{x | ∀ z, f x ≤ f z}.
Main results #
mem_argmin_iff_zero_mem_subgradient—xminimisesfexactly when0 ∈ ∂f x.conj_zero_eq_neg_iInf,argmin_eq_subgradient_conj_zero,iInf_ne_bot_and_argmin_eq_empty_iff,argmin_nonempty_and_isBounded_iff_zero_mem_interior_dom_conj,supportFn_setOf_le,argmin_eq_singleton_iff_hasGradientAt_conj_zero,supportFn_argmin,recessionCone_setOf_le_eq_polarCone_dom_conj,iInf_supportFn_setOf_le— the minimum set and the optimal value read off the conjugate at the origin (Theorem 27.1 in [^1], clauses (a)–(h)).isCompact_setOf_le— a level set of a closed proper convex function with no direction of recession is compact;argmin_nonempty_of_recessionConeFn_eq_zero,isCompact_argmin_of_recessionConeFn_eq_zero,exists_pos_forall_exists_mem_argmin_dist_lt— existence of a minimiser, and well-posedness (Theorem 27.2 in [^1]);tendsto_infDist_argminandtendsto_of_argmin_eq_singleton— the behaviour of minimising nets.exists_forall_le_of_recessionConeFn_inter_eq_zero,exists_forall_le_of_inter_subset_constancySpace_inter_linealitySpace,exists_forall_le_of_polyhedral_of_inter_subset_constancySpace— attainment over a closed convex set in its basic, general and polyhedral forms (Theorem 27.3 in [^1]), withargmin_nonempty_of_polyhedralFnfor a polyhedral objective.le_of_mem_subgradient_of_neg_mem_normalCone,exists_mem_subgradient_neg_mem_normalCone— the optimality condition for minimising over a convex set, sufficiency and necessity.argmin_sepSum,dom_sepSum— a separable objectivex ↦ ∑ᵢ hᵢ(xᵢ)on a dependent finite product is minimised coordinatewise: the decomposition principle.
Implementation notes #
The minimum set is {x | ∀ z, f x ≤ f z} rather than IsMinOn f Set.univ, because that unfolds to
the subgradient inequality at y = 0; mem_argmin_iff_isMinOn bridges to Mathlib. Necessity of
the optimality condition is stated against IsExactSum B h (indicatorFn C), which both of the
book's hypotheses instantiate. Minimising results are stated for an arbitrary filter where the book
uses sequences, except isBounded_range_of_tendsto_iInf, whose conclusion is about a range.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §27. Both level-set
formulas of clause (i) are in Duality/Level.lean.
The minimum set #
A point minimises exactly when its value is the infimum. The equational form of
mem_argmin_iff_le_iInf, which is what a statement identifying an optimal value with inf F 0
wants to rewrite with.
The maximum set of g: the points where g attains its supremum. The concave mirror of
argmin, and what "optimal solution" means for a concave program.
Instances For
A point maximises exactly when its value is the supremum. The mirror of
mem_argmin_iff_eq_iInf, and the step every statement of the form "v is an optimal solution to
the concave program (P*)" pays: argmax is a family of inequalities and the dual optimal value is
a supremum.
The minimum set transports along a surjection: x ↦ g (e x) is minimised exactly at the
e-preimages of the minimisers of g. Surjectivity makes the two quantifiers agree and is all the
proof uses; composed with argmin_sepSum it is the decomposition principle.
Separable sums on a finite product #
A separable objective x ↦ ∑ᵢ hᵢ(xᵢ) on a dependent finite product ∀ i, E i has its minimum
set and its effective domain given coordinatewise. This is the content of the decomposition
principle: once a Kuhn–Tucker vector has reduced a program to minimising h₁ + ⋯ + h_s
over C¹ × ⋯ × C^s, the problem splits into s independent problems. Both statements are about
the dependent product itself; no isometry with ℝⁿ, no relative interior and no linear structure
enter, since argmin and dom are order-theoretic.
The effective domain of a separable sum is the product of the effective domains. The only
hypothesis is that no summand takes ⊥, and it cannot be dropped: since ⊥ + ⊤ = ⊥, a sum can be
finite while a summand is +∞, which breaks ⊆. The ⊇ direction is unconditional.
A separable sum is minimised coordinatewise: the minimum set of x ↦ ∑ᵢ hᵢ(xᵢ) on a finite
product is the product of the minimum sets of the summands.
⊇ needs no hypothesis. ⊆ needs every summand proper, and both halves of properness carry
weight: a common domain point makes every hⱼ(xⱼ) finite, and finiteness is what allows the
j ≠ i part of the sum to be cancelled off both sides, EReal not being cancellative. Without the
domain point the statement is false — for ι = Fin 2 with h 0 ≡ ⊤ and h 1 = id on ℝ, the
left side is everything and the right side is empty.
The minimum set as a subdifferential of the conjugate #
The minimum set of a closed convex function is ∂f*(0); in particular the infimum is
attained exactly when f* is subdifferentiable at the origin. This is the subgradient inequality
for f* at the origin, where Fenchel–Moreau turns f** back into f.
Every nonempty level set of a closed proper convex function has the same recession cone, the
polar of dom f*.
The same for the minimum set: when the infimum is attained the minimum set is a level set, so
it too has the polar of dom f* as its recession cone.
Minimising over a convex set #
Sufficiency of the optimality condition: if some y ∈ ∂h x has -y normal to C at x,
then h attains its infimum over C at x. No hypothesis is needed — the subgradient inequality
and the normality inequality simply add.
The converse of mem_argmin_add_indicatorFn_of_forall: a minimiser of h + δ(· | C) that lies
in C minimises h over C.
Necessity: when the sum h + δ(· | C) is exact, every point where h attains its infimum
over C carries a subgradient y ∈ ∂h x with -y normal to C. The book's two hypotheses are
two ways of supplying that exactness.
Existence of a minimiser #
The level set that carries the existence argument: nonempty, closed, convex, and — when f
has no direction of recession — compact. Only the ⇒ direction is packaged here.
A closed proper convex function with no direction of recession attains its infimum. Any level
set of f is nonempty, closed, convex and compact, so lower semicontinuity attains a minimum on
it, and off that level set f is larger.
The minimum set is then a nonempty compact convex set.
With no direction of recession, the infimum of a closed proper convex function is real.
The minimum is then well posed: for every ε > 0 there is a δ > 0 with the level set
{x | f x ≤ inf f + δ} lying within ε of the minimum set. One application of the extreme value
theorem to the compact {f ≤ inf f + 1} \ (M + ε·int B) gives δ directly, in place of the
book's nested-compactness argument.
Minimising nets approach the minimum set: along any such net the distance to it tends to
0. Stated for an arbitrary filter — atTop on ℕ is the sequential case.
Every cluster point of a minimising net belongs to the minimum set.
A minimising sequence is bounded.
If a closed proper convex function attains its infimum at a unique point, every minimising net
converges to that point. No recession hypothesis is needed: a one-point minimum set is a level set,
and a bounded level set forces the recession cone to be {0}.
Minimising over a closed convex set #
The indicator of a nonempty closed convex set is a closed proper convex function.
The directions of recession of h + δ(· | C) are exactly the directions of recession common to
h and to C. This is the recession formula for a sum read against an indicator: δ(· | C)0⁺ is
δ(· | 0⁺C), which is 0 on 0⁺C and ⊤ off it.
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 directions
of recession of h + δ(· | C) are the common ones, so unconstrained existence applies; when
dom h ∩ C = ∅ the function is +∞ throughout C and every point minimises.
The same for an inequality system: a closed proper convex h attains its infimum subject to a
consistent system of constraints g i x ≤ 0 when h and the g i have no direction of recession
in common. The index type is arbitrary.
The polyhedral refinement #
For polyhedral C the recession hypothesis weakens from "h and C have no direction of
recession in common" to "every common direction of recession is one in which h is constant".
Where the book derives this from Helly's theorem, the proof here projects E along the constancy
space of h, which leaves h untouched and shrinks the common recession cone to {0}.
Polyhedrality of C enters exactly once: a linear map commutes with 0⁺ on a polyhedral set and
on no other kind.
Two points differing by a direction of constancy carry the same value. This is
mem_constancySpace_iff_forall_eq read as a statement about a pair of points rather than about
a direction.
Every subspace is the kernel of a linear projection. For a subspace M there is a linear
A : E →ₗ[ℝ] E and a complement N such that A moves points only by directions of M,
annihilates M, lands in N and fixes N pointwise. This is how "quotient out a subspace"
arguments run without leaving E, keeping a function constant along M unchanged.
The general form: a closed proper convex h attains its infimum over a nonempty closed
convex C as soon as every direction of recession common to h and C is both one in which h
is constant and a direction of linearity of C. The common recession cone may now be any such
subspace, not only {0}. The proof projects along
constancySubmodule h ⊓ linealitySubmodule C, where the image of C is C ∩ N.
The polyhedral refinement: a closed proper convex h attains its infimum over a nonempty
polyhedral convex C as soon as every direction of recession common to h and C is one in
which h is constant.
Polyhedrality of C pays for the weakened hypothesis and cannot be dropped: on ℝ² with
h(x₁, x₂) = x₂ and the closed convex C = {x | x₁ ≥ x₂²}, the common recession cone is
{(a, 0) | a ≥ 0}, along which h is constant, yet inf_C h = -∞. The proof replaces C by its
image under a projection killing the constancy space of h; the image is polyhedral, h is
unchanged along the fibres, and the common recession cone collapses to {0}.
A closed proper convex h all of whose directions of recession are directions in which h is
affine attains its infimum relative to any nonempty polyhedral convex C on which it is bounded
below.
The hypothesis recessionConeFn h ⊆ linealitySpaceFn h is weaker than the constancy hypothesis
above, and the price is the lower bound on C: a direction of recession in which h is affine has
slope ν = (h0⁺) y ≤ 0, and a lower bound along the half-lines of C in that direction forces
ν = 0, which is constancy. The lower bound cannot be dropped — h(x₁, x₂) = x₁ on ℝ² is affine
in every direction and its infimum over C = {x | x₂ = 0} is -∞. The hypothesis holds for every
affine or convex quadratic h, and whenever dom h* is affine.
The unconstrained case of the polyhedral refinement: a closed proper convex function whose
recession cone consists entirely of directions of constancy — equivalently, is a subspace —
attains its infimum. Existence with no direction of recession is the case of the subspace {0}.
Polyhedral minimisation #
A polyhedral convex function bounded below attains its infimum. In the finitely generated
description epi f = conv P + cone D a lower bound forces every generating direction to point
upward, so the vertical coordinate is minimised at one of the finitely many generating points.
Neither closedness nor properness is assumed.
A polyhedral convex function attains its infimum relative to any non-empty polyhedral convex
set on which it is bounded below. Restricting f to C cuts the epigraph down by the vertical
prism over C, so the restriction is again polyhedral. The book derives this from the
affine-recession form above, and hence from Helly's theorem; this argument needs neither.
The conjugate at the origin #
Three readings of f* near the origin: the interior of dom f* governs boundedness of the
minimum set, and the support functions of the level sets are read off f* by homogenisation and
by a limit of directional derivatives.
The origin is interior to dom f* exactly when f has no direction of recession: the
recession cone is the polar of dom f*, which is trivial exactly then.
The origin is in the relative interior of dom f* exactly when every direction of recession
of f is one in which f is constant. The relative-interior criterion for dom f*, read at the
origin, collapses to 0⁺f ⊆ constancy space.
The minimum set of a closed proper convex function is non-empty and bounded exactly when the
origin is interior to dom f*. Both directions pass through "no direction of recession": a bounded
level set has trivial recession cone one way, and existence of a minimiser the other.
The same in level-set form: some level set of f is non-empty and bounded exactly when the
origin is interior to dom f*. Here "some" is as good as "every", since all non-empty level sets
share the recession cone of f.
For the objective function of a convex program: the minimum set is non-empty and bounded
exactly when some level set is. Both say 0 ∈ int (dom f*).
Raising the conjugate by a real constant lowers the biconjugate by the same constant. This is
conj_add_const read on the dual pair.
For each real α the support function of the level set {f ≤ α} is the closure of the
positively homogeneous convex function generated by f* + α.
When f is bounded below, the support function of its minimum set is the closure of the
directional derivative of f* at the origin.
The level sets of f above its infimum are exactly the ε-subdifferentials of f* at the
origin. Fenchel–Moreau plus f*(0) = -inf f: z ∈ ∂_ε f*(0) says ⟨z, y⟩ - f*(y) ≤ inf f + ε for
every y, whose supremum on the left is f**(z) = f(z).
As the level shrinks to the infimum, the support functions of the level sets of f converge to
the directional derivative of f* at the origin. The ε-subdifferentials of f* at the origin are
exactly those level sets; the limit is an infimum because ε ↦ ∂_ε f*(0) is monotone.
The infimum of a closed proper convex function is finite but unattained exactly when f*(0)
is finite and f*'(0; ·) takes −∞ somewhere. Only one bound appears on each side, because
f*(0) ≠ ⊥ and ⨅ f ≠ ⊤ hold for every proper f.
A unique minimiser is a gradient of the conjugate #
The minimum set is ∂f*(0), and a subdifferential is a singleton exactly at a point of
differentiability; what follows is the two composed. No reflexivity is needed: the subdifferential
in question is subgradient B.flip (conj B f) 0, a subset of E.
Necessity: if the minimum set of f is the single vector x, then f* is differentiable
at the origin with ∇f*(0) = ⟨·, x⟩. The finite-dimensionality is F's, not E's — it is the
space f* lives on.
Sufficiency: if f* is differentiable at the origin with ∇f*(0) = ⟨·, x⟩, then x is
the unique minimiser of f.
Properness of f is not needed: differentiability of f* at the origin already forces f* proper,
hence f*(0) finite, which is all the uniqueness argument consumes. The separation that argument
needs is free from IsCompatiblePairing B, and it is not an artefact — if B x = 0 for some
x ≠ 0 then every level set of f = f** is invariant under translation by x and no minimum set
is ever a singleton. Finite-dimensionality of F is not used on this side.
The minimum set of a closed proper convex f is the single vector x exactly when f* is
differentiable at the origin with ∇f*(0) = ⟨·, x⟩.
The existential form: the infimum of f is attained at a unique point exactly when f* is
differentiable at the origin. Passing from the functional ∇f*(0) to the vector x : E
representing it is the surjectivity half of IsCompatiblePairing B.flip.