Continuity of a convex function on the relative interior of its domain #
A proper convex function on a finite-dimensional space is continuous, relative to the affine hull
of its effective domain, at every relative interior point of that domain. Mathlib proves the
interior statement (ConvexOn.continuousOn_interior) and leaves the relative version open,
because intrinsicInterior lives in a file that does not meet
Mathlib/Analysis/Convex/Continuous.lean. This file supplies it, and with it the quantitative
refinements: Lipschitz continuity on compact subsets of ri (dom f), and uniform continuity on the
whole space.
Main results #
relint_eq_vadd_image_interior— the chart:ri C = x₀ + ι (int D), whereDis the trace ofCon a subspaceVspanned byC - x₀. This is the reduction "relative interior = interior in the affine hull", carried out in a linear chart rather than in the affine hull itself, so thatConvexandConvexOn— which need a module, not a torsor — still apply.exists_chart_retraction— the chart packaged with a continuous linear retraction, which is what carries continuity and Lipschitz constants back from the chart toE.ConvexFn.continuousOn_toReal_relint_dom,ConvexFn.continuousOn_relint_dom— continuity onri (dom f), in the real-valued and theEReal-valued form;ConvexFn.continuous_of_dom_eq_univis the everywhere-finite case.ConvexOn.lipschitzOnWith_of_abs_le_of_cthickening_subset,ConvexOn.exists_lipschitzOnWith_of_isCompact,ConvexFn.exists_lipschitzOnWith_of_isCompact— Lipschitz continuity on compact subsets: the quantitative form with the constant2M/εexhibited (which is what equi-Lipschitz statements need, and which needs no finite-dimensionality), then theinteriorand theriform.ConvexFn.uniformContinuous_toReal_iff— uniform continuity on the whole space, withConvexFn.exists_lipschitzWith_of_recessionFn_ne_topas its quantitative half andConvexFn.exists_lipschitzWith_of_frequently_le,ConvexFn.exists_lipschitzWith_of_le_lipschitzas two easily checked sufficient conditions.intrinsicInterior_vadd— translation invariance ofri, which the chart needs and which Mathlib does not state.
Implementation notes #
The chart is a linear subspace, not the affine hull. intrinsicInterior ℝ C is defined as the
interior taken inside ↥(affineSpan ℝ C), but that subtype is an AddTorsor, while Convex,
ConvexOn and every Mathlib continuity theorem need a module; fixing x₀ ∈ C and moving to a
subspace V spanned by C - x₀ costs one translation and buys the whole module API. The subspace
is a parameter rather than a definition — every lemma takes V with hV : V = span ℝ (C - x₀) —
so that instance synthesis for ↥V never has to unfold a Submodule.span; callers obtain an
opaque V from ⟨_, rfl⟩. Transporting continuity back to E uses a continuous left inverse
rather than the embedding, which finite-dimensionality supplies through
LinearMap.linearProjOfIsCompl.
References #
- R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §10.
The relative interior is translation invariant.
The chart of C at x₀ in a subspace V: the directions z ∈ V with x₀ + z ∈ C.
Instances For
The chart maps onto the translate C - x₀.
The chart affinely spans the chart space: that is what makes ri collapse to interior
there.
The relative interior, computed in the chart. ri C is the translate by x₀ of the image
of the ordinary interior of chart C x₀ V.
The chart, packaged for reuse. For a convex C and a point x₀ ∈ C there is a subspace V
and a continuous linear retraction r : E →L[ℝ] V such that x ↦ r (x - x₀) carries ri C into
interior (chart C x₀ V) and x₀ + r (x - x₀) = x there, together with the chart identity
relint_eq_vadd_image_interior for that V. Continuity transports along r because r is
continuous, and Lipschitz constants because r is bounded.
The real-valued restriction of f is convex on dom f, in Mathlib's sense.
A proper convex function is continuous, relative to the affine hull of its domain, at every relative interior point — real-valued form.
A proper convex function on a finite-dimensional space is continuous on ri (dom f),
relative to the affine hull of its effective domain.
Functions finite everywhere #
A convex function that is finite everywhere is continuous. dom f = univ is "finite on
all of Rⁿ", properness supplying the other half.
A convex function finite everywhere is continuous, real-valued form.
Lipschitz continuity on compact subsets of the relative interior #
The quantitative core. If ψ is convex on D and bounded by M in absolute value on the
closed ε-collar of S, and that collar lies inside D, then ψ is Lipschitz on S with
constant 2M/ε. For x ≠ y in S the point
z = y + (ε / ‖y - x‖) • (y - x) sits in the collar and expresses y as a convex combination of
x and z, so convexity bounds the increment by the oscillation of ψ over the collar.
The constant is exhibited rather than existentially quantified: a family of convex functions
sharing one collar and one bound is therefore equi-Lipschitzian with a single constant. Mathlib's
ConvexOn.lipschitzOnWith_of_abs_le is the two-sided ball version, and
the collar argument does not follow from it.
The interior form: a function convex on D is Lipschitz on every compact subset of
interior D. Compactness supplies an ε-collar of S still inside
interior D, on which continuity bounds ψ.
A proper convex function is Lipschitz on every compact subset of ri (dom f). The usual
statement is for closed bounded subsets, which in finite dimensions is the same thing. The
retraction of the chart is a continuous linear map, hence Lipschitz,
so it carries Lipschitz constants back as well as continuity.
Uniform continuity and Lipschitz continuity on the whole space #
A finite convex function on the whole space is closed: it is continuous, hence lower semicontinuous, hence has a closed epigraph.
When f0⁺ is finite everywhere it is bounded by a linear function of the norm. The
constant is α = sup {(f0⁺) z | ‖z‖ = 1}, finite because f0⁺ is a finite convex function, hence
continuous, and the unit ball is compact; positive homogeneity spreads the bound over the whole
space.
Sufficiency: if the recession function of a finite convex function on the whole space is
finite everywhere, the function is Lipschitz, with α as constant.
Necessity: a uniformly continuous finite convex function has a finite recession function.
Uniform continuity at ε = 1 bounds f (x + z) - f x by 1 uniformly in x for short z, which
says (f0⁺) z ≤ 1.
A finite convex function on the whole space is uniformly continuous exactly when its
recession function is finite everywhere, and then it is in fact Lipschitz
(ConvexFn.exists_lipschitzWith_of_recessionFn_ne_top).
For Lipschitz continuity it is enough that f (a • y) / a stay bounded above along some
sequence a → ∞, in every direction y. The quotient is nondecreasing in a, so a bound reached
infinitely often is a bound everywhere.
A finite convex function dominated by a Lipschitz function is itself Lipschitz. The usual
statement assumes the dominating g convex; the proof does not use it, so g here is an arbitrary
Lipschitz function.