The convex cone generated by a convex set #
Three closure theorems of the same shape: generate a cone, or a positively homogeneous function,
from a convex object and ask when the result is closed. For closed convex C with 0 ∉ C, the
cone generated by C differs from its closure only by 0⁺C. For closed proper convex f with
f 0 > 0, the closure of the positively homogeneous convex function generated by f is the
attained infimum inf {fλ | λ > 0 or λ = 0⁺}. And conv (C ∪ D) is closed once directions of
recession of C and of D can cancel only inside the lineality spaces. All three come from the
closed-image and sum theorems, read off the cone {(λ, x) | λ > 0, x ∈ λC} one dimension up,
around which the file is organised.
Main definitions #
closedConeOver C—{(λ, x) | λ > 0, x ∈ λ • C} ∪ ({0} ×ˢ 0⁺C)inℝ × E. Named for its conclusion: for nonempty closed convexCit is the closure of the cone generated by the copy ofCat height one (closure_coe_hull_prodMk_one).posHomGen f— the positively homogeneous convex function generated byf:ofEpi KforKthe convex cone generated byepi f, and the greatest positively homogeneous convex minorant offthat is nonpositive at the origin (posHomGen_isGreatest).
Main results #
coe_hull_of_convex— for convexSthe cone generated bySis{0} ∪ ⋃ {t • S | t > 0}, with no convex combinations;coe_hull_convexHullabsorbsconvexHull.closure_coe_hull—cl (cone C) = ⋃ {t • C | t > 0} ∪ 0⁺C(Theorem 9.6 in [^1]), withisClosed_coe_hull_of_isBoundedfor boundedC.epi_lscHull_posHomGen,lscHull_posHomGen,proper_posHomGen— the epigraph formepi (cl k) = ⋃ {epi (fλ) | λ > 0} ∪ epi (f0⁺)is the pointwise formula together with the attainment of its infimum. If0 ∈ dom fthenkis already closed andλ = 0⁺may be dropped (lscHull_posHomGen_eq,posHomGen_eq_iInf_smulRight).closure_convexHull_union,recessionCone_closure_convexHull_union—cl (conv (C ∪ D)) = conv (C ∪ D) + (0⁺C + 0⁺D)and0⁺(cl (conv (C ∪ D))) = 0⁺C + 0⁺D(Theorem 9.8 in [^1]);isClosed_convexHull_union_of_recessionCone_eqis the case of equal recession cones, andclosedProperConvexFn_convFn₂carries it to functions.
Implementation notes #
PointedCone.hull ℝ is Submodule.span ℝ≥0, built from finite ℝ≥0-combinations;
coe_hull_of_convex is the bridge to {0} ∪ ⋃_{t>0} tC, and is what the rest of the file uses.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §8 and §9.
Auxiliary facts about epi and ofEpi #
General facts about the epi-closure operator F ↦ epi (ofEpi F), used below for the positively
homogeneous convex function generated by f.
Positive scaling commutes with the epi-closure. Both sides are the epigraph of (ofEpi F) a;
the proof only uses that a • epi g is an epigraph for a > 0 (epi_smulRight).
The convex cone generated by a convex set is the union of its positive multiples together with the origin.
Taking the convex hull first does not change the convex cone generated.
The cone over a convex set, one dimension up #
The convex cone in ℝ × E generated by {1} × C, for a convex set C: it consists of the
origin together with the pairs (λ, x) with λ > 0 and x ∈ λC.
This cone is the homogenisation of C, and the closure theorems of this file are all read
off its closure.
The closed cone over a set C ⊆ E: the pairs (λ, x) in ℝ × E with λ > 0 and
x ∈ λC, together with {0} × 0⁺C. For a nonempty closed convex C this is exactly the closure
of the convex cone generated by the copy of C at height one
(closure_coe_hull_prodMk_one), and the three closure theorems are all read off it.
Equations
Instances For
Membership of closedConeOver, as a disjunction on the homogenising coordinate.
The convex cone generated by {1} × C sits inside closedConeOver C.
The homogenising coordinate is nonnegative on closedConeOver C.
The half-line over a point of C in a direction of closedConeOver C, in the one form that
covers both branches of the disjunction: for p = (λ, λu) it is the convex combination
(1 - aλ) x + aλ u, and for p = (0, z) it is the recession half-line x + a z.
The closed cone over a set #
closedConeOver C is closed when C is a closed convex set.
The two branches are separated by the sign of the limit of the homogenising coordinates: when it
is positive the points (uₙ).1⁻¹ • (uₙ).2 lie in C and converge; when it is zero,
add_sub_smul_mem_of_mem_closedConeOver passes to the limit and gives the recession half-line.
The closure of the convex cone K generated by {1} × C, one dimension up: for a
nonempty closed convex set C,
cl K = K ∪ {(0, x) | x ∈ 0⁺C}.
The classical proof goes through relative interiors, which needs finite dimensions; this one does
not. closedConeOver C is closed, and each (0, z) with z ∈ 0⁺C is the limit of
(n+1)⁻¹ • (1, x + (n+1) • z) for any x ∈ C.
closedConeOver C is convex when C is a nonempty closed convex set: it is the closure of a
convex cone.
The slices of a sum of two cones #
The level-zero slice of closedConeOver C + closedConeOver D is 0⁺C + 0⁺D: the two
homogenising coordinates are nonnegative and sum to zero, so both vanish.
The level-one slice of closedConeOver C + closedConeOver D is contained in
conv (C ∪ D) + (0⁺C + 0⁺D): the two homogenising coordinates are nonnegative and sum to one, so
they are the weights of a convex combination, with a vanishing weight contributing a direction of
recession instead. This is the classical ⋃ {λ₁C₁ + λ₂C₂ | λᵢ ≥ 0⁺, λ₁ + λ₂ = 1}, written without
the λᵢ = 0⁺ convention.
The convex cone generated by a closed convex set #
The second coordinate of closedConeOver C is the union of the positive multiples of C
together with 0⁺C: this is the projection the proof below takes.
The second coordinate of the cone over C is the convex cone generated by C.
The closure of the convex cone generated by a closed convex set. Let C be a nonempty
closed convex set not containing the origin, and K the convex cone generated by C. Then
cl K = ⋃ {λC | λ > 0 or λ = 0⁺},
which is the same as K ∪ 0⁺C (closure_coe_hull_eq_union). The hypothesis 0 ∉ C makes the
projection (λ, x) ↦ x proper on the closed cone over C, so that the closed-image theorem
applies; it is not decoration — for C a ball with the origin on its boundary it fails.
The same, in the form "cl K = K ∪ 0⁺C".
The cone generated by a bounded set is closed: the convex cone generated by a nonempty closed bounded convex set not containing the origin is closed.
Boundedness is needed: for C a line in the plane not through the origin, the cone generated by
C is an open half-plane together with the origin.
The positively homogeneous convex function generated by a convex function #
The positively homogeneous convex function generated by f: the function determined by the
convex cone generated by epi f. It lives on the same space as f, and is the greatest
positively homogeneous convex g ≤ f with g 0 ≤ 0 (posHomGen_isGreatest). It is not hom f
of Homogenize.lean, which is this operator applied to the level-1 lift of f and lives on
ℝ × E. The gauge of a convex set C is posHomGen (δ(· | C) + 1), which is what makes
the gauge a special case of the theorem below.
Equations
Instances For
The cone generating posHomGen f lies inside its epigraph.
posHomGen f 0 ≤ 0: the origin lies in the cone generated by epi f.
posHomGen f is convex, with no hypothesis on f: a cone hull is convex.
posHomGen f is positively homogeneous, with no hypothesis on f.
The maximality property of posHomGen f: it dominates every positively homogeneous convex
minorant of f that is nonpositive at the origin.
posHomGen is monotone. A larger function generates a larger positively homogeneous
convex minorant: apply the maximality property to posHomGen f ≤ f ≤ g.
posHomGen f is the greatest positively homogeneous convex minorant of f vanishing (or
worse) at the origin — the property that names it.
Its closure, as an attained infimum #
f 0 > 0 says exactly that epi f misses the origin, the hypothesis of the cone theorem.
The union over λ > 0 of the epigraphs of the functions fλ is the set of positive multiples
of epi f.
At the level of epigraphs: for a closed proper convex f with
f 0 > 0 the closed convex cone generated by epi f is the union of the epigraphs of the
functions fλ, λ > 0, together with the epigraph of f0⁺.
The closed convex cone generated by epi f is itself an epigraph: it is closed, and it is
upward closed in the vertical coordinate because each of the two pieces above is.
The closure of the generated function. For a closed proper convex f with f 0 > 0, the
closure of the positively homogeneous convex function k generated by f has
epi (cl k) = (⋃ {epi (fλ) | λ > 0}) ∪ epi (f0⁺).
Read pointwise this is (cl k) x = inf {(fλ) x | λ > 0 or λ = 0⁺} (lscHull_posHomGen); that the
right-hand side is a union of epigraphs, and not merely the epigraph of the infimum, is exactly
the assertion that the infimum is attained.
Pointwise: (cl k) x = inf {(fλ) x | λ > 0 or λ = 0⁺}.
The attainment statement: whenever (cl k) x is bounded above by a real number, that
bound is already achieved by some (fλ) x with λ > 0, or by (f0⁺) x.
k is proper.
A vertical line in the epigraph of k would make (0, -1) a direction of recession of the closed
convex cone generated by epi f, hence a member of that cone; the description of that cone would
then force either f 0 < 0 or (f0⁺) 0 ≤ -1, and both are excluded.
The function determined by ⋃ {epi (fλ) | λ > 0} is the infimum of the fλ over λ > 0.
The estimate behind the case 0 ∈ dom f. When 0 ∈ dom f, the half-line
(0, f 0) + a (z, ν) stays in epi f for every (z, ν) ∈ 0⁺(epi f), so (fλ) z ≤ λ f 0 + ν for
λ = 1/a; letting a → ∞ puts (z, ν) in the epi-closure of ⋃ {epi (fλ) | λ > 0}. This is why
the term λ = 0⁺ can then be dropped from the infimum.
⋃ {epi (fλ) | λ > 0} sits inside the convex cone generated by epi f.
The case 0 ∈ dom f: the epigraph of k is already the closed
convex cone generated by epi f, so k is closed (lscHull_posHomGen_eq) and λ = 0⁺ may be
dropped from the infimum (posHomGen_eq_iInf_smulRight).
The case 0 ∈ dom f: k is itself closed.
The case 0 ∈ dom f: the term λ = 0⁺ may be dropped, and
k x = inf {(fλ) x | λ > 0} — although the infimum then need not be attained.
The convex hull of a union of two sets #
The key step. Under the recession hypothesis the sum of the closed cones over C and over
D is the closure of a convex cone — hence closed, hence its own recession cone. It is the sum
rule for cones applied one dimension up; the hypothesis transports because a cancelling pair in
the sum must have both homogenising coordinates zero.
The closure of the convex hull of a union. Let C and D be nonempty closed convex sets
such that the only way a direction of recession of C and a direction of recession of D can
cancel is inside the two lineality spaces. Then
cl (conv (C ∪ D)) = conv (C ∪ D) + (0⁺C + 0⁺D) and 0⁺(cl (conv (C ∪ D))) = 0⁺C + 0⁺D.
The right-hand side of the first identity is classically written
⋃ {λ₁C + λ₂D | λᵢ ≥ 0⁺, λ₁ + λ₂ = 1}, with the convention that 0 · C means 0⁺C; the form
here says the same thing without the convention. Both sets have to be nonempty — 0⁺∅ is
everything. The two conclusions are packaged together because they come from one application of
the sum rule for cones, read off the level-one and the level-zero slice of the same sum.
The closure formula: cl (conv (C ∪ D)) = conv (C ∪ D) + (0⁺C + 0⁺D).
The recession-cone formula: 0⁺(cl (conv (C ∪ D))) = 0⁺C + 0⁺D.
Directions of recession survive taking the convex hull: a translation carrying S into S
carries conv S into conv S.
A recession cone absorbs itself: it contains 0 and is closed under addition.
Equal recession cones. The convex hull of the union of two nonempty closed convex
sets with the same recession cone K is closed, and has K as its recession cone.
The cancellation hypothesis is automatic here: if z ∈ K and -z ∈ K then z lies in the
lineality space of both sets.
The convex hull of two functions #
The convex hull of two functions. Two closed proper convex functions with the
same recession function k have a convex hull conv {f, g} that is again closed proper convex,
again with recession function k; and its epigraph is the convex hull of the two epigraphs.
The epigraph identity is the content: conv (epi f ∪ epi g) is closed by the previous result,
hence an epigraph, hence the epigraph of conv {f, g} — and that is at the same time the
statement that the infimum defining conv {f, g} is attained (exists_combo_of_convFn₂_le).
Properness is read off the recession cone: a vertical line would put (0, -1) in epi k.
Attainment: under the same hypothesis the infimum defining conv {f, g} is attained —
every real bound on conv {f, g} at x is realised by an actual convex combination
a • u + b • v = x. In convFn₂_apply the infimum is only approached.