Relative interiors of convex sets #
The theory of relative interiors of convex sets in a finite-dimensional real normed space. The
relative interior ri C is the interior of C taken relative to its affine hull; it is Mathlib's
intrinsicInterior ℝ C, so no new definition is introduced, and what this file adds is the
convexity theory that Mathlib.Analysis.Convex.Intrinsic does not carry. Finite dimension also
sharpens several statements about convex functions and about separation that the topological
modules Closure.lean and Separation.lean can state only in dimension-free form.
Main definitions #
ri— scoped notation forintrinsicInterior ℝ, matching Rockafellar's usage.
Main results #
mem_intrinsicInterior_iff— the metric description ofri s: a point of the affine hull lies inri sexactly when some ball of the affine hull around it is contained ins. This is the cornerstone from which the rest of the file is derived.Convex.subset_closure_inter_setOf_pos,Convex.closure_inter_setOf_pos— a convex set on which a linear functional is non-negative and somewhere positive is the closure of the part where the functional is positive; a segment argument with no relative interiors in it, here because it is the density step of the cross-section arguments.Convex.segment_mem_relint— the line segment principle: the half-open segment from a relative interior point towards a point of the closure stays inri C(Theorem 6.1 in [^1]).Convex.relint_nonempty,Convex.affineSpan_relint— a nonempty convex set has a nonempty relative interior, and the same affine hull as it.Convex.interior_subset_relint— the full-dimensional collapseri C = int C, in the direction every caller uses.Convex.closure_relint,Convex.relint_closure—C,ri Candcl Cshare a closure and a relative interior, whenceConvex.closure_eq_iff_relint_eqandConvex.relint_inter_nonempty_of_isOpen.Convex.mem_relint_iff_prolong— the prolongation principle:z ∈ ri Cexactly when every segment ofCending atzcontinues past it (Theorem 6.4 in [^1]).Convex.closure_iInter,Convex.relint_iInter— closure and relative interior commute with an intersection whose relative interiors meet, withConvex.relint_inter_affineandConvex.relint_subset_relint_of_subset_closure.Convex.relint_image— linear images commute withri, withConvex.relint_smulandConvex.relint_add;Convex.relint_preimageandConvex.closure_preimagedo the same for inverse images, provided some point is carried intori D.Convex.mem_relint_prod_iff— relative interior points of a convex set in a product, read off from the projection and the slice;Convex.relint_cone_prodMk_oneapplies it to the cone overC, andConvex.relint_convexHull_unionto the convex hull of a union.ConvexFn.relint_epi— the relative interior of an epigraph, whenceConvexFn.exists_mem_relint_dom_ltandConvexFn.le_of_mem_closure.ConvexFn.eq_bot_of_mem_relint_dom— an improper convex function is−∞onri (dom f).ConvexFn.proper_clFn,ConvexFn.clFn_eq_of_mem_relint_dom— the closure of a proper convex function is proper and agrees with it onri (dom f); withConvexFn.relint_dom_clFnandConvexFn.interior_dom_clFn,dom (cl f)has the same relative interior and the same interior asdom f.ConvexFn.tendsto_lscHull_along_segment_relint— the closure offatyas a limit offalong a segment towardsyfrom a relative interior point ofdom f.ConvexFn.relint_setOf_le,ConvexFn.closure_setOf_le— the relative interior and the closure of a level set, withConvexFn.relint_setOf_lt_eq,ConvexFn.closure_setOf_lt_eqand the relatively open and closed special cases.exists_separatesProperly_iff_disjoint_relint— two nonempty convex sets separate properly exactly when their relative interiors are disjoint (Theorem 11.3 in [^1]).
Implementation notes #
Everything rests on mem_intrinsicInterior_iff, which converts x ∈ ri s — defined in Mathlib
through the subspace topology on affineSpan ℝ s — into a statement about distances in the ambient
space. Rockafellar instead reduces to the full-dimensional case by transporting along an affine
isomorphism; the metric description avoids that transport, and the AddTorsor bookkeeping a change
of ambient space would force on every proof. Finite-dimensionality enters through
intrinsicClosure_eq_closure and through closedness of affine subspaces; results not needing it
carry omit [FiniteDimensional ℝ E].
The convexity lemmas are named Convex.* and shadow the root namespace Convex. Generalised field
notation resolves hC.segment_mem_relint against the root Convex namespace only, so these
lemmas must be applied by their explicit names, Convex.segment_mem_relint hC ….
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §6, §7 and §11.
Rockafellar's ri C, the relative interior of C: Mathlib's intrinsicInterior ℝ C.
Equations
- Tdaf.ConvexAnalysis.termRi = Lean.ParserDescr.node `Tdaf.ConvexAnalysis.termRi 1024 (Lean.ParserDescr.symbol "ri")
Instances For
The positive part of a convex set #
A convex set on which a continuous linear functional is non-negative and somewhere positive is the closure of the part where the functional is strictly positive. This is a segment argument in a topological vector space — no relative interiors, no finite dimension — and it is the density step that every "a closed convex cone is the closure of the cone generated by one of its cross-sections" argument runs on.
The strictly positive part of a convex set is dense in it. If a continuous linear functional
ℓ is non-negative on a convex set C and positive at one of its points x₀, then every point x
of C is a limit of points of C at which ℓ is positive: the segment points
(1 - t) x + t x₀ have ℓ value (1 - t) ℓ x + t ℓ x₀ > 0 for 0 < t ≤ 1. No continuity of ℓ
is needed, the approximating points being produced explicitly.
A convex set is the closure of its strictly positive part, under the hypotheses of
Convex.subset_closure_inter_setOf_pos.
The metric description of ri #
Rockafellar's definition of ri, recovered from Mathlib's intrinsicInterior: a point of
ri s is a point of the affine hull of s around which every point of the affine hull that is
close enough already lies in s.
A set whose affine hull is everything has ri s = int s. In particular this is the case for a
full-dimensional convex set, which is why ri is only interesting in lower dimensions.
The relative interior of an affine set is the set itself: an affine set is relatively open.
An affine combination of two points of an affine subspace lies in it.
The line segment principle #
In finite dimensions an affine subspace is closed, so the closure of a set stays inside its affine hull.
The line segment principle, the engine of the whole section: the half-open segment from a relative interior point of a convex set towards a point of its closure stays in the relative interior.
Convexity and the affine hull of the relative interior #
The relative interior of a convex set is convex.
A nonempty convex set has a nonempty relative interior: Mathlib's
Set.Nonempty.intrinsicInterior, restated with the argument order the rest of the file uses.
Taking the closure never changes the affine hull. No convexity is needed; this is
affineSpan_intrinsicClosure together with intrinsicClosure_eq_closure.
Passing to the relative interior does not change the affine hull, hence does not change the dimension.
For a full-dimensional convex set the affine hull is the whole space and ri C = int C. A
convex set with an interior point is full-dimensional, so the two interiors agree; int C ⊆ ri C
is the half every caller uses, since it makes the relative-interior theorems applicable at an
ordinary interior point.
Interchanging closure and relative interior #
The algebraic identity behind every prolongation argument: prolonging the segment from x past
z by a factor μ ≠ 0 and then travelling from x to that point at parameter μ⁻¹ returns
to z.
Every segment ending at a relative interior point z and starting from a point of the affine
hull can be prolonged slightly beyond z without leaving C. This is the easy half of the
prolongation criterion, stated for the affine hull rather than for C because that is what the
closure results below need.
A linear function that attains its maximum over C at a relative interior point is constant
on C — the half of the relative-boundary criterion below that does not need separation.
Prolonging the segment from x past z stays in C, and a linear function cannot be maximal at
an interior point of a segment without being constant along it. Neither convexity of C nor
continuity of φ is used.
The sign form of the preceding lemma: a linear function that is ≤ 0 on C and vanishes at a
relative interior point vanishes on all of C.
A convex set and its relative interior have the same closure: cl (ri C) = cl C.
A convex set and its closure have the same relative interior: ri (cl C) = ri C.
The relative interior is idempotent: ri (ri C) = ri C, so ri C is relatively open.
Two convex sets have the same closure exactly when they have the same relative interior.
A set sandwiched between ri C and cl C has the same closure as C.
An open set meeting cl C already meets ri C.
The prolongation criterion #
The prolongation principle: z is a relative interior point of a nonempty convex set C
exactly when every segment in C ending at z can be prolonged slightly beyond z inside C.
A point is interior to a convex set exactly when the set absorbs every direction at that
point. The prolongation principle gives the relative-interior version; absorbing every direction
forces the affine hull to be everything, where ri and int agree.
Intersections #
The technical core of the intersection theorem: from a common relative interior point, every point common to all the closures is a limit of points common to all the relative interiors.
When the relative interiors have a common point, closure commutes with intersection. No finiteness is needed.
The easy inclusion ri (⋂ i, C i) ⊆ ⋂ i, ri (C i), valid for an arbitrary index set.
The relative interior commutes with a finite intersection whose relative interiors have a
common point. Finiteness is essential: the intersection of ri [0, 1 + α] over α > 0 is (0, 1],
not ri [0, 1].
Binary intersections, and intersections with an affine set #
Closure commutes with the intersection of two convex sets whose relative interiors meet.
The relative interior commutes with the intersection of two convex sets whose relative interiors meet.
Intersecting with an affine set that meets ri C commutes with the relative interior. This is
the workhorse of the theory of convex functions and of recession cones.
Intersecting with an affine set that meets ri C commutes with the closure.
A convex subset of cl C₁ that is not entirely contained in the relative boundary of C₁ has
its relative interior inside ri C₁.
Images under a linear map #
A linear image commutes with the relative interior. Continuity of A is automatic in finite
dimensions, which is why no hypothesis on A appears.
A linear map carries the closure of a set into the closure of its image: just continuity of
A, needing no convexity.
Scaling commutes with the relative interior: ri (a • C) = a • ri C for every real a,
including a = 0.
The relative interior of a sum is the sum of the relative interiors. Mathlib's
intrinsicInterior_prod_eq supplies the direct-sum half.
The sum of the closures is contained in the closure of the sum.
Inverse images under a linear map #
The set-level identity behind the inverse-image theorem: the graph of A meets the horizontal
slab univ ×ˢ T exactly over A ⁻¹' T. Stated for an arbitrary set M presented as the graph, so
the caller may keep whichever coercion of LinearMap.graph A it already has.
An inverse image under a linear map commutes with the relative interior, provided some point is
carried into ri D. A ⁻¹' D is the projection of graph A ∩ (univ ×ˢ D), so intersection with
an affine set and the image theorem do all the work, the relative interior hypothesis feeding the
former.
The same for closures. One inclusion is continuity of A; the other runs through the same
projection of the graph.
A product set is the intersection of the preimages of its factors under the coordinate projections.
Over a Finset: the relative interior of a finite intersection is the intersection of the
relative interiors, as soon as the latter has a point in common. This is Convex.relint_iInter
read over the subtype ↥s.
The relative interior of a product of convex sets is the product of the relative interiors.
This is the Set.pi form of intrinsicInterior_prod_eq; unlike that one it needs finite dimension,
being Convex.relint_iInter applied to the coordinate preimages.
Slices of a convex set in a product #
A point of a convex subset of a product is a relative interior point exactly when its first coordinate is a relative interior point of the projection and its second coordinate is a relative interior point of the corresponding slice.
Recession cones #
The cone over a convex set, and convex hulls of unions #
Rockafellar's K, the convex cone in ℝ × E generated by {1} × C, is written out here as the
explicit set insert 0 {p | 0 < p.1 ∧ p.2 ∈ p.1 • C}; coe_hull_prodMk_one in
Tdaf/Analysis/Convex/Recession/ConeHull.lean identifies it with PointedCone.hull ℝ ({1} × C).
The relative interior of a closed half-line of ℝ is the corresponding open half-line.
The cone {(λ, x) | λ > 0, x ∈ λC} ∪ {0} over a convex set is convex. The convex combination is
checked directly, Convex.add_smul ((s + t) • C = s • C + t • C) carrying the only interesting
case.
The relative interior of the convex cone generated by {1} × C consists of the pairs (λ, x)
with λ > 0 and x ∈ λ (ri C). This is the product criterion with the first factor ℝ: the
projection of the cone is [0, ∞), whose relative interior is (0, ∞), and the slice above
λ > 0 is λ C.
A point of C lies in ri C exactly when its lift to height one lies in the relative
interior of the cone over C.
The cone over conv (C₁ ∪ C₂) is the sum of the cones over C₁ and over C₂: the convex hull
of a union becomes a sum one dimension up.
The relative interior of the convex hull of a union of two nonempty convex sets is the union of the relative interiors of the convex combinations. The proof passes to the cones one dimension up, where the convex hull of the union becomes a sum, applies the formula for the relative interior of a sum, and reads the answer off the cone description.
The relative interior and the closure of a convex set have the same directions of recession.
This is the statement Tdaf/Analysis/Convex/Recession/Cone.lean defers, where
recessionCone_interior_eq_recessionCone_closure is proved instead.
The relative interior of an epigraph #
The relative interior of an epigraph consists of the pairs (x, μ) with x ∈ ri (dom f) and
f x < μ < ∞. This is the product criterion in which the second factor is ℝ.
Improper convex functions #
An improper convex function takes the value −∞ at every relative interior point of its
effective domain — so it is infinite except perhaps at relative boundary points of dom f.
ConvexFn.eq_bot_or_eq_top in Tdaf/Analysis/Convex/Closure.lean is the dimension-free
replacement, valid in any topological vector space; this is the finite-dimensional statement, which
needs no hypothesis on dom f and locates the ⊥ values precisely.
A lower semicontinuous improper convex function is −∞ on the whole closure of its effective
domain — the finite-dimensional sharpening of the preceding statement.
A convex function whose effective domain is relatively open is either nowhere −∞, or
everywhere infinite.
The closure of a proper convex function #
The key step: the lower semicontinuous hull agrees with f at every relative interior point of
dom f. The vertical line over x meets ri (epi f), so intersecting with an affine set lets the
closure be computed inside that line, where the epigraph section is already closed.
The lower semicontinuous hull of a proper convex function is nowhere −∞. This is what makes
clFn f the hull rather than the constant ⊥, and it is finite-dimensional.
For a proper convex function the closure is the lower semicontinuous hull; the exceptional
branch of clFn is never taken.
The closure of a proper convex function is proper (and hence, by closedFn_clFn, a closed
proper convex function).
cl f agrees with f at every relative interior point of dom f, whether or not f is
proper.
cl f also agrees with f off the closure of dom f, where both are +∞. Together with
ConvexFn.clFn_eq_of_mem_relint_dom this is the assertion that cl f differs from f at most at
relative boundary points of dom f.
dom (cl f) is squeezed between dom f and its closure, so the two domains have the same
closure and the same relative interior.
The companion statement for interiors: dom (cl f) has the same plain interior as dom f,
not only the same relative interior. The inclusion ⊇ is cl f ≤ f; for ⊆,
interior (dom (cl f)) is an open set inside ri (dom (cl f)) = ri (dom f) ⊆ dom f, and an open
subset of a set is inside its interior.
A proper convex function whose effective domain is an affine set — in particular one that is finite everywhere — is closed.
A convex function bounded below by a real constant on a convex set on which it is finite is
bounded below by that same constant on the closure of the set. The line segment principle plus one
limit: from a relative interior point y of D the whole half-open segment towards x ∈ cl D
stays in D, so the affine bound is ≥ c for every t < 1. Rockafellar carries no hypothesis at
−∞; here g is asked never to take that value, which is how the result is used and what makes
the statement true as it stands.
Limits along a segment from a relative interior point #
The lower semicontinuous hull of f at y is the limit of f along the segment running from
a relative interior point of dom f towards y. Tdaf/Analysis/Convex/Closure.lean proves
tendsto_lscHull_along_segment, where the segment must start at an interior point of epi f; here
the description of ri (epi f) supplies a relative interior point instead, and the line segment
principle replaces Mathlib's Convex.combo_interior_closure_mem_interior.
The same limit for clFn. Properness is what rules out the exceptional branch of clFn;
compare clFn_eq_limit_along_segment, which has to assume it directly.
The level sets of a convex function #
The relative interior of a closed half-line of ℝ is the corresponding open half-line.
If a convex function is anywhere below a real level, then it is already below that level at
some relative interior point of its effective domain. The open half-space {(x, μ) | μ < α}
meets epi f, hence meets ri (epi f), and the description of ri (epi f) reads off the
point.
The relative interior of a level set: ri {x | f x ≤ α} = {x ∈ ri (dom f) | f x < α}, whenever
α exceeds the infimum of f. The horizontal hyperplane {(x, α)} of the textbook argument is
replaced by the slab E × (-∞, α], whose relative interior is E × (-∞, α). Properness is not
needed.
The closure of a level set: cl {x | f x ≤ α} = {x | (cl f) x ≤ α}, stated for the lower
semicontinuous hull, which carries the content. ⊆ is closure_le_subset_lscHull_le and needs no
hypothesis; for ⊇, exists_mem_relint_dom_lt supplies a point y ∈ ri (dom f) with f y < α,
and the line segment principle runs the segment from (y, α) ∈ ri (epi f) to (x, α) ∈ cl (epi f)
inside ri (epi f).
The two level sets {f ≤ α} and {f < α} have the same closure.
The two level sets {f ≤ α} and {f < α} have the same relative interior.
The relative interior of the strict level set {f < α}.
The closure of the strict level set {f < α}, in terms of the lower semicontinuous hull.
The closure formula for a proper convex function, where the hull is the closure cl f.
For a convex function whose effective domain is relatively open, the relative interior of a
level set is the corresponding strict level set. Rockafellar assumes f closed as well; closedness
is not used.
For a closed proper convex function the closure of a strict level set is the corresponding
level set. Rockafellar assumes in addition that dom f is relatively open; that hypothesis is
needed only for the companion formula above.
Proper separation, and normals at a boundary point #
Transversal thickening #
Rockafellar's device for turning a relative-interior statement into an interior statement: add to
C a complement W' of the direction of its affine hull. The thickened set C + W' is convex, its
affine hull is everything (so it has nonempty interior), and it meets aff C in C again — so
x ∉ ri C becomes x ∉ int (C + W') and Mathlib's separation theorems for open convex sets
apply. The three lemmas below need the topology but not [FiniteDimensional ℝ E], which is why
each carries an omit; finite-dimensionality enters only in exists_lt_of_notMem_relint, through
Convex.interior_nonempty_iff_affineSpan_eq_top and closedness of an affine subspace.
Transversal thickening, trace. The thickened set meets the affine hull of C in C.
Transversal thickening, span. The thickened set is affinely spanning.
Transversal thickening, relative interior. A point of aff C outside ri C is outside the
interior of the thickening. This is the step that lets an open-set separation theorem be used.
A point outside ri C is properly separated from C by a hyperplane through it. The proof
thickens C transversally to its affine hull, so that x₀ ∉ ri C becomes x₀ ∉ int (C + W') and
Mathlib's separation of a point from an open convex set applies.
A point of a convex set is a relative boundary point exactly when some linear function that
is not constant on C attains its maximum over C there.
A convex set has a nonzero normal at each of its boundary points.
Two nonempty convex sets can be separated properly exactly when their relative interiors are
disjoint. It is proved here rather than in Tdaf/Analysis/Convex/Separation.lean because it rests
on the line segment principle and on ri C ≠ ∅ for nonempty convex C, both
finite-dimensional.