Rockafellar, §7: Closures of Convex Functions #
Lower semicontinuity, the lower semicontinuous hull, the closure cl f of a convex function, and
closed convex functions. All 17 numbered results of §7 are formalized.
Lower semicontinuity is Mathlib's LowerSemicontinuous; the lower semicontinuous hull is
lscHull, characterised as the greatest lsc minorant by lscHull_isGreatest; the closure of a
convex function is clFn; and a closed convex function is one with ClosedFn f. Two unnumbered
claims of the text are recorded as closedFn_iff_lowerSemicontinuous_of_proper and
closed_improper_eq_const — the only closed improper convex functions are the constants +∞
and −∞.
The cl f case split, and the book's slip about epi (cl f) #
Rockafellar defines cl f by cases: the lower semicontinuous hull when f is nowhere −∞, and
the constant −∞ otherwise. The backbone's clFn branches on the hull taking −∞ rather than
on f doing so, which is the standard Γ-regularisation and the only branch that keeps
f** = cl f true; ConvexFn.clFn_eq_lscHull is the proof that the two descriptions agree.
The book then asserts epi (cl f) = cl (epi f) "by definition". That is false for improper
f: when f takes the value −∞, cl f ≡ −∞ and epi (cl f) is all of ℝⁿ⁺¹, while
cl (epi f) is cl (dom f) × ℝ. The identity holds for the hull with no hypothesis at all
(epi_lscHull), and for cl f exactly when f is proper. No statement below inherits the slip:
every use of it goes through epi_lscHull or through properness.
References #
- R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §7.
The definitions of §7 #
Rockafellar §7, the sentence defining the lower semicontinuous hull: "there exists a
greatest lower semi-continuous function (not necessarily finite) majorized by f".
Rockafellar §7: "For a proper convex function, closedness is thus the same as lower
semi-continuity." Only the ≠ -∞ half of properness is used, and convexity is not used at all.
Rockafellar §7: "the only closed improper convex functions are the constant functions +∞
and −∞". Convexity is not needed.
Dimension bookkeeping #
Corollary 6.3.1 in the form Corollary 7.4.1 and Theorem 7.6 need; dim itself is §1's.
Non-empty sets with the same affine hull have the same dimension.
Theorem 7.1 #
Theorem 7.1. Let f be an arbitrary function from ℝⁿ to [-∞, +∞]. Then
the following conditions are equivalent:
(a) f is lower semi-continuous throughout ℝⁿ;
(b) {x | f x ≤ α} is closed for every α ∈ R;
(c) the epigraph of f is a closed set in ℝⁿ⁺¹.
Neither convexity nor finite dimension enters; the book's ℝⁿ⁺¹ is Rn n × ℝ.
Theorem 7.2 and its corollaries #
Theorem 7.2. If f is an improper convex function, then f x = -∞ for every
x ∈ ri (dom f). Thus an improper convex function is necessarily infinite except perhaps at
relative boundary points of its effective domain. No properness hypothesis is added: the theorem is
about improper functions.
Corollary 7.2.1. A lower semicontinuous improper convex function has no finite values.
Corollary 7.2.2. Let f be an improper convex function. Then cl f is a
closed improper convex function which agrees with f on ri (dom f).
Note that the agreement is not obtained from epi (cl f) = cl (epi f), which fails exactly in
this improper case.
Corollary 7.2.3. If f is a convex function whose effective domain is
relatively open (for instance if dom f = ℝⁿ), then either f x > -∞ for every x, or f x is
infinite for every x.
Lemma 7.3 and its corollaries #
Lemma 7.3. For any convex function f, ri (epi f) consists of the pairs
(x, μ) such that x ∈ ri (dom f) and f x < μ < ∞.
The book's μ < ∞ is carried by the type: the second component of a point of ℝⁿ⁺¹ = Rn n × ℝ is a
real number.
Corollary 7.3.1. Let α be a real number, and let f be a convex function
such that, for some x, f x < α. Then actually f x < α for some x ∈ ri (dom f).
Corollary 7.3.2. For convex f and convex C with ri C ⊆ dom f: if f x < α for some
x ∈ cl C, then f x < α for some x ∈ ri C.
Corollary 7.3.3. For convex f finite on a convex set C: if f x ≥ α throughout C,
then f x ≥ α throughout cl C. Stated in the book's form, which needs f ≠ -∞ only on C,
where the backbone's ConvexFn.le_of_mem_closure assumes it globally.
Corollary 7.3.4. If convex f and g have ri (dom f) = ri (dom g) and agree there,
then cl f = cl g. No improper case split is needed, unlike in the book, because clFn is a
function of lscHull alone.
Theorem 7.4 and its corollaries #
Theorem 7.4. Let f be a proper convex function on ℝⁿ. Then cl f is a
closed proper convex function. Moreover, cl f agrees with f except perhaps at relative
boundary points of dom f — that is, off cl (dom f) \ ri (dom f).
Corollary 7.4.1. If f is a proper convex function, then dom (cl f) differs from dom f
at most by including some additional relative boundary points of dom f. In particular,
dom (cl f) and dom f have the same closure and relative interior, as well as the same dimension.
The dimension clause is dim_eq_of_closure_eq, which belongs to §6.
Corollary 7.4.2. If f is a proper convex function such that dom f is an
affine set (which is true in particular if f is finite throughout ℝⁿ), then f is closed.
IsAffineSet and its bridge to AffineSubspace are §1's (Section01.lean).
Theorem 7.5 and its corollary #
Theorem 7.5. Let f be a proper convex function, and let x ∈ ri (dom f). Then
(cl f) y = lim_{λ ↑ 1} f ((1 - λ) x + λ y) for every y. The book's λ ↑ 1 is the filter
𝓝[<] (1 : ℝ).
Theorem 7.5, parenthetical clause: the formula is also valid for improper f and
y ∈ cl (dom f). The restriction to cl (dom f) is not decorative — off it the function along
the segment is eventually +∞.
Corollary 7.5.1. For a closed proper convex function f, one has
f y = lim_{λ ↑ 1} f ((1 - λ) x + λ y) for every x ∈ dom f and every y.
The backbone proves this directly rather than through Theorem 7.5 and a restriction to a line, so no relative interiors appear.
Theorem 7.6 and its corollary #
For α above the infimum of a convex f, the set {x ∈ ri (dom f) | f x < α} has the same
affine hull as dom f, hence the same dimension. The step Theorem 7.6's dimension clause needs;
the book takes it by a slice dimension count, this by the line segment principle.
Theorem 7.6. For proper convex f and real α > inf f, the level sets {x | f x ≤ α}
and {x | f x < α} have the same closure {x | (cl f) x ≤ α}, the same relative interior
{x ∈ ri (dom f) | f x < α}, and the same dimension as dom f.
Corollary 7.6.1. If f is a closed proper convex function whose effective
domain is relatively open (in particular if dom f is an affine set), then for
inf f < α < +∞ one has ri {x | f x ≤ α} = {x | f x < α} and
cl {x | f x < α} = {x | f x ≤ α}.
The book's α < +∞ is carried by α : ℝ. The two hypotheses split: the first formula needs only
relative openness of dom f, and the second only closedness.