Equi-Lipschitz families and convergence of convex functions #
Four theorems about families of convex functions on a relatively open convex set. A pointwise
bounded family is uniformly bounded and equi-Lipschitzian on compact subsets; a function convex in
x and continuous in t is jointly continuous; pointwise convergence on a dense subset propagates
and becomes uniform on compact subsets; and a bounded sequence has a subsequence converging
uniformly on compact subsets.
Each theorem appears twice: an interior form, on an open convex set, which carries the whole
argument, and a _relint form, on ri C for an arbitrary convex C, obtained from it through the
linear chart of Continuity.lean. The hypotheses are the weakened pair throughout: a subset C'
with ri C ⊆ cl C' on which the family is pointwise bounded above, plus a single point of ri C
at which it is bounded below. Taking C' = ri C recovers the headline statements, and the two
convergence theorems need the weakened form, their own hypotheses being about a dense subset.
Main results #
exists_forall_abs_le_of_isCompact,exists_forall_lipschitzOnWith_of_isCompactand their_relinttwins — uniform boundedness and equi-Lipschitz continuity, withexists_forall_abs_le_and_lipschitzOnWith_of_isCompact_relintas the headline form for a pointwise bounded family. The uniform bound splits intoexists_forall_le_of_isCompactandexists_forall_ge_of_isBounded, andbddAbove_range_of_subset_convexHull_closureis the step that spreads pointwise boundedness off a dense subset.continuousOn_prod_of_convexOn,continuousOn_prod_of_convexOn_relint— joint continuity, for an arbitrary locally compactT.exists_tendstoUniformlyOn_of_dense,exists_tendstoUniformlyOn_of_dense_relint— convergence from a dense subset, withtendstoUniformlyOn_of_tendsto(_relint) for the case where the limit is already known andeventually_forall_le_add_of_eventually_le(_relint) for the eventual upper bound.uniformCauchySeqOn_of_denseis the analytic core.exists_subseq_tendstoUniformlyOn,exists_subseq_tendstoUniformlyOn_relint— a uniformly convergent subsequence.convexOn_ciSup— a finite pointwise supremum of convex functions is convex.convexOn_chart,mem_relint_of_mem_interior_chart,mem_interior_chart_of_mem_relint,chart_subset_interior_chart,interior_chart_subset_closure_chart— the chart bookkeeping.
Implementation notes #
The functions are real-valued rather than EReal-valued: these theorems are about families
finite on a relatively open convex set, and every conclusion — a supremum, a Lipschitz constant,
a uniform bound, a limit — is a statement about real numbers. So the family is f : ι → E → ℝ with
∀ i, ConvexOn ℝ C (f i), which composes directly with Mathlib; a caller holding an
EReal-valued ConvexFn converts with ConvexFn.convexOn_toReal_dom. The upper-bound hypothesis
actually needs only C ⊆ conv (cl C'), which is what
bddAbove_range_of_subset_convexHull_closure proves; the theorems are stated with cl C' because
the step from a bound to uniform convergence needs points of C' metrically near S, which a
convex hull does not supply. The subsequence theorem avoids a diagonal argument: the values on a
countable
dense subset live in a compact box in ℕ → ℝ, compact by Tychonoff and sequentially compact
because ℕ → ℝ is first countable.
References #
- R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §10.
The pointwise supremum of a family of functions convex on U is convex on U, provided the
supremum is finite at every point of U.
Pointwise boundedness spreads through a convex hull. If a family of functions convex on an
open convex set U is pointwise bounded above on a subset C' of U with U ⊆ conv (cl C'),
then it is pointwise bounded above on all of U. This is the weakest form of the upper-bound
hypothesis: the set of points where the family is bounded above is convex, so its closure
contains conv (cl C'), and a convex set contains the interior of its own closure.
Uniform boundedness from above: a family of functions convex on an open convex set U and
pointwise bounded above there is uniformly bounded above on every compact subset of U. The
pointwise supremum is a finite convex function, hence continuous, hence bounded on compact
sets.
Uniform boundedness from below: if a family of functions convex on an open convex set
U is pointwise bounded above on U and bounded below at a single point
x₀, it is uniformly bounded below on every bounded subset of U. For x ∈ U the point
z = x₀ + (δ/‖x₀ - x‖) • (x₀ - x) lies on the sphere of radius δ about x₀, and x₀ is a
convex combination of z and x, which gives a bound depending on x only through
‖x₀ - x‖.
The uniform boundedness half, in the interior form: a family of functions convex on an
open convex set U, pointwise bounded above on a subset C' whose closure
contains U and bounded below at a single point of U, is uniformly bounded on every compact
subset of U. Taking C' = U recovers the headline statement.
The equi-Lipschitz half, in the interior form: under the hypotheses of
exists_forall_abs_le_of_isCompact a single Lipschitz constant works for every member of the
family on every compact subset of U. One ε-collar and one bound M feed
ConvexOn.lipschitzOnWith_of_abs_le_of_cthickening_subset, whose constant 2M/ε does not mention
the function.
Convergence from a dense subset #
The uniform Cauchy property. A sequence of functions convex on an open convex set U
which is pointwise Cauchy on a subset C' whose closure contains U is uniformly Cauchy on
every compact subset of U. Given ε, equi-Lipschitz continuity supplies one Lipschitz constant
for the whole sequence on a compact collar of S, and finitely many points of C' then
suffice.
Convergence from a dense subset, in the interior form: a sequence of functions convex on
an open convex set U which converges pointwise on a subset C' whose closure contains U
converges pointwise
on all of U, the limit is convex, and the convergence is uniform on every compact subset of U.
Taking C' = U gives the version in which convergence is assumed everywhere.
The same with the limit function supplied: pointwise convergence on all of an open convex
U upgrades to uniform convergence on compact subsets.
An eventual upper bound, in the interior form: if a sequence of functions convex on an
open convex set U satisfies limsup_i f i x ≤ g x pointwise for a convex g, then on each
compact
S ⊆ U the bound f i ≤ g + ε holds for all large i. The limsup hypothesis is spelled as "for
every ε > 0, eventually f i x ≤ g x + ε", which avoids the junk values Filter.limsup takes on
unbounded sequences.
Arzelà–Ascoli for convex functions, in the interior form: a sequence of functions convex
on an open convex set U whose values are bounded at each point of a subset C' with U ⊆ cl C'
has a subsequence
converging, uniformly on every compact subset of U, to a finite convex function.
Joint continuity #
Joint continuity, in the interior form: a real-valued function on U × T, with U open
and convex and T locally compact, that is convex in its first argument and continuous in its
second is jointly continuous. Continuity in t is only needed at the points of a subset C' of
U whose closure contains U; taking C' = U gives the headline statement.
The chart: from interior to ri #
Every statement above is transported to the relative interior by the linear chart of
Continuity.lean: exists_chart_retraction produces a subspace V, a continuous linear
retraction r : E →L[ℝ] V, and the identity ri C = x₀ + ι (int (chart C x₀ V)). The three
lemmas here are the bookkeeping that identity buys.
Points of the interior of the chart come from points of ri C.
Points of ri C come from points of the interior of the chart.
A subset of ri C charts inside the interior of the chart.
Density transports to the chart: if C' is dense in ri C, its chart is dense in the interior
of the chart of C.
Pointwise boundedness in the ri form #
The uniform boundedness half: a family of functions convex on a convex set C, pointwise
bounded above on a subset C' of ri C whose closure contains ri C and bounded below at one
point of ri C, is uniformly bounded on every compact subset of ri C. Taking C' = ri C gives
the usual hypothesis, for a relatively open C.
The equi-Lipschitz half: under the hypotheses of
exists_forall_abs_le_of_isCompact_relint a single Lipschitz constant serves the whole family on
any compact subset of ri C.
Convergence, in the ri form #
Convergence from a dense subset: a sequence of functions convex on a convex set C
which
converges pointwise on a subset C' of ri C whose closure contains ri C converges pointwise on
all of ri C, to a finite convex limit, uniformly on every compact subset of ri C.
The same with the limit supplied: pointwise convergence on ri C upgrades to uniform
convergence on its compact subsets.
An eventual upper bound: if limsup_i f i x ≤ g x for every x ∈ ri C, with g
convex, then on each compact S ⊆ ri C the bound f i ≤ g + ε holds uniformly for large i.
The limsup hypothesis is spelled as "for every δ > 0, eventually f i x ≤ g x + δ".
Arzelà–Ascoli for convex functions: a sequence of functions convex on C whose values are
bounded
at each point of a subset C' of ri C with ri C ⊆ cl C' has a subsequence converging uniformly
on the compact subsets of ri C to a finite convex function.
Joint continuity, in the ri form #
Joint continuity: a real-valued function on ri C × T, with T locally compact,
convex in its first argument and continuous in its second, is jointly continuous relative to
ri C × T.
The headline form #
A family of convex functions finite and pointwise bounded on ri C is uniformly bounded
and equi-Lipschitzian on every compact subset of ri C.