The complete lattice of convex functions #
The convex functions on E, pointwise ordered, form a complete lattice. The least upper bound of a
family is the pointwise supremum, since a pointwise supremum of convex functions is convex. The
greatest lower bound is not the pointwise infimum, which need not be convex; it is the convex hull
conv {f i}, the greatest convex minorant of the family. ConvexFns.exists_coe_inf_lt_inf makes
the difference concrete on ℝ: the indicators of {0} and {1} have pointwise minimum ⊤ at
1/2, while their meet, the indicator of [0, 1], is 0 there. So the coercion to E → EReal is
an sSupHom but cannot be an sInfHom.
Main definitions #
ConvexFns E— the convex functions onEas a type, withConvexFns.instCompleteLattice.ConvexFns.coeOrderEmbedding,ConvexFns.coeSSupHom— the coercion toE → ERealas an order embedding and as ansSupHom.
Main results #
ConvexFns.coe_sSup,ConvexFns.coe_sup— the join is the pointwise supremum.ConvexFns.coe_iInf,ConvexFns.coe_inf— the meet isconvFn, resp.convFn₂.ConvexFns.coe_top,ConvexFns.coe_bot— the extreme elements are the constants⊤and⊥.ConvexFns.not_coe_inf_eq_inf— the meet is genuinely not the pointwise infimum.
Implementation notes #
ConvexFns E is a reducible abbreviation for the subtype gci_val_convHullFn is stated about, so
that coreflection lifts to a CompleteLattice directly and the order is definitionally the
pointwise one.
References #
- R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §5.
The type of convex functions #
The convex functions on E, bundled as a type carrying the pointwise order.
Equations
- Tdaf.ConvexAnalysis.ConvexFns E = { f : E → EReal // Tdaf.ConvexAnalysis.ConvexFn f }
Instances For
The convex functions on E, pointwise ordered, form a complete lattice. The instance is
the coreflection gci_val_convHullFn transported by
GaloisCoinsertion.liftCompleteLattice, so every field is the corresponding operation on
E → EReal followed by convHullFn; the lemmas below evaluate that hull.
The coercion ConvexFns E → (E → EReal) is an order embedding: f ≤ g in the lattice of
convex functions means exactly f x ≤ g x for every x.
Equations
Instances For
A convex function is a member of the lattice, and only convex functions are.
Suprema: the join is pointwise #
The least upper bound is the pointwise supremum (Rockafellar's "sup {f i}").
The binary case: the join of two convex functions is their pointwise maximum.
The coercion to E → EReal as an sSupHom: it preserves arbitrary suprema. There is no
companion sInfHom — see ConvexFns.not_coe_inf_eq_inf.
Equations
- Tdaf.ConvexAnalysis.ConvexFns.coeSSupHom = { toFun := Subtype.val, map_sSup' := ⋯ }
Instances For
Infima: the meet is a convex hull #
The greatest lower bound is a convex hull, conv of the pointwise infimum.
Rockafellar's conv {f i | i ∈ I}. The greatest lower bound of a family of convex functions
is their convex hull convFn, not their pointwise infimum, which is generally not convex.
The binary case: the meet of two convex functions is their binary convex hull convFn₂.
The meet lies below the pointwise infimum, and generally strictly:
ConvexFns.exists_coe_inf_lt_inf.
The extreme elements #
The greatest convex function is the constant ⊤.
The least convex function is the constant ⊥.
The meet is not the pointwise infimum #
The coercion ConvexFns E → (E → EReal) is not an sInfHom, not even a lattice
homomorphism: it does not commute with binary meets. Contrast ConvexFns.coeSSupHom.