Closures of convex functions #
Two operations on functions f : E → EReal over a real topological vector space: the lower
semicontinuous hull lscHull f, whose epigraph is closure (epi f), and the closure clFn f of
a convex function, which is that hull except that it is flattened to the constant ⊥ when the hull
takes the value ⊥ anywhere.
Main definitions #
lscHull f— the lower semicontinuous hull,ofEpi (closure (epi f)).clFn f— the closure of a convex function.ClosedFn f—fis closed, i.e.clFn f = f.ClosedProperConvexFn f— closed, proper and convex, bundled; the standing hypothesis of the duality theory, and the classconjEquivandsupportEquivare bijections between.lscHullClosure,clFnClosure— both operations asClosureOperators on(E → EReal)ᵒᵈ.
Main results #
lowerSemicontinuous_iff_isClosed_epi,lowerSemicontinuous_iff_isClosed_le— lower semicontinuity, closed sublevel sets and a closed epigraph coincide.epi_lscHull—epi (lscHull f) = closure (epi f), unconditionally; the workhorse of the file.isGreatest_lscHull—lscHull fis the greatest lower semicontinuous minorant off.closedFn_iff—fis closed exactly when it is the constant⊥, or lower semicontinuous and never⊥.iInf_clFn_eq_iInf—fandcl fhave the same infimum.ConvexFn.eq_bot_or_eq_top— a lower semicontinuous improper convex function has no finite values. This replaces the relative-interior dichotomy outside finite dimensions.exists_affine_le_of_closed_proper— a closed proper convex function on a locally convex space has a continuous affine minorant; the keystone of Fenchel–Moreau.tendsto_lscHull_along_segment,tendsto_along_segment_of_closed_proper— the closure as a limit along a segment, withinterior (epi f)in place ofri (epi f).lscHull_le_setOf—{x | (cl f) x ≤ α} = ⋂_{μ > α} cl {f ≤ μ}, the level sets of the closure, in the part that does not need relative interiors.lscHull_eq_liminf,clFn_eq_liminf_or— the hull and the closure asliminf f (𝓝 x).posHomogeneous_lscHull,posHomogeneous_clFn— both hulls preserve positive homogeneity.closedProperConvexFn_coe_affineMap— a continuous affine function is closed proper convex.
Implementation notes #
clFn branches on lscHull f, not on f as Rockafellar does. The two agree for convex f on
ℝⁿ but not in general, and branching on f would make Fenchel–Moreau
false: a discontinuous linear functional g on an infinite-dimensional space is convex, finite and
proper, yet its kernel is dense, so lscHull g ≡ ⊥ and g has no continuous affine minorant at
all. Branching on the hull is the standard Γ-regularization and makes f** = clFn f
unconditional; the price is that Proper f → Proper (clFn f) is finite-dimensional and appears as
ConvexFn.proper_clFn in Tdaf/Analysis/Convex/RelativeInterior.lean, together with the
relative-interior dichotomy itself.
References #
- R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §7.
Lower semicontinuity #
A function is lower semicontinuous exactly when its epigraph is closed.
A function is lower semicontinuous exactly when every sublevel set {x | f x ≤ α} with α
real is closed.
The lower semicontinuous hull and the closure of a convex function #
The lower semicontinuous hull of f, the function whose epigraph is the closure of the
epigraph of f: the greatest lower semicontinuous minorant of f.
Equations
Instances For
The closure of a convex function: its lower semicontinuous hull, except that if the hull
takes the value ⊥ anywhere then the closure is the constant function ⊥. Rockafellar branches
on whether f itself takes ⊥, which is equivalent for convex f on ℝⁿ but not in general; see
the module docstring.
Equations
- Tdaf.ConvexAnalysis.clFn f = if ∃ (x : E), Tdaf.ConvexAnalysis.lscHull f x = ⊥ then fun (x : E) => ⊥ else Tdaf.ConvexAnalysis.lscHull f
Instances For
A function is closed when it equals its own closure.
Equations
Instances For
The universal property, easy half. A lower semicontinuous minorant of f is a minorant of
lscHull f, because its epigraph is a closed set containing epi f.
For a lower semicontinuous g, being a minorant of lscHull f is the same as being a minorant
of f.
The closure of f is a minorant of its lower semicontinuous hull; the two differ only in the
exceptional branch.
The hull is a hull #
The workhorse of this file. The epigraph of the lower semicontinuous hull is the closure of
the epigraph, with no hypothesis on f: the closure of an epigraph is again an epigraph.
The universal property. lscHull f is the greatest lower semicontinuous minorant of
f.
A function equals its lower semicontinuous hull exactly when it is lower semicontinuous.
What closedness means. A function is closed exactly when it is the constant ⊥, or is
lower semicontinuous and never takes the value ⊥.
For a function that never takes the value ⊥ — in particular for a proper convex function —
closedness is exactly lower semicontinuity.
The only closed improper convex functions are the constant functions +∞ and −∞.
Convexity is not needed for this direction.
Infima, effective domains and level sets #
f and its lower semicontinuous hull have the same infimum. A constant function is
lower semicontinuous, so ⨅ x, f x is already a minorant of lscHull f.
f and cl f have the same infimum.
dom f ⊆ dom (cl f) ⊆ cl (dom f); this is the second inclusion, which
holds for the hull with no hypothesis on f. It is dom_eq_fst_image_epi pushed through the
continuous projection Prod.fst.
The closure of an improper function is improper. Neither convexity nor finite dimension is
used. The converse — properness is preserved — needs both, and is ConvexFn.proper_clFn in
Tdaf/Analysis/Convex/RelativeInterior.lean.
A point of closure (epi f) at height μ is a limit of points where f is below any ν > μ.
This is the pointwise content of Rockafellar's description of cl f as the infimum of the μ with
x ∈ cl {z | f z ≤ μ}.
The closure of a sublevel set of f is contained in the corresponding sublevel set of the
hull.
The level sets of the closure: {x | (cl f) x ≤ α} = ⋂_{μ > α} cl {x | f x ≤ μ}. Stated
for the hull, which is where the content is; the ri-flavoured half is finite-dimensional and is
not proved here.
lscHull and clFn as closure operators #
Both operations are monotone, idempotent and decreasing, so each is a closure operator on the
order dual of E → EReal. Recording that makes Mathlib's ClosureOperator API available and
identifies LowerSemicontinuous and ClosedFn as the two closedness predicates; the constructor's
hypotheses are literally the universal property.
lscHull, as a closure operator on (E → EReal)ᵒᵈ. Its closed elements are the lower
semicontinuous functions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
clFn, as a closure operator on (E → EReal)ᵒᵈ. Its closed elements are exactly the closed
functions, so ClosedFn is the closedness predicate of a genuine closure operator.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The universal property of the closure. clFn f is the greatest closed minorant of f;
this is the hmin field of clFnClosure, restated without the OrderDual wrapping.
Indicator functions #
The lower semicontinuous hull of an indicator function is the indicator of the closure.
cl δ(· | s) = δ(· | cl s): closing an indicator function closes its set.
Approaching the endpoint of a segment #
The three lemmas below package the filter 𝓝[<] (1 : ℝ) bookkeeping shared by the dichotomy
for improper functions and by the limit formulas for the closure.
Convexity of the hull and of the closure #
The lower semicontinuous hull of a convex function is convex: the closure of a convex set is
convex (Convex.closure), and convexFn_ofEpi turns that back into a convex function.
The closure of a convex function is again convex, in either branch.
The dichotomy for improper convex functions #
"An improper convex function is −∞ on ri (dom f)" is finite-dimensional. Its
lower-semicontinuous consequence below is not, and holds in any topological vector space. It is
also the sharp form: the stronger-sounding "a lower semicontinuous convex function taking ⊥
anywhere is identically ⊥" is false; see eq_bot_of_lsc_of_eq_bot.
The algebraic engine of the dichotomy, valid in any real vector space: if f is convex,
f x₀ = ⊥ and y is in the effective domain, then f is ⊥ on the half-open segment [x₀, y).
The hypothesis y ∈ dom f is needed: for f = restrict {x₀} (fun _ => ⊥) the segment meets
dom f only at x₀.
A lower semicontinuous convex function that takes the value ⊥ somewhere takes it at every
point of its effective domain. Only lower
semicontinuity at y is used, through the limit λ ↑ 1 along the segment from x₀ to y.
A lower semicontinuous improper convex function has no finite values: it is ⊥ on its
effective domain and ⊤ off it.
A lower semicontinuous convex function taking the value ⊥ is ⊥ exactly on its effective
domain, which is therefore closed.
The dichotomy, in the form that is actually true. A lower semicontinuous convex function
that takes the value ⊥ somewhere and is nowhere ⊤ is identically ⊥. The hypothesis hdom is
not removable — see the example at the end of this file — and the sharp unconditional form is
ConvexFn.eq_bot_or_eq_top.
Positively homogeneous functions #
The lower semicontinuous hull of a positively homogeneous function is positively
homogeneous. Positive homogeneity is the epigraph being a cone, epi (lscHull f) is the closure
of epi f, and the closure of a cone is a cone. Convexity is not used anywhere in that chain.
The closure of a positively homogeneous function is positively homogeneous. The improper
branch is a case rather than an exclusion: there cl f is the constant ⊥, and a * ⊥ = ⊥ for
a > 0. The same conclusion for convex f follows from writing cl f as a support function;
neither the pairing that needs, nor convexity, is required here.
Non-negative scalar multiples #
scaleSnd c is continuous. It scales only the real coordinate, so E contributes nothing
beyond its own topology — no ContinuousSMul ℝ E is needed.
A non-negative multiple of a closed function is closed, provided the function never takes
⊥. The ⊥-freedom is what makes closedness of cf equivalent to lower semicontinuity of cf;
given it, epi (cf) is epi f pulled back along the continuous scaleSnd c⁻¹, and at c = 0 the
product is the constant 0.
Closed proper convex functions #
A closed proper convex function: the standing hypothesis of the duality theory, and the
class conjEquiv and supportEquiv are bijections between. The three conditions travel
together throughout the duality theory, so they are bundled rather than repeated.
- convex : ConvexFn f
The epigraph is convex.
- closed : ClosedFn f
fequals its own closure. - proper : Proper f
fis finite somewhere and never-∞.
Instances For
For a proper function, closedness of the epigraph is closedness of the function, so this is the form of the constructor the recession theory uses.
A continuous affine function, read into EReal, is closed proper convex. This is what a
section with affine constraints asks for: an equality constraint a x = 0 enters the theory as the
pair of convex functions a and -a. Continuity is a hypothesis rather than a consequence: on an
infinite-dimensional space a discontinuous linear functional is convex, finite everywhere and
proper, and is not closed. In finite dimensions AffineMap.continuous_of_finiteDimensional
discharges it.
Why the dichotomy needs a hypothesis #
The example below is the reason eq_bot_of_lsc_of_eq_bot carries ∀ x, f x < ⊤: the function
that is ⊥ at the origin of ℝ and ⊤ elsewhere has the vertical line {0} × ℝ as its epigraph,
so it is convex and lower semicontinuous, takes the value ⊥, and is not the constant ⊥.
Affine minorants of closed proper convex functions #
A closed proper convex function has a continuous affine minorant, the keystone of
Fenchel–Moreau. Closedness is essential: for a merely proper convex f the statement is false in
infinite dimensions — a discontinuous linear functional g has dense kernel, so lscHull g ≡ ⊥,
while g is convex, finite everywhere and proper. The proof separates the closed convex set
epi f from the point (x₀, f x₀ - 1); the separating functional cannot be vertical, since a
functional (y, 0) agrees at (x₀, f x₀ - 1) and at (x₀, f x₀) ∈ epi f.
Limits along a segment #
The lower semicontinuous hull of f at y is the limit of f along the segment running
from x to y, provided the segment starts at an interior point of epi f. The classical
hypothesis is x ∈ ri (dom f), which says that the vertical line over x meets ri (epi f);
relative interiors are finite-dimensional, so the general statement uses interior (epi f)
instead. In finite dimensions interior (epi f) may be
empty when ri (epi f) is not, so this is a restriction as well as a generalisation.
The same limit formula for clFn. The exceptional branch has to be ruled out by hand, and it
genuinely can occur: for the function that is ⊥ on a closed ball and ⊤ outside it, clFn f ≡ ⊥
while the limit along a segment ending outside the ball is ⊤. The classical statement carries the
matching restriction y ∈ cl (dom f) in the improper case.
For a closed proper convex f, every x ∈ dom f and every y,
f y = lim_{a ↑ 1} f ((1 - a) • x + a • y). No relative interiors are involved: lower
semicontinuity gives the liminf half for every y, including f y = ⊤, and convexity applied to
the finite values f x and f y gives the limsup half.
The lower semicontinuous hull as a liminf #
Rockafellar writes (cl f)(x) = liminf_{y → x} f(y). In a complete lattice
liminf f (𝓝 x) = ⨆ s ∈ 𝓝 x, ⨅ y ∈ s, f y, which is exactly the value of lscHull at x, so the
identity needs no convexity and no hypothesis on f.
The pointwise liminf of f along the neighbourhood filter is a minorant of f: the
neighbourhood filter contains the point itself.
x ↦ liminf_{y → x} f(y) is lower semicontinuous: a neighbourhood witnessing the bound at x
witnesses it, through its interior, at every nearby point.
The lower semicontinuous hull is a liminf: (lsc f)(x) = liminf_{y → x} f(y), since the
liminf function is a lower semicontinuous minorant of f and a lower semicontinuous function is
at most its own liminf.
Rockafellar's cl f = liminf f, in the regular branch: as soon as the lower semicontinuous
hull is nowhere -∞, the closure of f at x is the liminf of f at x.
Rockafellar's cl f = liminf f, in full. For a convex f the closure at x is the
liminf of f at x, except in the single degenerate case where the left side is -∞ and the
right side is +∞; that case can only arise in the exceptional branch of clFn, where the
dichotomy leaves lscHull f with only the values -∞ and +∞.