When is a linear image closed? #
A linear image A C of a convex set need not be closed. It is closed, and its recession cone is
the image of the recession cone, as soon as
0⁺(cl C) ∩ ker A ⊆ lin (cl C),
that is, as soon as every direction of recession of cl C killed by A is also one backwards.
Sums of sets, images and sums and infimal convolutions of functions, and pointwise suprema follow.
Main results #
isClosed_image_of_recessionCone_inter_ker,recessionCone_image_of_recessionCone_inter_ker— the closedness and recession-cone halves under the reduced hypothesis0⁺C ∩ ker A ⊆ {0};Convex.closure_image_eq_and_recessionConeand its three components are the full statement (Theorem 9.1 in [^1]), andimage_recessionCone_subsetis the unconditional inclusion.Convex.isClosed_add,Convex.closure_add_eq,Convex.recessionCone_add— the same three conclusions for a sumC + D, with the no-cancellation, bounded and conic cases following.closedProperConvexFn_mapLin— a linear image of a closed proper convex function is closed proper convex, and the infimum defining it is attained.closedProperConvexFn_infConv_of_recessionFn_symm,closedProperConvexFn_infConv— the same for infimal convolution, under a symmetry and under a positivity hypothesis.ClosedProperConvexFn.add,closedProperConvexFn_finsetSum,recessionFn_add,clFn_add— a sum of closed proper convex functions whose effective domains share a point is closed proper convex, its recession function is the sum, andcl (f + g) = cl f + cl g.isClosed_epi_iSup,recessionFn_iSup,lscHull_iSup— pointwise suprema;isClosed_epi_compLin,recessionFn_compLin,clFn_compLin— composition with a linear map.
Implementation notes #
Both halves come from one compactness argument: a decreasing sequence of nonempty closed convex
sets, each with recession cone {0}, is a sequence of compact sets, so its intersection is
nonempty. The hypothesis says exactly that N := 0⁺(cl C) ∩ ker A is a subspace, and splitting
cl C = N + (cl C ∩ M) along a complement M of N leaves the image unchanged while cutting the
recession cone down to one that meets ker A only at 0. Finite dimensionality of the source is
used only to get that compactness; the target space needs none.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §9.
Rays in a convex set #
A ray in a convex set is filled in from its base point: if x₀ and x₀ + c • z both lie
in C, so does x₀ + b • z for every 0 ≤ b ≤ c.
Convex.add_smul_mem is the same statement with b / c in place of b; this form is the one that
comes up when the endpoints are indexed by ℕ.
The unconditional inclusion #
A linear map carries directions of recession forward: A (0⁺C) ⊆ 0⁺(A C). No convexity,
no closedness, no hypothesis on A.
Images under the reduced hypothesis #
Closedness under the reduced hypothesis: if a closed convex set recedes in no direction
of ker A other than 0, its image under A is closed.
The recession cone of the image, under the reduced hypothesis: 0⁺(A C) = A (0⁺C).
Closedness of a linear image #
The reduction step. The hypothesis says exactly that N := 0⁺(cl C) ∩ ker A sits inside
the lineality space, hence is a subspace. Splitting cl C along any complement M of N
produces a set with the same image, the same image of the recession cone, and the reduced
hypothesis 0⁺ ∩ ker A ⊆ {0}. It is packaged as an existential so that the closedness half and
the recession-cone half can both consume it.
Closedness of a linear image: if cl C recedes in no direction of ker A other than
those it also recedes in backwards, then A (cl C) is closed.
The closure of a linear image: cl (A C) = A (cl C).
The recession cone of a linear image: 0⁺(A (cl C)) = A (0⁺(cl C)).
The closure and the recession cone of a linear image, both conclusions together.
Sums of sets #
The sum C + D is the image of C ×ˢ D under the linear map (x, y) ↦ x + y. This is what
turns a question about a sum into a question about a linear image.
The cancellation hypothesis for two sets, transported to the product.
Closedness of a sum: the sum of two closed convex sets is closed as soon as the only way a
direction of recession of C and a direction of recession of D can cancel is inside the two
lineality spaces.
The closure of a sum: cl (C + D) = cl C + cl D.
The recession cone of a sum: 0⁺(cl C + cl D) = 0⁺(cl C) + 0⁺(cl D).
Sums under a no-cancellation hypothesis #
The no-cancellation hypothesis implies the lineality one: if no direction of recession of C
has its opposite among the directions of recession of D, the only cancelling pair is (0, 0),
which lies in both lineality spaces.
The sum of two closed convex sets is closed as soon as no direction of recession of one is the opposite of a direction of recession of the other.
Under the same hypothesis, 0⁺(C + D) = 0⁺C + 0⁺D.
A bounded summand suffices: a bounded set recedes in no direction, so the hypothesis is
automatic and C + D is closed.
The closure of a sum of two pointed convex cones: the cancellation hypothesis reads on
the closures, and gives cl (K + L) = cl K + cl L.
Images of functions #
The hypothesis at the level of the epigraph: (z, 0) is a direction of recession of epi f
exactly when f recedes in the direction z, and it lies in the lineality space exactly when f
is constant along z.
The image of a function under a linear map: the image of a closed proper convex function
is again closed proper convex, and the infimum defining it is attained, provided f is constant
along every direction of recession that A kills.
The three conclusions are packaged together because they come from one application of the image
theorem to epi f: the epigraph identity is the statement that the infimum is attained, and
closedness and properness are read off it.
Attainment on its own: under the same hypothesis the infimum defining (A f) y is
attained whenever it is bounded above by a real.
Infimal convolution #
The positivity hypothesis, transported to the epigraphs: a direction of recession of epi f
whose opposite recedes from epi g has to be zero.
The vertical coordinate is what makes this more than a restatement: at z = 0 the hypothesis says
nothing, and it is properness — f0⁺ 0 = g0⁺ 0 = 0 — that pins the vertical coordinate to 0.
Call z a direction of joint recession for f and g when
(f0⁺) z + (g0⁺) (-z) ≤ 0; it is the direction in which f □ g fails to increase. If the set of
such directions is symmetric, then a direction of recession of epi f whose opposite recedes from
epi g lies in the lineality space of epi f, and its opposite in that of epi g — which is the
hypothesis of Convex.isClosed_add.
The vertical coordinates are what make this more than a restatement: the hypothesis speaks only
about directions in E, and it is properness — through le_recessionFn_of_neg_le — that pins the
two vertical coordinates against each other.
Infimal convolution under a symmetry hypothesis. If f and g are closed proper convex
and the set of directions of joint recession — those z with (f0⁺) z + (g0⁺) (-z) ≤ 0 — is
symmetric, then f □ g is a closed proper convex function, the infimum defining it is attained,
and (f □ g)0⁺ = f0⁺ □ g0⁺.
This is strictly weaker in hypothesis than closedProperConvexFn_infConv, which asks the set of
directions of joint recession to be {0}. Symmetry allows a whole subspace of directions along
which f and g are affine with opposite slopes; f = g = 0 is already such a pair, and the
conclusions hold for it.
Properness is where the symmetry does its work. A vertical line in epi f + epi g produces
directions with (f0⁺) z + (g0⁺) (-z) ≤ -1; symmetry then forces the reversed sum to be ≤ 0
too, and (f0⁺) (-z) + (g0⁺) z ≥ 1 by le_recessionFn_of_neg_le.
The positivity hypothesis implies the symmetry one: if the only direction of joint recession
is 0, the set of them is trivially symmetric.
Infimal convolution under a positivity hypothesis. If f and g are closed proper convex
functions with (f0⁺) z + (g0⁺) (-z) > 0 for every z ≠ 0, then f □ g is a
closed proper convex function, the infimum defining it is attained, and
(f □ g)0⁺ = f0⁺ □ g0⁺.
The three conclusions come from one application of the no-cancellation sum rule to epi f and
epi g: the epigraph identity epi (f □ g) = epi f + epi g is the attainment statement, since
a sum of epigraphs is an epigraph exactly when every infimum defining f □ g is achieved.
The hypothesis is stronger than it needs to be: it is enough that the set of directions of joint
recession be symmetric, not that it be {0}. That is
closedProperConvexFn_infConv_of_recessionFn_symm, of which this is a specialisation.
Attainment for infimal convolution, under the symmetry hypothesis: the infimum defining
(f □ g) x is attained whenever it is bounded above by a real.
Attainment for infimal convolution, under the positivity hypothesis.
Sums of functions #
A sum of two closed proper convex functions is again closed proper convex, as soon as it
is not identically +∞.
Lower semicontinuity of the sum is Mathlib's LowerSemicontinuous.add', whose explicit continuity
hypothesis is exactly what properness supplies: neither summand is ⊥, so EReal addition is
continuous at every pair of values.
A finite sum: f₁ + ⋯ + fₘ is closed proper convex as soon as the summands are and their
effective domains share a point.
The binary rule needs a point of the domain at every step, so the induction carries one: what is
proved is the conjunction of the conclusion with x₀ ∈ dom (∑ i ∈ s, gᵢ).
The recession function of a sum: (f + g)0⁺ = f0⁺ + g0⁺.
Both sides are limits of difference quotients based at one common point of dom f ∩ dom g, and
Tdaf.EReal.coe_mul_sub_add_coe_mul_sub says the quotients themselves add up. Uniqueness of
limits finishes; closedness is what makes a single base point enough.
The lower semicontinuous hull of a sum: when the two effective domains share a relative interior point, the hull of a sum is the sum of the hulls.
Each of the three hulls at y is a limit along one and the same segment based at the common
point, which lies in ri (dom (f + g)) because the relative interior of an intersection of convex
sets with a common relative interior point is the intersection of the relative interiors.
The closure of a sum: cl (f + g) = cl f + cl g when the effective domains share a
relative interior point.
Pointwise suprema #
A pointwise supremum of closed functions is closed, because its epigraph is an intersection of epigraphs. Nothing else is needed.
The recession function of a pointwise supremum: (⨆ i, fᵢ)0⁺ = ⨆ i, (fᵢ)0⁺. It is the
recession cone of an intersection, read through epi_recessionFn.
The lower semicontinuous hull of a pointwise supremum: cl (⨆ i, fᵢ) = ⨆ i, cl fᵢ.
A point x lying in every ri (dom fᵢ) at which the supremum is finite supplies a common
relative interior point of the epigraphs: (x, μ) lies in every ri (epi fᵢ) for any real μ
above the supremum, which is what lets the closure pass inside the intersection.
Composition with a linear map #
Closedness of a composition: g A is closed whenever g is, with no relative interior
hypothesis, because epi (g A) is a preimage of epi g under a continuous map.
The recession function of a composition: (gA)0⁺ = (g0⁺)A. It is the recession cone of a
preimage, read through epi_recessionFn.
The relative interior hypothesis, transported to epigraphs: if A x is a relative interior
point of dom g, some (x, μ) is carried into ri (epi g).
The lower semicontinuous hull of a composition: cl (g A) = (cl g) A as soon as some
A x is a relative interior point of dom g. It is the rule for the closure of a preimage,
applied to epi g.
The same for clFn: cl (g A) = (cl g) A for proper g.