Recession cones and lineality spaces #
The recession cone 0⁺C of a set C collects the directions in which C recedes: the y such
that every half-line {x + a • y | a ≥ 0} issuing from a point of C stays inside C. The
lineality space is the largest subspace it contains, 0⁺C ∩ (-0⁺C), the directions in which C
is linear. Most of the theory is algebraic; closedness of 0⁺C and the limit descriptions need
only a real topological vector space, and finite dimensionality enters only for boundedness.
Main definitions #
recessionCone C,recessionPointedCone C—0⁺C, bare and as aPointedCone ℝ E.linealitySpace C,linealitySubmodule C,lineality C— the lineality space, bare, as aSubmodule ℝ E, and its dimension.
Main results #
recessionCone_eq_add_subset— for convexC,0⁺C = {y | C + y ⊆ C}. That0⁺Cis a convex cone containing the origin needs no hypothesis (recessionPointedCone).recessionCone_setOf_forall_le— the recession cone of a system of weak linear inequalities is the homogeneous system;recessionCone_coe_affineSubspacedoes the same for affine sets.eq_add_inter_of_isCompl— the decompositionC = L + (C ∩ L')for a complementL'ofL.isClosed_recessionCone—0⁺Cis closed as soon asCis; no convexity, no nonemptiness.mem_recessionCone_iff_exists_tendsto— for nonempty closed convexC,0⁺Cis the set of limits of sequenceslᵢ • xᵢwithxᵢ ∈ Candlᵢ ↓ 0(Theorem 8.2 in [^1]).mem_recessionCone_of_exists_ray— one half-line in the directionyinside a closed convexCforces all of them (Theorem 8.3 in [^1]);recessionCone_iInterandrecessionCone_preimagecarry that to intersections and preimages, andrecessionCone_prod,recessionCone_pisay that a nonempty product recedes coordinatewise.isBounded_iff_recessionCone_eq_zero— a nonempty closed convex set is bounded exactly when it recedes in no direction, andisBounded_inter_of_direction_eqmoves that along parallel slices.iInter_recessionCone_eq_zero_iff_exists_isBounded— the recession hypothesis of Helly's theorem: for closed convex sets with the finite-intersection property, "no common direction of recession" holds exactly when some finite subfamily is bounded.
Implementation notes #
Mathlib's asymptoticCone ℝ C is not 0⁺C: it is always closed and is empty for C = ∅, and
what it computes is 0⁺(cl C) (recessionCone_closure_eq_asymptoticCone; the two agree for
nonempty closed convex sets). 0⁺C itself is algebraic, and is used where there is no topology.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §8 and §21.
The definitions and their algebraic structure #
The recession cone 0⁺C: the directions in which C recedes.
y ∈ 0⁺C when every half-line {x + a • y | a ≥ 0} issuing from a point x of C is contained
in C. The classical definition excludes y = 0, which has no direction; including it is what
makes 0⁺C a cone.
Instances For
Membership in the recession cone, unfolded.
The defining property of a direction of recession.
A direction of recession may be added to any point of C.
0⁺C is a convex cone containing the origin, bundled as a Mathlib PointedCone. No
hypothesis on C is needed; convexity enters only in recessionCone_eq_add_subset, the
description of 0⁺C by a single step.
Equations
- Tdaf.ConvexAnalysis.recessionPointedCone C = { carrier := Tdaf.ConvexAnalysis.recessionCone C, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Instances For
Every direction recedes from the empty set, vacuously.
The recession cone as an intersection of preimages of C. This is what makes it closed
whenever C is; see isClosed_recessionCone. For a > 0 the a-th preimage is
a⁻¹ • (C - x), which is the form Rockafellar's argument uses.
Directions of recession of every member of a family recede from the intersection. The reverse
inclusion needs closedness and convexity; it is recessionCone_iInter.
For a convex set it is enough to test the recession condition at a = 1.
The lineality space of C: the directions in which C is linear.
Equations
Instances For
The lineality space is a subspace, bundled as a Submodule ℝ E. It is Mathlib's
PointedCone.lineal of recessionPointedCone.
Equations
Instances For
The lineality space is the largest subspace inside 0⁺C.
The direct-sum decomposition, for an arbitrary subspace N of the lineality space: if M
is a complement of N, then C = N + (C ∩ M). Only N ⊆ lin C is used, and that extra room is
what the closed-image theorem needs, where the relevant subspace is lin C ∩ ker A.
The direct-sum decomposition: if L' is any complement of the lineality space L of C,
then C = L + (C ∩ L'). The classical statement takes L' = Lᗮ in an inner-product space; that
is the special case.
The recession cone is invariant under z ↦ x + c • z for c > 0. Directions of recession
do not see translations, and positive rescaling permutes the rays of a cone. This is the change of
variables that turns "C recedes in the direction v" into a decreasing family of sets.
The lineality of C: the dimension of its lineality space.
Equations
Instances For
Affine sets and systems of weak linear inequalities #
A subspace is its own recession cone.
A pointed convex cone is its own recession cone. This is what makes the sum rule for cones a special case of the sum rule for sets: for cones the recession hypothesis is a hypothesis about the cones themselves.
The recession cone of a nonempty affine set is the subspace parallel to it.
The lineality space of a nonempty affine set is the subspace parallel to it.
The recession cone of the solution set of a system of weak linear inequalities is the solution set of the corresponding homogeneous system.
The lineality space of the solution set of a system of weak linear inequalities is given by the corresponding system of equations.
Products, and preimages under a linear map #
The recession cone of a product is the product of the recession cones. Both factors must be
nonempty: 0⁺(C ×ˢ ∅) = 0⁺ ∅ = univ, which is not 0⁺C ×ˢ univ unless 0⁺C is everything.
The lineality space of a product is the product of the lineality spaces.
A family of recession directions is a recession direction of the product set. Unconditional,
and the Set.pi form of prod_recessionCone_subset.
The recession cone of a product set is the product of the recession cones. The Set.pi
form of recessionCone_prod; the nonemptiness hypothesis is there for the same reason, that
testing one coordinate needs a witness in all the others.
The lineality space of a product set is the product of the lineality spaces.
One inclusion of the preimage rule, valid with no hypothesis at all.
Closedness, limits, and one-half-line criteria #
The sequence (n+1)⁻¹ tends to 0. Mathlib states this as 1 / (n + 1).
The closure of a pointed convex cone is its own recession cone. PointedCone.closure
supplies the cone structure on cl K; recessionCone_coe_pointedCone then applies verbatim.
The recession cone of a closed set is closed. No convexity, no nonemptiness and no local
compactness are needed: by recessionCone_eq_iInter, 0⁺C is an intersection of preimages of C
under the continuous maps y ↦ x + a • y.
Directions of recession survive taking the closure. The reverse inclusion is false: for
C = {(s, t) | s > 0, t > 0} ∪ {0} in ℝ², 0⁺(cl C) is the closed quadrant while 0⁺C is C
itself.
The sequence (n+1)⁻¹ • (x + (n+1) • y) converges to y: the witness for the easy half of
the sequential description, and what makes one half-line enough.
The hard half of the sequential description: a limit of lᵢ • xᵢ with xᵢ ∈ C and
lᵢ ↓ 0 is a direction of recession of a closed convex C. Finite-dimensionality is not needed:
(1 - a lᵢ) • x + (a lᵢ) • xᵢ lies in C once a lᵢ ≤ 1, and converges to x + a • y.
The easy half: every direction of recession of a nonempty set is a limit of lᵢ • xᵢ
with xᵢ ∈ C and lᵢ ↓ 0.
For a nonempty closed convex set, 0⁺C is exactly the set of limits of sequences lᵢ • xᵢ
with xᵢ ∈ C and lᵢ ↓ 0.
One half-line is enough: if a closed convex set C contains even one half-line in the
direction y, it contains every half-line in that direction issuing from a point of C.
For a closed convex set containing the origin, 0⁺C = ⋂_{ε > 0} ε • C.
The recession cone of an intersection of closed convex sets with a common point is the intersection of the recession cones.
The same over a subfamily: the recession cone of ⋂ i ∈ s, C i is
⋂ i ∈ s, 0⁺Cᵢ. Stated with a bare predicate rather than a Set or a Finset, so that it applies
to either spelling of the bounded intersection.
The binary form: 0⁺(C ∩ D) = 0⁺C ∩ 0⁺D for closed convex sets that meet.
A convex set with nonempty interior has the same directions of recession as its interior and
as its closure. The classical statement uses the relative interior in place of interior.
The bridge to Mathlib's asymptoticCone #
Every direction of recession of a nonempty set lies in Mathlib's asymptoticCone.
For a closed convex set, Mathlib's asymptoticCone is contained in the recession cone.
For a nonempty closed convex set, 0⁺C is Mathlib's asymptoticCone ℝ C.
In general Mathlib's asymptoticCone ℝ C is the recession cone of the closure of C — the
"asymptotic cone" of the older literature.
Preimages under a linear map #
0⁺(A⁻¹ D) = A⁻¹ (0⁺D) for a closed convex D with nonempty preimage. Continuity of A is
not needed — one half-line is enough inside D, not inside A ⁻¹' D — so the domain E
carries no topology.
Bounded sets and balls #
A nonempty bounded set recedes in no direction. Neither closedness, nor convexity, nor finite-dimensionality is needed.
The recession cone of a closed ball is trivial.
The recession cone of A ⁻¹' (closedBall x ε) is the kernel of A. This is the computation
the closed-image theorem runs on, and it needs no topology on the domain.
Boundedness #
A nonempty closed convex set is bounded exactly when it recedes in no direction. This is
the one place in this file where finite-dimensionality is used, and it enters through Mathlib's
isBounded_iff_asymptoticCone_subset_singleton.
Contrapositive form: an unbounded closed convex set recedes in some nonzero direction.
A nonempty closed convex set is compact exactly when it recedes in no direction.
If M ∩ C is nonempty and bounded for a closed convex C and an affine set M, then
N ∩ C is bounded for every affine set N parallel to M.
A family of closed sets whose recession cones meet only at the origin has a finite
subfamily whose recession cones already meet only at the origin. Convexity is not used: 0⁺C is a
closed cone, so the unit sphere is covered by the complements of finitely many of them.
The recession hypothesis of Helly's theorem: for a family of closed convex sets every
finite subfamily of which has a common point, having no common direction of recession holds if
and only if some finite subfamily has a bounded intersection. Neither direction needs the
recession cone of the whole intersection: ⇒ applies the boundedness criterion to a finite
subfamily produced by compactness of the unit sphere, and ⇐ reads it backwards through the
recession cone of an intersection.