Co-finite bifunctions #
A convex bifunction is co-finite when every slice Fu is a co-finite convex function: closed,
proper, convex, with an epigraph containing no non-vertical half-line. This is the condition under
which the algebra of bifunctions loses its side conditions — a co-finite bifunction has all of U
as its effective domain and an everywhere-finite inner product ⟨Fu, y⟩, so the relative-interior
hypotheses become vacuous. The identity ⟨GFu, z⟩ = ⟨u, F* G* z⟩ lives here too, for the same
reason: it needs a relative interior, hence a topology and a finite dimension.
Main definitions #
CofiniteBifun F— a convex bifunction all of whose slices are co-finite convex functions.
Main results #
CofiniteBifun.domBifun_eq_univ,CofiniteBifun.proper— a co-finite bifunction has full effective domain and is proper.CofiniteBifun.bracket_lt_top,cofiniteBifun_of_forall_bracket_lt_top— a closed convex bifunction is co-finite exactly when⟨Fu, y⟩is finite for everyuandy(Corollary 13.3.1 in [^1], slice by slice).cofinite_infConv,cofiniteBifun_infConvBifun,adjointBifun_infConvBifun_of_cofinite— Rockafellar's closing remark:F₁ □ F₂is co-finite and(F₁ □ F₂)* = F₁* □ F₂*, with no hypothesis beyond co-finiteness.cofinite_smulRightandcofiniteBifun_smulRightBifunare the same forF ↦ Fλ,λ > 0.cofiniteBifun_iff_domBifun_eq_univ— a closed proper convex bifunction is co-finite iffdom F = Uanddom F* = Y. Rockafellar deduces this from the saddle-function correspondence; the proof here is the finiteness criterion for conjugates, slice by slice.CofiniteBifun.bracket_eq_concaveBracket_adjointBifun—⟨Fu, y⟩ = ⟨u, F* y⟩for everyu; andbracket_compBifun_eq_concaveBracket_concaveCompBifunis the corresponding⟨GFu, z⟩ = ⟨u, F* G* z⟩for a product of bifunctions.
Implementation notes #
Rockafellar defines co-finiteness for convex bifunctions only, and the convexity is genuinely extra
data — the graph function of a bifunction all of whose slices are convex need not be convex on
U × X — so CofiniteBifun carries ConvexBifun as a field.
Elsewhere the relative-interior conditions are carried as IsExactSum hypotheses; here they are
discharged, because the functions being added are finite on the whole space and
IsExactSum.of_relint applies at the origin. That is why this module is finite-dimensional.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §38 and §13.
Co-finite bifunctions #
A co-finite convex bifunction: every slice is a co-finite convex function. This forces
dom F = U and makes F proper.
- convexBifun : ConvexBifun F
The bifunction is convex.
- cofinite_apply (u : U) : Cofinite (F u)
Every slice is a co-finite convex function.
Instances For
Co-finiteness forces a full effective domain: every slice is proper.
Finiteness of the inner product #
With CofiniteBifun.bracket_lt_top: ⟨Fu, y⟩ is finite, every slice being proper.
For a co-finite bifunction the inner product ⟨Fu, y⟩ is never +∞. This is the
finiteness criterion for the conjugate of a co-finite function, read at the slice Fu.
The converse: closed proper convex slices and a finite ⟨Fu, y⟩ give co-finiteness.
Infimal convolution of co-finite functions #
The conjugate of a co-finite function is finite everywhere.
The conjugates of two co-finite functions add exactly: their effective domains are the whole space, so the relative-interior condition for an exact sum holds at the origin.
The infimal convolution of two co-finite functions is a conjugate, namely the conjugate of
f* + g*. This is what makes it closed.
The infimal convolution of two co-finite convex functions is co-finite: f □ g is the
conjugate of f* + g*, hence closed proper convex, and its own conjugate is f* + g*, which is
finite everywhere.
Infimal convolution of co-finite bifunctions #
Slice by slice this is cofinite_infConv; convexity of F₁ □ F₂ is
convexBifun_infConvBifun.
The two brackets add exactly, both being finite everywhere. This is what makes
adjointBifun_infConvBifun unconditional for co-finite bifunctions.
(F₁ □ F₂)* = F₁* □ F₂* for co-finite bifunctions, with the exactness hypothesis
discharged.
For a co-finite bifunction the two inner products agree at every u,
⟨Fu, y⟩ = ⟨u, F* y⟩. They agree on ri (dom F), and dom F is all of U.
Right scalar multiplication of co-finite functions #
fa is the conjugate of a f*, for a > 0 and closed convex f: the conjugation rule
conj_smul at g = f*, with Fenchel–Moreau turning f** back into f. It supplies closedness of
fa, which the epigraph-image definition of smulRight does not see.
fa is closed when f is closed convex and a > 0. It is a conjugate
(smulRight_eq_conj_smul).
fa is proper when f is and a > 0.
Right scalar multiplication preserves co-finiteness, for a > 0.
Right scalar multiplication, and the co-finiteness criterion #
F ↦ Fλ preserves co-finiteness for λ > 0. Slice by slice this is cofinite_smulRight;
the convexity of Fλ is convexBifun_smulRightBifun.
dom F* = Y, the half of the co-finiteness criterion needing no closedness: ⟨F·, y⟩ is a
finite concave function on U, so its negative is proper convex and its conjugate is proper; the
sign dictionary carries that back to F* y.
The substantial direction: dom F = U makes every bracket ⟨Fu, y⟩ finite below, and
dom F* = Y makes it finite above — if ⟨Fu₀, y⟩ = +∞ for a single u₀ then F* y ≡ -∞. The
finiteness criterion for conjugates, slice by slice, does the rest.
A closed proper convex bifunction is co-finite iff dom F = U and dom F* = Y. The proof
here is the finiteness criterion for conjugates, slice by slice.
The inner product of a product of bifunctions #
⟨GFu, z⟩ = ⟨u, F* G* z⟩. The two brackets of GF agree at a relative interior point of
dom (GF), and adjointBifun_compBifun rewrites (GF)* as F* G*. The companion equality
⟨GFu, z⟩ = ⟨Fu, G* z⟩ is bracket_compBifun_eq_fenchelPairing.