The convex hull of a family of functions #
The pointwise infimum of convex functions is generally not convex; the convex hull is what replaces
it. The convex hull of a family f : ι → E → EReal is the function determined by the convex hull of
the union of the epigraphs, and it is the greatest convex function below every f i.
Main definitions #
convFn f— the convex hull of a family: the infimum in the lattice of convex functions.convHullFn g— the convex hullconv gof a single function: the coreflector onto that lattice. The two determine each other (convFn_eq_convHullFn_iInf,convFn_unit) but play different roles — onlyconvHullFnis an adjoint, onlyconvFntakes a family.convFn₂ f g— the binary case, the meet of two convex functions.
Main results #
convFn_le,le_convFn,isGreatest_convFn— the universal property: greatest convex minorant, from which everything else in the file follows.convexFn_convFn— the convex hull is convex.convFn_le_iInf— the convex hull is below the pointwise infimum, generally strictly;convFn₂_indicatorFn_lt_infis a witness.gci_val_convHullFn—convis right adjoint to the inclusion of the convex functions, as aGaloisCoinsertion. This is what makes the convex functions a complete lattice with⨅ = convFnand⨆ = sSup.convFn_apply— the explicit formula(conv {f i}) x = inf {∑ λ i * f i (x i) | ∑ λ i • x i = x}(Theorem 5.6 in [^1]);convFn₂_applyis the two-function form later sections use.IsEpiLike.mem_convexHull_of_le,isEpiLike_convexHull_epi_union,epi_convFn₂— when that infimum is attained.epi (conv {f, g})isconv (epi f ∪ epi g)exactly when that hull is an epigraph, and the only way it can fail to be one is by failing to be closed.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §5.
The convex hull of a family #
The convex hull of a family of functions: the function determined by the convex hull of the
union of the epigraphs. Equivalently (isGreatest_convFn), the greatest convex h, proper or not,
with h ≤ f i for every i.
Equations
- Tdaf.ConvexAnalysis.convFn f = Tdaf.ConvexAnalysis.ofEpi ((convexHull ℝ) (⋃ (i : ι), Tdaf.ConvexAnalysis.epi (f i)))
Instances For
The convex hull of a family is a convex function, a convex hull of sets being convex.
The universal property. Any convex function below every f i is below the convex hull;
with convFn_le and convexFn_convFn, the convex hull is the greatest convex minorant.
The epigraph of the convex hull is the convex hull of the union of epigraphs, under the
hypothesis that the latter is an epigraph at all. It need not be: even for two functions the
infimum in the formula for convFn need not be attained.
The convex hull is below the pointwise infimum, strictly in general
(convFn₂_indicatorFn_lt_inf), which is the entire reason the convex hull exists.
The convex hull of a single function #
The convex hull of a function, conv g: the greatest convex function majorised by g.
Equations
Instances For
The universal property of conv g.
Convexity is exactly closedness under conv.
The coreflection onto the convex functions #
conv is right adjoint to the inclusion of the convex functions. For convex h and
arbitrary g, h ≤ g and h ≤ conv g say the same thing.
A coinsertion, because conv fixes the convex functions. The convex functions therefore
inherit a complete lattice structure in which the infimum is convFn.
Equations
Instances For
The two hulls determine each other #
Rockafellar: the convex hull of a collection "is the convex hull of the pointwise infimum of
the collection". Both sides are the greatest convex function below every f i.
convHullFn is the one-element instance of convFn.
The binary case #
The convex hull of two functions: the greatest convex function below both, i.e. the meet in the lattice of convex functions.
Equations
Instances For
The binary convex hull is below the pointwise minimum, generally strictly.
The inequality convFn₂_le_inf is strict in general. The indicator functions of {0} and
{1} in ℝ are both convex; their pointwise minimum is ⊤ at 1 / 2, while their convex hull —
the indicator function of the segment [0, 1] — is 0 there.
The explicit formula for two functions #
Every convex combination a • u + b • v = x bounds the convex hull at x: the easy half of the
formula. Only f, g ≠ ⊥ is needed, not full properness — with ⊥ allowed the right-hand side
can be ⊥ (since ⊥ + ⊤ = ⊥ in EReal) while the left-hand side is ⊤.
The convex hull of two proper convex functions is given by the explicit formula
(conv {f, g}) x = inf {a f u + b g v | a u + b v = x, a, b ≥ 0, a + b = 1},
the infimum over all representations, and genuinely an infimum — it need not be attained.
convFn_apply proves the same theorem for an arbitrary family and needs only the ≠ ⊥ half of
properness. Here dom f, dom g ≠ ∅ is used as well, to make the epigraphs non-empty and so turn
the convex hull of their union into a convex join.
conv (f ⊓ g) = conv {f, g}: both sides are the greatest convex function below f and g.
When a convex hull of epigraphs is again an epigraph #
epi (convFn₂ f g) is conv (epi f ∪ epi g) only when that hull is epi-like, which is exactly the
statement that the infimum in the formula is attained. Of the two halves of isEpiLike_iff_forall
the upward-closure half holds unconditionally; only attainment is at issue.
The convex hull of an epi-like set is upward closed in the vertical coordinate: conv F
inherits every translation p ↦ p + (0, t), t ≥ 0, that F itself admits.
The binary case of epi_convFn.
The explicit formula in general #
The convex hull of a family of convex functions, none of which takes the value ⊥, is given by
the explicit formula
(conv {f i}) x = inf {∑ λ i * f i (x i) | ∑ λ i • x i = x},
the infimum being over all representations of x as a convex combination of points x i, with
only finitely many non-zero coefficients.
The classical statement assumes the f i proper; only the ≠ ⊥ half is used, twice — it keeps
λ i * f i (x i) from being −∞ where λ i = 0, and it turns a finite bound on the sum into a
finite bound on each term. dom (f i) ≠ ∅ does no work, exactly as for sums.
The description of a convex hull by convex combinations presents a point of the hull as drawn from
the epi (f i) with repetitions, whereas the infimum here ranges over one point per index. The
proof of ≥ bridges the two by merging the points drawn from a single epi (f i) into their
center of mass, which is the only use made of convexity of the f i.
Closedness supplies the missing half #
A closed convex hull of two epigraphs is an epigraph: IsEpiLike.mem_convexHull_of_le
gives upward closure unconditionally and closedness gives attainment of the vertical infima. So the
only way conv (epi f ∪ epi g) can fail to be an epigraph is by failing to be closed, which turns
the closedness criteria for convex hulls into attainment statements for that infimum.