Continuity of finite saddle-functions #
A finite concave-convex function on C × D is Lipschitz on every product of compact subsets of
ri C and ri D, hence continuous there; a pointwise bounded family of such functions is
uniformly bounded and equi-Lipschitz on such a rectangle; and the usual convergence and
Arzelà–Ascoli consequences follow. Each is a statement about convex functions of one variable,
applied once in each variable and combined.
Main definitions #
ConcaveConvexOn C D K—K : U × X → ℝis concave in its first argument onCfor each point ofDand convex in its second onDfor each point ofC. Its two fields are exactly the hypotheses the simple extensions ofSaddle/Kernel.leantake.
Main results #
exists_forall_abs_le_and_lipschitzOnWith_prod— a pointwise bounded family, indexed by an arbitrary type, is uniformly bounded and equi-Lipschitz (Theorem 35.2 in [^1]); the engine here.ConcaveConvexOn.exists_lipschitzOnWith_of_isCompact,.exists_forall_abs_le_of_isCompact,.continuousOn— the same for a single function, and continuity onri C × ri D.continuousOn_prod_of_concaveConvexOn,continuousOn_prod_of_concaveConvexOn'— joint continuity in a parameter.exists_tendstoUniformlyOn_prod_of_dense,tendstoUniformlyOn_prod_of_tendsto— pointwise convergence on a dense set becomes uniform on compact rectangles, andexists_subseq_tendstoUniformlyOn_prodis the Arzelà–Ascoli form.exists_isCompact_mem_nhdsWithin_relint,exists_isCompact_collar_relint—ri Cis locally compact, and a compact subset of it has a compact relative collar.uniformCauchySeqOn_of_equiLipschitz— the metric core of the convergence theorems, with the convexity stripped out.
Implementation notes #
Everything is stated for arbitrary convex C and D, with ri C and ri D written out; the
customary form takes them relatively open, where ri C = C. The Lipschitz constant is α₁ + α₂
rather than 2(α₁ + α₂), because Mathlib's product metric is the supremum metric and no factor is
paid passing between the coordinate distances and the distance on the product.
The convergence theorems take an arbitrary dense A ⊆ ri C ×ˢ ri D rather than a product
C' ×ˢ D'. The equi-Lipschitz input does need a product, but the diagonal extraction behind the
Arzelà–Ascoli statement produces a countable dense set that is not a product.
Unlike the one-variable theory, these results cannot be transported from the interior case along
a chart: the chart of C ×ˢ D is not the product of the charts of C and D, and it is the
product structure that the concave-convex hypothesis lives on. They are proved directly in ri.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §35.
Concave-convex functions on a rectangle #
K is concave-convex on C × D: concave in its first argument on C for each point of
D, convex in its second on D for each point of C. The finite, set-relative form of
ConcaveConvexFn, and the hypothesis the continuity theory runs on.
K (·, x)is concave onCfor everyx ∈ D.K (u, ·)is convex onDfor everyu ∈ C.
Instances For
The concave slice, as a family of convex functions: the form the convex lemmas consume.
Negation #
The one-variable results are stated for convex functions; the concave variable reaches them
through -K, and these lemmas carry the conclusions back.
Negating a real-valued function does not change its Lipschitz constants.
-f is Lipschitz on S exactly when f is.
Uniform bounds and equi-Lipschitz constants for a family #
The engine of the file: one-variable pointwise boundedness applied four times — twice to bound the family, once in each variable, and twice to make it equi-Lipschitz.
The convex slices of a concave-convex family, at a point of C, as a family of convex
functions on D.
The first bounding step: for a fixed u ∈ C' the convex slices K i (u, ·) are uniformly
bounded on every compact T ⊆ ri D: the one-variable statement, in the second variable.
The second bounding step: for a fixed x ∈ D' the concave slices K i (·, x) are uniformly
bounded on every compact S ⊆ ri C: the one-variable statement in the first variable, reached
through -K.
The two equi-Lipschitz halves #
In the first variable: the family is uniformly bounded on S ×ˢ T and equi-Lipschitz in
u, uniformly in x ∈ T.
In the second variable: the family is equi-Lipschitz in x, uniformly in u ∈ S.
A family of finite concave-convex functions on C × D, pointwise bounded on C' × D', is
uniformly bounded and equi-Lipschitzian on S ×ˢ T for every compact S ⊆ ri C and T ⊆ ri D.
The customary hypothesis is conv (cl (C' × D')) ⊇ C × D for relatively open C, D; the form
used here is C' ⊆ ri C ⊆ cl C' and likewise for D, and C' = ri C, D' = ri D gives the
headline statement.
The single-function case #
A finite concave-convex function on C × D is Lipschitzian on every product of compact
subsets of ri C and ri D: the family statement at a one-element family.
A finite concave-convex function is bounded on every product of compact subsets of the relative interiors.
Compact relative neighbourhoods #
ri C is locally compact — being a translate of an open subset of a finite-dimensional subspace —
which is what turns "Lipschitz on every compact rectangle" into "continuous".
Every point of ri C has a compact relative neighbourhood inside ri C.
The continuity clause #
A finite concave-convex function on C × D is continuous relative to ri C × ri D.
Continuity is local, ri C and ri D are locally compact, and on a compact rectangle the function
is Lipschitz.
The relative collar #
The convergence and joint-continuity theorems need, for a compact S ⊆ ri C, a slightly larger
compact subset of ri C containing every point of ri C near S.
IsCompact.exists_cthickening_subset_open will not serve: cthickening ε S ⊆ ri C is false,
because points off the affine hull of C are near S.
A compact subset of ri C has a relative collar: an ε > 0 and a compact S' ⊆ ri C
containing S and every point of ri C within ε of S. The relative analogue of
IsCompact.exists_cthickening_subset_open, and what makes the interior proofs of the
one-variable convergence theorems run in ri.
Equi-Lipschitz plus a dense Cauchy set #
The metric core of the convergence theorems, with the convexity stripped out: on a compact S
carrying a collar S' on which the sequence is equi-Lipschitz, pointwise Cauchy behaviour on a
dense subset of S is already uniform Cauchy behaviour on S.
Equi-Lipschitz on a collar plus pointwise Cauchy on a dense subset gives uniform Cauchy.
hcollar is the only thing the ambient structure has to supply: every point of A within ε of
S must lie in S', the set on which the family is equi-Lipschitz. In the interior setting
S' = cthickening ε S; in the relative setting it is exists_isCompact_collar_relint.
Convergence #
Both are the one-variable statements with the compact set replaced by a compact rectangle: the
family theorem supplies the equi-Lipschitz constant, exists_isCompact_collar_relint the room to
move in, and uniformCauchySeqOn_of_equiLipschitz does the rest.
The uniform Cauchy property behind both convergence theorems: a sequence of finite
concave-convex functions, pointwise bounded on C' × D' and pointwise Cauchy on a set A dense in
ri C × ri D, is uniformly Cauchy on every compact rectangle inside ri C × ri D.
A sequence of finite concave-convex functions on C × D, whose values are bounded at every
point of a product C' × D' dense in ri C × ri D and convergent at every point of a dense
A ⊆ ri C × ri D, converges at every point of ri C × ri D to a finite concave-convex limit,
uniformly on every compact rectangle. Taking A = C' ×ˢ D' gives the customary statement.
The same in its customary form: pointwise convergence on a product of dense subsets.
With the limit supplied: pointwise convergence on all of ri C × ri D upgrades to uniform
convergence on compact rectangles.
Arzelà–Ascoli for saddle-functions: a sequence of finite concave-convex functions on
C × D whose values are bounded at every point of a product C' × D' dense in ri C × ri D has a
subsequence converging, uniformly on every compact rectangle inside ri C × ri D, to a finite
concave-convex function.
As in one variable the subsequence comes from a countable dense subset of the product C' ×ˢ D',
which is why exists_tendstoUniformlyOn_prod_of_dense is stated for a general dense A.
Joint continuity in a parameter #
A real-valued function of (u, x, t) with T locally compact, concave-convex in (u, x)
for each t and continuous in t for each (u, x), is jointly continuous relative to
ri C × ri D × T.
Continuity in t is only needed at the points of dense subsets C' and D';
continuousOn_prod_of_concaveConvexOn' is the headline statement. On a compact neighbourhood T₀
of t₀ the family {F(·, t) | t ∈ T₀} is pointwise bounded on C' × D', so the family theorem
equi-Lipschitz near (u₀, x₀), and a four-term estimate through a nearby point closes it.
The same with continuity in the parameter assumed at every point of ri C × ri D.