Rockafellar, §38: The Algebra of Bifunctions #
Addition, scalar multiplication, application and composition of convex bifunctions, and how each behaves under taking adjoints. All twelve numbered results of §38 are formalized: Theorems 38.1–38.5 and 38.7, Lemma 38.6, and Corollaries 38.2.1, 38.4.1, 38.5.1, 38.7.1 and 38.7.2.
Implementation notes #
Theorem 38.1's inner-product identity holds "if one sets ∞ − ∞ = −∞ + ∞ = −∞", and its
parenthetical adds "similarly for concave bifunctions, but with ∞ − ∞ = −∞ + ∞ = +∞". Those are
two different binary operations on EReal, named apart here as convexAdd — which is EReal's
own addition — and concaveAdd, which is not: theorem_38_1_bracket_concave is false with
convexAdd in its place.
Rockafellar's inner product ⟨f, g⟩ of a convex and a concave function is a partial operation;
he states the definedness condition in prose and then writes ⟨f, g⟩ freely. Here
HasInnerProduct is that condition, and it is an explicit hypothesis wherever an inner product is
claimed to exist.
Divergences from the book #
Every relative-interior hypothesis of §38 is carried as an IsExactSum. Rockafellar's conditions
are always "ri (dom …) and ri (dom …) have a point in common", the hypothesis of Theorem 16.4;
IsExactSum is that theorem's conclusion. Two consequences show in the statements: exactness is
demanded once per dual vector, where the book's single condition is uniform in it, and
IsExactSum carries properness of both summands, which is the book's main branch.
□ is unconditionally commutative and associative here, where the book hedges "to the extent that
it is defined" — infConv is total on EReal, so improper bifunctions are included. That is
stronger than the book. The caveat that is real is the one about bifunction multiplication,
and it is not discharged.
References #
- R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §38, pp. 401–412.
The two ∞ − ∞ conventions of Theorem 38.1 #
Rockafellar's convex ∞ − ∞ convention, ∞ − ∞ = −∞ + ∞ = −∞, under which Theorem 38.1's
inner-product identity holds for convex bifunctions. On EReal this is the ambient addition; the
definition exists only to give the convention a name distinct from the concave one.
Equations
- Rockafellar.convexAdd a b = a + b
Instances For
The concave convention resolves ∞ − ∞ upwards.
The two conventions are genuinely different operations, which is why they are named apart
where the book's ⟨·, ·⟩ carries both.
The inner product ⟨f, g⟩ of a convex and a concave function #
Rockafellar's inner product ⟨f, g⟩ exists: the two extrema sup_x {g*(x) − f(x)} and
inf_y {f*(y) − g(y)} agree. He leaves ⟨f, g⟩ undefined when they do not, so this predicate is
the definedness side condition and appears in every statement below that mentions one.
Equations
Instances For
The value of ⟨f, g⟩, represented by the inf side. It is Rockafellar's inner product only
under HasInnerProduct.
Equations
Instances For
The definedness condition in the book's own two extrema.
Weak duality: the sup side never exceeds the inf side, with no hypothesis. This is what makes every existence claim below a single inequality.
Theorem 38.1 #
Theorem 38.1, first assertion: the infimal convolution (F₁ □ F₂)u = F₁u □ F₂u of two
proper convex bifunctions from ℝᵐ to ℝⁿ is a convex bifunction.
Theorem 38.1, second assertion: dom (F₁ □ F₂) = dom F₁ ∩ dom F₂. The book prints the
left-hand side as dom (F₁ ∩ F₂); the operation meant is □, as its own proof shows. No
hypothesis is needed.
Theorem 38.1, the inner-product identity ⟨(F₁ □ F₂)u, x*⟩ = ⟨F₁u, x*⟩ + ⟨F₂u, x*⟩, under
the convex convention ∞ − ∞ = −∞. It needs no hypothesis: it is Theorem 16.4's unconditional
row conj_infConv read slice by slice.
Theorem 38.1, concave orientation: for concave bifunctions □ is supremal convolution
and the identity holds under the concave convention ∞ − ∞ = +∞, with ⟨Gu, x*⟩ the concave
conjugate of the slice. The statement is false with convexAdd in place of concaveAdd. Like
its convex twin it is unconditional.
The algebra of □ #
□ is commutative "in the class of convex bifunctions from ℝᵐ to ℝⁿ to the extent that it
is defined". The hedge is unnecessary here: infConv is total on EReal, so this holds for
arbitrary bifunctions, improper ones included — strictly stronger than the book.
□ is associative, again with no hypothesis.
Theorem 38.2 #
Theorem 38.2: (F₁ □ F₂)* = F₁* □ F₂*, the bifunction generalisation of
(A₁ + A₂)* = A₁* + A₂*; the □ on the right is supremal convolution. Where the book asks that
ri (dom F₁) and ri (dom F₂) meet, the hypothesis here is IsExactSum for the two concave
functions u ↦ ⟨Fᵢu, x*⟩, one instance per x*.
Corollary 38.2.1 #
The IsExactSum Corollary 38.2.1 consumes. The book's condition is that ri (dom F₁*) and
ri (dom F₂*) have a point in common.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Corollary 38.2.1, first assertion: for closed proper convex F₁ and F₂, F₁ □ F₂ is
closed. The hypothesis is IsExactSumCor3821, where the book asks that ri (dom F₁*) and
ri (dom F₂*) meet. The proof is not Rockafellar's: F₁ □ F₂ is exhibited as a lower adjoint,
and those are closed unconditionally.
Corollary 38.2.1, last assertion: (F₁ □ F₂)* = cl (F₁* □ F₂*). Stated in the F⁎*
packaging, where the right-hand □ is convolution in the first variable — what the book's
concave F₁* □ F₂* becomes once the negations move outside, keeping everything convex.
Theorem 38.3 #
Theorem 38.3, first assertion: for λ > 0 the scalar multiple Fλ, defined by
((Fλ)u)(x) = λ (Fu)(λ⁻¹x), is convex when F is.
Theorem 38.3, the inner-product identity: ⟨(Fλ)u, x*⟩ = λ ⟨Fu, x*⟩.
Theorem 38.3, the adjoint formula: (Fλ)* = F*λ, with no hypothesis beyond 0 < λ.
Theorem 38.3, second assertion, closedness: Fλ is closed when F is closed convex and
λ > 0.
Theorem 38.3, second assertion, properness: Fλ is proper when F is and λ > 0.
Theorem 38.4 #
Theorem 38.4, first assertion: the image Ff of a proper convex f on ℝᵐ under a
proper convex bifunction F, (Ff)(x) = inf_u {f(u) + (Fu)(x)}, is convex on ℝⁿ.
Theorem 38.4, the conjugacy formula: (Ff)* = F⁎* f*. Where the book asks that ri (dom f)
meet ri (dom F), the hypothesis here is the IsExactSum of Theorem 16.4 for f and
u ↦ ⟨Fu, x*⟩, whose properness field is his side condition x* ∈ dom F*.
Theorem 38.4, the attainment clause: the infimum defining (F⁎* f*)(x*) is attained.
Corollary 38.4.1 #
The IsExactSum Corollary 38.4.1 consumes; the book's condition is that ri (dom f*) meets
ri (dom F⁎*).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Corollary 38.4.1, first assertion: Ff is closed, being a conjugate.
Corollary 38.4.1, middle assertion: the infimum defining (Ff)(x) is attained.
Corollary 38.4.1, last assertion: (Ff)* = cl (F⁎* f*).
Theorem 38.5 #
(GF)⁎ = F⁎ G⁎: inversion reverses the order of a product.
Theorem 38.5, first assertion: the product GF, ((GF)u)(y) = inf_x {(Fu)(x) + (Gx)(y)},
is a convex bifunction from ℝᵐ to ℝᵖ.
Theorem 38.5, the adjoint formula: (GF)* = F* G*, the product on the right being the
concave one. Where the book asks that ri (dom F⁎) meet ri (dom G), the hypothesis here is
IsExactSum for f(x) = ⟨u*, F⁎x⟩ and g(x) = ⟨Gx, y*⟩, one instance per (y*, u*).
Theorem 38.5, the attainment clause: the supremum defining ((F* G*)y*)(u*) is
attained.
Corollary 38.5.1 #
The IsExactSum Corollary 38.5.1 consumes; the book's condition is that ri (dom F*) and
ri (dom G⁎*) have a point in common.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Corollary 38.5.1, first assertion: GF is closed, being a lower adjoint.
Corollary 38.5.1, middle assertion: the infimum defining ((GF)u)(y) is attained.
Corollary 38.5.1, last assertion: (GF)* = cl (F* G*), in the F⁎* packaging
(GF)⁎* = cl (G⁎* F⁎*) — inversion reverses the order twice, so the right-hand product is taken
in the same order as GF.
Lemma 38.6 #
Lemma 38.6, first assertion: if ⟨f, g⟩ exists then so does ⟨f*, g*⟩. The book's proof
is the chain −⟨f, g⟩ ≤ ⟨f*, g*⟩_sup ≤ ⟨f*, g*⟩_inf ≤ −⟨f, g⟩, whose middle link is weak
duality.
Lemma 38.6, the value: ⟨f*, g*⟩ = −⟨f, g⟩. The lemma's second assertion, that
⟨cl f, cl g⟩ then exists and equals ⟨f, g⟩, is not formalized.
Theorem 38.7 and Corollary 38.7.1 #
Corollary 38.7.1, existence: ⟨f, F*x*⟩ exists for every x*. Weak duality supplies one
inequality for free and Theorem 38.4 the other.
Corollary 38.7.1: ⟨Ff, x*⟩ = ⟨f, F*x*⟩ — an adjoint moves across the inner product. The
left side is (Ff)*(x*), the right the inner product of the convex f with the concave
F*x*.
Theorem 38.7, first equality: ⟨Ff, g*⟩ = ⟨f, F*g*⟩. Where the book asks that some u in
ri (dom f) ∩ ri (dom F) have ri (dom (Fu)) meeting ri (dom g), the hypothesis here is
IsExactSum together with a point at which f, F and g are all finite. The middle member
−⟨f*, F⁎g⟩ of the book's four-term chain is not formalized.
Theorem 38.7, last equality: ⟨F⁎*f*, g⟩ = −⟨Ff, g*⟩. The left side is the sup side of
⟨F⁎*f*, g⟩, and both sides unwind to the same double extremum.
Corollary 38.7.2 #
Corollary 38.7.2, the existence clause: ⟨Fu, G*y*⟩ exists.
Corollary 38.7.2, first equality: ⟨GFu, y*⟩ = ⟨Fu, G*y*⟩, Corollary 38.7.1 at the slice
Fu, since (GF)u = G(Fu). It carries the IsExactSum its proof consumes: the book derives that
hypothesis by "a pithy exercise in the calculus of relative interiors" left to the reader.
Corollary 38.7.2, second equality: ⟨GFu, y*⟩ = ⟨u, F*G*y*⟩ at every u ∈ ri (dom (GF)).
This is Corollary 33.2.1 with Theorem 38.5, and unlike the first equality it genuinely needs the
relative interior.
The closing discussion: co-finite bifunctions #
For a co-finite convex bifunction ⟨Fu, x*⟩ is finite for all u and x*: Corollary 13.3.1
at the slice Fu.
A closed convex bifunction is co-finite if and only if ⟨Fu, x*⟩ is finite for all u
and x*.
For a co-finite F the two inner products agree at every u: ⟨Fu, x*⟩ = ⟨u, F*x*⟩, which
is Corollary 33.2.1 with ri (dom F) = ℝᵐ.
The infimal convolution of two co-finite convex bifunctions is co-finite.
(F₁ □ F₂)* = F₁* □ F₂* for co-finite bifunctions, with Theorem 38.2's relative-interior
hypothesis discharged: the brackets are finite everywhere.
F ↦ Fλ with λ > 0 preserves co-finiteness.
A closed proper convex bifunction F from ℝᵐ to ℝⁿ is co-finite if and only if
dom F = ℝᵐ and dom F* = ℝⁿ. Rockafellar cites Theorem 34.2; the proof here does not use the
saddle-function correspondence at all, only Corollary 13.3.1 slice by slice.