Recession functions #
The recession function f0⁺ of f : E → EReal has as its epigraph the recession cone of the
epigraph of f: epi (f0⁺) = 0⁺(epi f) (epi_recessionFn, for every f). It says how fast f
can grow in each direction: (f0⁺) y ≤ ν means f (x + a • y) ≤ f x + a * ν for all x, a ≥ 0.
The directions with (f0⁺) y ≤ 0 form the recession cone of f, those with (f0⁺) (±y) ≤ 0
its constancy space, and those with (f0⁺) (-y) = -(f0⁺) y its lineality space.
Most of the theory needs only a real vector space with no topology; closedness of epi f enters
exactly where the answer must not depend on the base point x, and is always carried as
IsClosed (epi f), never as ClosedFn f, which also collapses improper functions to ⊥.
Main definitions #
recessionFn f— the recession functionf0⁺, asofEpi (0⁺(epi f)).recessionConeFn f,recessionPointedConeFn f— the recession cone, bare and as aPointedCone.constancySpace f,constancySubmodule f— the constancy space, bare and as aSubmodule ℝ E.linealitySpaceFn f,linealitySubmoduleFn f,linealityFn f— the lineality space offand its dimension.
Main results #
posHomogeneous_recessionFn,convexFn_recessionFn,proper_recessionFn—f0⁺is positively homogeneous and convex, proper whenfis proper and closed whenfis closed; andrecessionFn_apply_eq_iSup_sub:(f0⁺) y = sup {f (x + y) - f x | x ∈ dom f}, reached for closedfby the difference quotients at any onex ∈ dom f(Theorem 8.5 in [^1]).recessionFn_isLeast—f0⁺is the leasthwithf z ≤ f x + h (z - x).tendsto_smulRight_recessionFn—(f0⁺) y = lim_{a ↓ 0} (fa) y.antitone_along_of_liminf_lt_top,forall_antitone_iff_recessionFn_nonpos— a convexfthat does not blow up along one half-line is nonincreasing along the whole line, and(f0⁺) y ≤ 0says exactly that this happens from every base point;ConvexFn.eq_of_le_on_affineSubspaceis the affine-set form.recessionCone_setOf_le,linealitySpace_setOf_le— all nonempty level sets of a closed convexfshare its recession cone and constancy space, and byisBounded_setOf_leone of them is bounded only if all are.forall_eq_add_iff_mk_mem_linealitySpace_epi,linealitySpaceFn_eq_image—fis affine with slopeνalongyexactly when(y, ν)lies in the lineality space ofepi f, whose projection is the lineality space off.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §8.
The recession function #
The recession function f0⁺ of f: the function whose epigraph is the recession cone of
the epigraph of f. It is defined as ofEpi of that cone, which is all one can write down
before knowing the cone is an epigraph; epi_recessionFn then proves epi (f0⁺) = 0⁺(epi f).
Equations
Instances For
The recession condition on (y, ν), unfolded against the epigraph: (y, ν) recedes from
epi f exactly when f (x + a • y) ≤ μ + a * ν whenever f x ≤ μ and a ≥ 0.
The recession condition on (y, ν), in EReal arithmetic: f (x + a • y) ≤ f x + a * ν for
every x and every a ≥ 0. Equivalent to the epigraph form even at improper values, because
⊥ + (r : ℝ) = ⊥ matches "f x ≤ μ for every real μ".
A vertical section of 0⁺(epi f) is upward closed: this is one of the two halves of
IsEpiLike.
The recession cone of an epigraph is an epigraph, with no hypothesis on f whatsoever.
Vertical sections are upward closed because μ + a * ν grows with ν, and they are closed from
below because f (x + a • y) ≤ μ + a * ρ for every ρ > ν forces f (x + a • y) ≤ μ + a * ν.
Neither half needs epi f to be closed or convex.
The defining property of the recession function: its epigraph is the recession cone of the
epigraph. Rockafellar takes this as the definition; here it is a theorem, and it carries no
hypothesis on f.
The ≤-characterisation of f0⁺ against a real bound, in epigraph form.
The ≤-characterisation of f0⁺ against an arbitrary function: f0⁺ is the greatest function
whose epigraph contains 0⁺(epi f).
For a convex f it is enough to test the recession inequality at a = 1: a convex set
recedes in a direction as soon as it is stable under one step in it.
f0⁺ is a positively homogeneous convex function #
A positive multiple of a recession cone is that recession cone: 0⁺C is a cone. This is the
scaling half of recessionPointedCone, in the a • s = s form that
posHomogeneous_iff_isCone_epi asks for.
The recession function is positively homogeneous. No hypothesis on f is needed, because
0⁺(epi f) is a cone for every f.
The recession function is convex. Again no hypothesis on f is needed: 0⁺C is convex
for every C, convex or not.
epi (f0⁺) bundled as a cone. The two theorems above would give it as a ConvexCone ℝ (E × ℝ)
via PosHomogeneous.epiCone, but recessionPointedCone already carries the same set as a
PointedCone ℝ (E × ℝ), with no hypothesis, so that is the bundling recorded here.
f0⁺ is nonpositive at the origin, because 0 recedes from every set.
f0⁺ never takes the value -∞ when f is proper.
Properness is needed on both counts: for f ≡ +∞ the epigraph is empty, 0⁺∅ is everything and
f0⁺ ≡ -∞; and if f takes the value -∞ somewhere, a vertical section of 0⁺(epi f) can be
all of ℝ.
The recession function of a proper convex function is proper.
The difference formula and the least-function property #
Rearranging f (x + y) ≤ f x + r as a difference quotient. The ⊥-freeness hypothesis is
what makes f x real on dom f, and the restriction to dom f is what keeps ⊤ + r = ⊤ from
being read as a constraint.
The difference formula
(f0⁺) y = sup {f (x + y) - f x | x ∈ dom f}.
Convexity enters by letting the recession condition be tested at a = 1 only, and
∀ x, f x ≠ ⊥ is what makes the difference meaningful. Properness is not needed: for
f ≡ +∞ both sides are -∞, the supremum because dom f = ∅.
The inequality f (x + y) ≤ f x + (f0⁺) y: f0⁺ is one such bounding function.
f0⁺ is the least function h for which f satisfies the global inequality
f z ≤ f x + h (z - x) at every pair of points.
Directions of recession #
The recession inequality at ν = 0: (f0⁺) y ≤ 0 means that moving in the direction y
never increases f.
f (x + a • y) is a nonincreasing function of a for every x exactly when
(f0⁺) y ≤ 0.
This half needs no hypothesis on f at all, neither convexity nor properness; the usual
statement carries "proper convex" because it is packaged with the two implications below.
A convex function that fails to blow up along one half-line is nonincreasing along the whole
line: a finite liminf of f (x + a • y) as a → ∞ makes a ↦ f (x + a • y) antitone.
The proof is elementary, and in particular needs no closure, no relative interiors and no finite
dimension: for λ₁ < λ₂ and a real bound μ on f (x + λ₁ • y), write x + λ₂ • y as a convex
combination of x + λ₁ • y and x + λ • y for a very large λ with f (x + λ • y) < α; the
weight on the second point tends to 0, so convexity gives f (x + λ₂ • y) ≤ μ in the limit.
f is constant along every line in the direction y exactly when both (f0⁺) y ≤ 0 and
(f0⁺) (-y) ≤ 0.
A convex function is constant on any affine set on which it is bounded above.
It follows from the line version above, applied along the line through any two points of M, so
no closure and no relative interiors are needed. Finiteness of f on M is not needed either,
since the two inequalities hold whatever value f takes.
The recession cone, constancy space and lineality space of a function #
The recession cone of f — not to be confused with the recession cone of epi f. It is
the horizontal slice {y | (y, 0) ∈ 0⁺(epi f)} of the latter, and it collects the directions in
which f recedes.
Equations
Instances For
The recession cone of f is the horizontal slice of the recession cone of epi f.
The recession cone of f is a convex cone containing the origin, bundled as a
PointedCone ℝ E. No hypothesis on f is needed.
Equations
- Tdaf.ConvexAnalysis.recessionPointedConeFn f = { carrier := Tdaf.ConvexAnalysis.recessionConeFn f, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Instances For
The constancy space of f: the largest subspace inside the recession cone of f, which
collects the directions in which f is constant.
Equations
Instances For
The constancy space is exactly the set of directions along which f is constant.
The constancy space is the lineality space of the recession cone of f, hence a subspace,
bundled as a Submodule ℝ E.
Equations
Instances For
The constancy space is the largest subspace inside the recession cone of f.
Directions in which f is affine #
Two opposite directions of recession of a proper f have nonnegative total slope: adding the
two recession directions gives (0, ν + ρ) ∈ 0⁺(epi f), and (f0⁺) 0 = 0.
A bound on (f0⁺) (-y) is a lower bound on (f0⁺) y.
(y, ν) lies in the lineality space of epi f exactly when (f0⁺) y = ν and
(f0⁺) (-y) = -ν. Properness is what upgrades the inequalities (f0⁺) y ≤ ν,
(f0⁺) (-y) ≤ -ν to equalities.
If (y, ν) lies in the lineality space of epi f, then f (x + a • y) = f x + a * ν on the
forward half-line a ≥ 0.
f is affine with slope ν along the whole line through every x in the direction y
exactly when (y, ν) lies in the lineality space of epi f. No hypothesis on f is needed
for this half.
For proper f, being affine along y with slope ν is (f0⁺) y = ν together with
(f0⁺) (-y) = -ν.
The lineality space of f: the directions in which f is affine, that is the y with
(f0⁺) (-y) = -(f0⁺) y.
Equations
Instances For
The lineality space of f is the image of the lineality space of epi f under the projection
(y, ν) ↦ y.
The lineality space of f is a subspace, bundled as a Submodule ℝ E. It is defined as the
image of linealitySubmodule (epi f) under the projection, so the subspace structure is free, and
coe_linealitySubmoduleFn identifies its carrier with linealitySpaceFn.
Equations
Instances For
The carrier of linealitySubmoduleFn is the lineality space of f.
The lineality of f: the dimension of its lineality space.
Equations
Instances For
An affine direction of recession along which f is bounded below is a direction of
constancy. If y is a direction of recession of a proper f in which f is affine
(y ∈ linealitySpaceFn f) and f is bounded below on the half-line x + a • y, a ≥ 0, issuing
from some x ∈ dom f, then y ∈ constancySpace f. Affineness turns the hypotheses on y into
f (x + a • y) = f x + a * ν with ν = (f0⁺) y ≤ 0, and the lower bound forces ν = 0.
Difference quotients #
The difference quotient (f (x + a • y) - f x) / a is below ν exactly when the point
(x, f x) + a • (y, ν) lies in epi f. This is the translation that turns the difference formula
into a statement about a single half-line.
The difference quotient is nondecreasing in a. Convexity is the whole content:
x + a₁ • y is a convex combination of x and x + a₂ • y.
The recession function of an indicator #
The recession cone of C ×ˢ [0, ∞) — that is, of epi δ(· | C) — is 0⁺C ×ˢ [0, ∞).
The recession function of an indicator function is the indicator function of the recession
cone. Nonemptiness of C is needed: for C = ∅ the left-hand side is the constant -∞, since
epi δ(· | ∅) = ∅ and 0⁺∅ is everything, while the right-hand side is the constant 0.
The recession cone of an indicator function is the recession cone of the set.
Closed functions: the limit formula, and testing at a single base point #
f0⁺ is closed as soon as f is. Only closedness of epi f is used; neither convexity nor
nonemptiness enters.
f0⁺ is a closed function when f is a closed proper function.
One half-line is enough, on epigraphs: for a closed convex f, a single half-line inside
epi f already witnesses a direction of recession.
For a closed convex f the recession condition may be tested at a single point of dom f.
This is the sharpening that the difference-quotient formula rests on.
The difference-quotient formula: for a closed convex f and any one x ∈ dom f,
(f0⁺) y = sup {(f (x + a • y) - f x) / a | a > 0}. Closedness is what makes the answer
independent of x.
The limit formula: the difference quotient increases to (f0⁺) y as a → ∞.
Monotonicity of the quotient (monotone_coe_inv_mul_sub) is what turns the supremum into a
limit.
When f is closed, a single x ∈ dom f along which f is nonincreasing already forces
(f0⁺) y ≤ 0.
For a closed f, a single x ∈ dom f along which f is affine with slope ν already forces
(f0⁺) y = ν and (f0⁺) (-y) = -ν.
For a closed convex f, every nonempty level set {x | f x ≤ α} has the same recession cone,
namely the recession cone of f.
The lineality half: every nonempty level set of a closed convex f has the constancy
space of f as its lineality space.
The limit of the right scalar multiples #
(f0⁺) y = lim_{a ↓ 0} (fa) y is proved here directly from the recession calculus, rather than
through the homogenisation hom f: the latter route would need cl (hom f), since
hom f (0, ·) = δ(· | 0) and not f0⁺. The proof splits into the two halves of tendsto_order,
and only the upper half needs a point of dom f on the ray through y.
The lower half, and the half that carries the closedness hypothesis: no fa can dip below
(f0⁺) y in the limit. It is the sequential criterion for a direction of recession applied to
aₙ⁻¹ • (y, β) in epi f.
The upper half, from a point θ • y ∈ dom f on the line through y: (fa) y eventually
stays below any bound exceeding (f0⁺) y. θ = 1 is the case y ∈ dom f and θ = 0 the case
0 ∈ dom f; no other point of dom f helps, because the endpoint of the half-line must lie on
the line through y. This half needs no topology on E: it is the one-step recession test plus
one limit in ℝ.
For a closed proper convex f, the recession function is the limit of the right scalar
multiples fa as a ↓ 0, at every y ∈ dom f — and, by
tendsto_smulRight_recessionFn_of_zero_mem_dom, at every y when 0 ∈ dom f.
Global form: when 0 ∈ dom f the limit formula holds at every y, with no condition on
y at all.
Slices of a function of two variables #
A closed convex function of two variables has the same recession function on every slice
x ↦ G (u, x) with non-empty effective domain: it is "one half-line is enough", read on the
epigraph.
A recession direction of one slice of a closed convex G is a recession direction of every
slice, with the same bound. The slice inequality at a single point exhibits a half-line of epi G
in the direction ((0, y), ν), and for a closed convex set one half-line is enough.
No hypothesis is placed on u: when G (u, ·) ≡ ⊤ the conclusion holds vacuously.
One recession function for all slices: a closed convex function of two variables has the same recession function on any two slices with non-empty effective domain.
Bounded level sets #
For a closed convex f, if one nonempty level set is bounded then every nonempty level set
is. Finite-dimensionality enters only through the criterion for boundedness.