Support functions of level sets #
Three results that need both the conjugate and the recession function: the support function of a
level set {x ∣ f x ≤ 0}, the lineality space of f*, and co-finiteness. The first is stated in
terms of the positively homogeneous convex function generated by f — the greatest positively
homogeneous convex minorant of f, obtained from the convex cone generated by epi f. That
operator lives on the same space as f, and is not Homogenize.lean's hom, which is this
operator applied to the level-one lift, so it is developed here.
Main definitions #
posHomGenCone f— the convex cone{0} ∪ ⋃_{a > 0} a • epi fgenerated by the epigraph; for convexfit isPointedCone.hull ℝ (epi f).posHomGen_eq_ofEpi— the bridge toposHomGen(Recession/ConeHull.lean), the positively homogeneous convex function generated byf: for convexf,ofEpiof that cone. The book's formulak x = inf {λ f (λ⁻¹ x) ∣ λ > 0}isposHomGen_apply_of_ne_zero, and the value at the origin is0or-∞according to the sign off 0.Cofinite f— closed proper convex functions whose recession function is+∞in every nonzero direction.
Main results #
setOf_clFn_posHomGen_le_zero—{x ∣ (cl k) x ≤ 0}is the closed convex cone generated by{x ∣ f x ≤ 0}, for closed proper convexfwithf 0 > 0 > inf f.conj_posHomGen—(posHomGen f)* = δ(· ∣ {y ∣ f* y ≤ 0}), with no hypothesis whatsoever.conj_apply_zero,iInf_conj_eq_neg_apply_zero—f*(0) = -inf funconditionally, andinf f* = -f(0)for closed convexf; together they say that the hypothesisf 0 > 0 > inf fis self-dual.supportFn_setOf_le_zero,clFn_posHomGen— the two halves of the level-set dualityδ*(· ∣ {x ∣ f x ≤ 0}) = cl (posHomGen f*)andcl (posHomGen g) = δ*(· ∣ {x ∣ g* x ≤ 0})(Theorem 13.5 in [^1]).clFn_homis the same forhom f, over the product pairing onℝ × E.mem_linealitySpaceFn_conj_iff,linealitySpaceFn_conj_eq_annihilator—yis a direction of affineness off*exactly when⟨·, y⟩is constant ondom f, so the lineality space off*is the annihilator of the subspace parallel toaff (dom f)(Theorem 13.4 in [^1]);interior_dom_conj_nonempty_iffreads that as "dom f*has interior points exactly whenfis affine along no line".recessionFn_eq_supportFn_dom_conj— the recession function of a closed proper convexfis the support function ofdom f*.closure_dom_conj_eq_univ_iff,cofinite_iff_dom_conj_eq_univ—fis co-finite exactly whendom f*is dense, and, in finite dimensions, whendom f*is everything (Corollary 13.3.1 in [^1]).mem_closure_dom_conj_iffand its three companions — where a pointy₀sits relative todom f*is decided by the sign off 0⁺ - ⟨·, y₀⟩.
Divergences from the reference #
The level-set duality needs no properness: the improper cases are carried by the general
identification of the closure of a positively homogeneous convex function as a support function,
which covers cl g ≡ -∞ as the support function of ∅. Several statements assume
SeparatingDual ℝ E — "δ*(y ∣ F) is +∞ for y ≠ 0" needs the pairing to separate the
points of E, and with the indiscrete topology every support function vanishes;
separatingRight_flip_of_separatingDual and injective_of_separatingDual are the two forms later
results consume. Co-finiteness assumes FiniteDimensional ℝ F in one direction: the book's
step from "dom f* is contained in no closed half-space" to "dom f* is everything" fails in
infinite dimensions, where the kernel of a discontinuous functional is a dense proper convex
subset. closure_dom_conj_eq_univ_iff survives.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §5 (the positively homogeneous convex function generated by a convex function), §13 and §14.
The positively homogeneous convex function generated by f #
The convex cone in E × ℝ generated by epi f: the origin together with every positive
multiple of the epigraph. Reading it as an epigraph gives the positively homogeneous convex function
generated by f (posHomGen_eq_ofEpi). Like homCone it is not an epigraph: it meets the fibre
over 0 in the single point 0.
Equations
- Tdaf.ConvexAnalysis.posHomGenCone f = {0} ∪ ⋃ (a : ℝ), ⋃ (_ : a > 0), a • Tdaf.ConvexAnalysis.epi f
Instances For
Minimality of the generated cone: it is contained in every cone through the origin that
contains epi f.
The cone generated by the epigraph of a convex function is its PointedCone hull, so
posHomGenCone describes the cone that defines posHomGen rather than being a second definition
of it. For non-convex f the two differ: the hull adds sums the union misses.
The cone generated by the epigraph of the level-one lift of a convex f is its PointedCone
hull, so homCone f is the convex cone generated by the vectors ((1, x), μ) with μ ≥ f x.
The positively homogeneous convex function generated by a convex f is ofEpi of
posHomGenCone f. posHomGen itself is defined from the PointedCone hull, which gives it its
unconditional convexity and maximality; this is the ray description the classical proofs use.
The ray description of the generated cone is enough for maximality: it is contained in
epi g for every positively homogeneous g with g 0 ≤ 0 and g ≤ f, without convexity of
g, which le_posHomGen needs because it works with the hull.
The formula for the generated function, away from the origin:
k x = inf {λ f (λ⁻¹ x) | λ > 0}. The origin must be excluded because the generated cone
contributes the point (0, 0) there.
hom f is posHomGen applied to the level-one lift, the two generated cones being the
same set. The hypothesis f ≢ +∞ is needed: for f ≡ +∞ the cone degenerates to {0}, whose
ofEpi is δ(· | 0), whereas hom f ≡ +∞.
The zero level set of the generated function #
Two sublevel sets of k = posHomGen f sandwich the convex cone generated by {x | f x ≤ 0}:
{k < 0} lies inside it and {k ≤ 0} contains it, because (fλ) x ≤ 0 for a positive λ says
exactly that λ⁻¹ x lies in {x | f x ≤ 0}. Both sublevel sets have the same closure, so the
closed convex cone generated by {x | f x ≤ 0} is the zero sublevel set of cl k.
The zero sublevel set of posHomGen f is a convex cone, so it contains the whole cone
generated by {x | f x ≤ 0}. The hypothesis ∀ x, posHomGen f x ≠ ⊥ is what reading positive
homogeneity plus convexity as subadditivity costs.
Where posHomGen f is negative, the point already lies on a ray through {x | f x ≤ 0}:
(fλ) x ≤ 0 for a positive λ exactly when λ⁻¹ x lies in {y | f y ≤ 0}. The hypothesis
f 0 ≥ 0 excludes the origin, forcing posHomGen f 0 = 0.
The closed convex cone generated by {x | f x ≤ 0} is the zero sublevel set of cl k,
where k = posHomGen f.
{k < 0} and {k ≤ 0} sandwich the cone generated by {x | f x ≤ 0}, and both have closure
{x | (cl k) x ≤ 0}. That step needs k proper convex with inf k < 0, which is where f 0 > 0
and inf f < 0 are used, and it is the only source of finite dimension here.
The conjugate of a generated positively homogeneous function #
This is the algebraic core of the level-set duality, needing no topology: posHomGen f is
positively homogeneous, so its conjugate is an indicator function
(conj_eq_indicatorFn_of_posHomogeneous), and the set it indicates is unchanged by the passage from
f to posHomGen f.
The conjugate of the positively homogeneous convex function generated by f is the
indicator of {y | f* y ≤ 0}.
No hypothesis at all — neither closedness, nor properness, nor convexity of f — because
posHomGen f is positively homogeneous and nonpositive at the origin whatever f is.
The infimum of the conjugate is minus the value at the origin: inf f* = -f(0), for a
closed convex f. With conj_apply_zero, this says that the hypothesis f 0 > 0 > inf f is
self-dual.
The support function of a zero level set #
Only the space the function lives on carries a topology: the closure of a positively homogeneous convex function is a support function, and the level set produced is a subset of the other space.
The closure of the positively homogeneous convex function generated by g is the support
function of {x | g*(x) ≤ 0}.
No hypothesis at all, not even convexity of g, and the improper case is already covered: there
both sides are the support function of ∅.
The same with the closure removed: if posHomGen g is closed, it is the support function
of {x | g*(x) ≤ 0}.
The support function of the level set {x | f x ≤ 0} of a closed convex function is the
closure of the positively homogeneous convex function generated by f*.
Closedness of f is what turns {x | f**(x) ≤ 0} back into {x | f(x) ≤ 0}. The book's
properness hypothesis is not needed: biconj_eq_self covers the improper cases too.
The homogenisation hom f #
The previous result applied to the level-one lift of f, paired against ℝ × F by
⟨(λ, x), (λ*, x*)⟩ = λ λ* + ⟨x, x*⟩. The ℝ factor is paired with itself by multiplication,
which is innerₗ ℝ; that is the only compatible pairing of ℝ with ℝ up to a positive
scalar, and it is the one the book's λ λ* means.
The conjugate of the level-one lift is nonpositive at (λ*, x*) exactly when f*(x*) ≤ -λ*.
This is the computation h*(λ*, x*) = λ* + f*(x*), stated as a sublevel-set condition rather than
as an equation so as to stay clear of EReal's ⊤ + ⊥.
The closure of the homogenisation hom f is the support function of
{(λ*, x*) | λ* ≤ -f*(x*)}.
The book states the conclusion for the explicit k (λ, x) = (fλ) x for λ > 0, (f 0⁺) x for
λ = 0, +∞ for λ < 0; identifying that k with cl (hom f) is a separate recession-function
statement.
The lineality space of the conjugate #
The lineality space of a function (linealitySpaceFn) is the set of directions in which its
recession function is additively reversible — Rockafellar's directions of affineness. It is
strictly larger than the constancy space (constancySpace), which asks the recession function to
vanish in both directions, and it is the lineality space that is computed here.
y is a direction of affineness of f* exactly when ⟨·, y⟩ is constant on dom f.
The same, as the set of y on which ⟨·, y⟩ takes one value across all of dom f.
The lineality space of f* is the annihilator of the subspace parallel to aff (dom f),
which is vectorSpan ℝ (dom f). In an inner-product space that annihilator is the orthogonal
complement, which is the book's phrasing.
The dual form: for a closed proper convex f, the lineality space of f itself is the
annihilator of the subspace parallel to aff (dom f*).
Co-finiteness #
Co-finite convex functions: closed proper convex functions whose epigraph contains no
non-vertical half-line, i.e. whose recession function is +∞ in every nonzero direction. They are
exactly the functions with an everywhere-finite conjugate (cofinite_iff_forall_conj_lt_top).
- recessionFn_eq_top (y : E) : y ≠ 0 → recessionFn f y = ⊤
The recession function is
+∞in every direction but0.
Instances For
For a closed proper convex f, the recession function of f is the support function of
dom f*.
The support function of the whole dual space is +∞ in every nonzero direction, provided the
pairing separates the points of E. The hypothesis is not decoration: with the indiscrete topology
on E the continuous dual is 0 and every support function vanishes identically.
The conjugate of the constant function 0 is δ(· | 0), conj_indicatorFn_zero being the
converse. It carries the separation hypothesis of supportFn_univ_of_ne_zero, 0 being the
indicator of the whole space.
Co-finiteness, in the form that survives infinite dimensions: dom f* is dense if and
only if f is co-finite.
The book's dom f* = ℝⁿ is genuinely stronger outside finite dimensions: the kernel of a
discontinuous linear functional is a dense proper convex subset on which no nonzero continuous
linear functional is bounded above. dom_conj_eq_univ_iff restores the book's form under
FiniteDimensional ℝ F.
A compatible pairing whose left space has a separating dual separates the points of that
space: if ⟨x, y⟩ = 0 for every y, then every continuous linear functional kills x. This is
what statements quantifying over the nonzero vectors of E need.
A compatible pairing is injective on the left when the left space has a separating dual.
This is separatingRight_flip_of_separatingDual packaged as injectivity of the bilinear map, the
form the uniqueness results take as an explicit Function.Injective B.flip hypothesis because they
are stated with no topology at all. Over a normed space SeparatingDual ℝ E is automatic, so
[IsCompatiblePairing B] alone suffices.
Where a point sits relative to dom f* #
In the closure, the relative interior, the interior or the affine hull of dom f* — each is decided
by the recession function of f, through the support-function description of each of those four
positions relative to a convex set, and recessionFn_eq_supportFn_dom_conj.
The book states the four clauses for the translated function g = f - ⟨·, y₀⟩, whose recession
function is g 0⁺ = f 0⁺ - ⟨·, y₀⟩; "(g 0⁺)(y) ≥ 0" and "⟨y, y₀⟩ ≤ (f 0⁺)(y)" are the same
inequality, and the translation is what the statements below avoid having to name.
y₀ lies in the closure of dom f* exactly when the recession function of f dominates the
linear function ⟨·, y₀⟩.
The same at the origin: the origin lies in the closure of dom f* exactly when f recedes
nowhere at a negative rate.
The recession bound f 0⁺ y ≤ -ε written out: f decreases at rate at least ε along y.
Restricting x to dom f is free — off dom f the right-hand side is ⊤ - ε = ⊤.
The origin lies outside the closure of dom f* exactly when f decreases at a uniform
positive rate along some direction.
y ≠ 0 is automatic: at y = 0 the inequality at a = 1 would read 0 ≤ -ε at any point of the
nonempty effective domain.
In finite dimensions a dense convex set is everything: ri (cl C) = ri C together with
ri univ = univ.
For a closed proper convex f, the conjugate f* is finite everywhere if and only if f is
co-finite.
The same, stated through Cofinite.
The same, in the "finite everywhere" phrasing.
y₀ lies in the relative interior of dom f* exactly when the recession function of f
dominates ⟨·, y₀⟩, strictly in every direction in which it is not additively reversible. The
exceptional directions, those with -(f 0⁺)(-y) = (f 0⁺)(y), are the ones along which dom f*
lies in a hyperplane.
y₀ lies in the interior of dom f* exactly when the recession function of f strictly
dominates ⟨·, y₀⟩ in every nonzero direction.
y₀ lies in the affine hull of dom f* exactly when ⟨·, y₀⟩ agrees with the recession
function of f in every direction in which the latter is additively reversible.
dom f* has nonempty interior exactly when the lineality space of f is trivial — when
there is no line along which f is finite and affine.