Rockafellar, §39: Convex Processes #
A convex process from ℝᵐ to ℝⁿ is a multivalued map whose graph is a convex cone containing
the origin. It sits between a linear transformation and a convex bifunction, and it inherits a full
duality theory from §§30–38. All nine numbered results of §39 are formalized: Theorems 39.1–39.8
and Corollary 39.7.1.
Implementation notes #
Orientation is data, not a convention. Rockafellar is explicit: "an oriented convex set is a
pair consisting of a convex set and one of the words supremum or infimum". Theorems 39.5 and
39.8 require two processes to carry the same orientation and Theorem 39.2 flips it, so both
orientations have to be simultaneously expressible: a global convention of the kind §36 imposes on
saddle-functions cannot even state Theorem 39.5. Hence Orientation, OrientedProcess and the
dispatch Orientation.adjointProcess.
PolyhedralConvexProcess is a surface definition; no numbered result of §39 needs it.
Divergences from the book #
Theorem 39.1 is stated with A 0 = {0} where the book assumes A 0 bounded. The first line of
Rockafellar's proof turns one into the other and nothing later uses boundedness, so A 0 = {0} is
the hypothesis the theorem actually has, and it needs neither a norm nor finite dimension;
theorem_39_1_isBounded recovers the book's literal form.
Theorems 39.5, 39.7 and 39.8 carry an IsExactSum where the book carries a relative-interior
condition. IsExactSum demands proper summands, and the summands here are u ↦ -⟨Aᵢ u, x*⟩,
which take -∞ wherever Aᵢ u is unbounded in the direction x*; quantified over all x* that
forces dom Aᵢ* = ℝⁿ. The hypothesis is therefore strictly stronger than the book's — strong
enough to exclude §39's own running example Au = {x | x ≤ Bu} for u ≥ 0 — and the gap is not
closable by IsExactSum.of_relint.
Theorem 39.3's last assertion is stated without closedness on the u side, where the book prefixes
both halves with "if A is closed": that half is Corollary 33.2.1.
References #
- R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §39, pp. 413–424.
Convex processes: the elementary properties #
Each value A u of a convex process is a convex set.
A 0 consists precisely of the vectors y with A u + y ⊆ A u for every u.
dom A = {u | A u ≠ ∅} is a convex cone containing the origin.
range A = ⋃ {A u | u ∈ ℝᵐ} is a convex cone containing the origin.
dom A⁻¹ = range A.
range A⁻¹ = dom A.
Theorem 39.1 #
Theorem 39.1. A convex process from ℝᵐ to ℝⁿ with dom A = ℝᵐ and A 0 = {0} is a
linear transformation.
Rockafellar's hypothesis is that A 0 be bounded, and the first line of his proof turns that into
A 0 = {0}; nothing later uses boundedness. The hypothesis here is therefore strictly weaker than
the book's, and it needs neither a norm nor finite dimension.
Theorem 39.1 in the book's literal form, with A 0 bounded. The two hypotheses coincide,
A 0 being a convex cone containing the origin.
Polyhedral convex processes #
A convex process is polyhedral if its graph is a polyhedral convex cone. No numbered result
of §39 needs this — all nine are proved without it — so it is a surface definition, with
polyhedral_graph_of_polyhedral as the bridge to Polyhedral.
Instances For
The graph of a polyhedral convex process is a polyhedral convex set.
A polyhedral convex process is closed, a polyhedral convex cone being closed.
The algebra of convex processes #
dom (A₁ + A₂) = dom A₁ ∩ dom A₂.
The image A C of a convex set under a convex process is convex.
The image of a convex function under a convex process, (Af)(x) = inf {f u | u ∈ A⁻¹x}.
This is imageBifun at the indicator bifunction of A; imageFn_apply turns the unrestricted
infimum of imageBifun into the book's restricted one.
Equations
Instances For
(Af)(x) = inf {f u | u ∈ A⁻¹x}, the book's own formula. The hypothesis f u ≠ ⊥ is what
turns the summand f u + δ(x | A u) into ⊤ off the fibre; it is automatic for the proper convex
f of Theorem 39.7.
(BA)⁻¹ = A⁻¹B⁻¹.
Multiplication of convex processes is associative, so the convex processes from ℝⁿ to itself
form a semigroup under multiplication.
The identity transformation is a left identity for multiplication of convex processes.
And a right identity.
A⁻¹A is in general multivalued and not the identity transformation: for the zero map on
ℝ¹, A⁻¹0 = ℝ¹ and (A⁻¹A) u = ℝ¹, whereas I u = {u}. This is why the convex processes from
ℝⁿ to itself form a semigroup and not a group.
The first distributive inequality: A(A₁ + A₂) ⊇ AA₁ + AA₂, inclusion in the sense of
graphs.
The second distributive inequality: (A₁ + A₂)A ⊆ A₁A + A₂A.
The complete lattice of convex processes #
The lattice of pointed cones is Mathlib's Submodule lattice, and the structure is transported
along the graph bijection rather than rebuilt.
A convex process is its graph: the bijection between convex processes and pointed convex cones in the product, along which the lattice structure is transported.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The convex processes from ℝᵐ to ℝⁿ form a complete lattice under inclusion, "inasmuch
as the collection of all convex cones containing the origin in ℝᵐ⁺ⁿ is a complete lattice under
inclusion".
The order of the lattice is inclusion of graphs, Rockafellar's A ⊇ B read the other way
round.
Orientation #
Rockafellar's orientation: "an oriented convex set is a pair consisting of a convex set and one of the words supremum or infimum". This is that word.
- sup : Orientation
The supremum orientation:
Cis identified withδ(· | C). - inf : Orientation
The infimum orientation:
Cis identified with-δ(· | C).
Instances For
The opposite orientation. The inverse of an oriented convex process is given the opposite orientation, and so is its adjoint (Theorem 39.2).
Equations
Instances For
The inner product ⟨C, x*⟩ = ⟨x*, C⟩ of an oriented convex set with a vector: the supremum
of ⟨x, x*⟩ over C when C is supremum oriented, the infimum when it is infimum oriented.
Equations
- Rockafellar.Orientation.sup.bracketSet C y = ⨆ x ∈ C, ↑(((TdafSurface.pairing n) x) y)
- Rockafellar.Orientation.inf.bracketSet C y = ⨅ x ∈ C, ↑(((TdafSurface.pairing n) x) y)
Instances For
For a supremum-oriented convex set, ⟨C, ·⟩ is the support function of C, the convex
conjugate of δ(· | C).
For an infimum-oriented convex set, ⟨C, x*⟩ = -δ*(-x* | C); that is, ⟨C, ·⟩ is the concave
conjugate of -δ(· | C).
An oriented convex process is a convex process together with an orientation, A u carrying
that orientation for every u. It must be a pair: Theorems 39.5 and 39.8 require two processes to
carry the same orientation and Theorem 39.2 flips it, so no global convention can state them.
- process : Tdaf.ConvexAnalysis.ConvexProcess (TdafSurface.Rn m) (TdafSurface.Rn n)
The underlying convex process.
- orientation : Orientation
The orientation, one of the two words.
Instances For
The adjoint of a convex process in a given orientation: adjointProcess for the supremum
orientation and coadjointProcess for the infimum one, the two differing only in the direction of
the defining inequality.
Equations
Instances For
The inverse of an oriented convex process, with the opposite orientation.
Instances For
The adjoint A* of an oriented convex process: an oriented convex process from ℝⁿ to
ℝᵐ, with the opposite orientation.
Equations
- A.adjoint = { process := A.orientation.adjointProcess A.process, orientation := A.orientation.flip }
Instances For
The sum of two convex processes with like orientation, given that same orientation. Only sums of processes with like orientation are considered, which is why every theorem about a sum below carries the hypothesis that the two orientations agree.
Equations
- Rockafellar.OrientedProcess.instAdd = { add := fun (A₁ A₂ : Rockafellar.OrientedProcess m n) => { process := A₁.process + A₂.process, orientation := A₁.orientation } }
The scalar multiple λA, with the same orientation.
Equations
- Rockafellar.OrientedProcess.instSMulReal = { smul := fun (a : ℝ) (A : Rockafellar.OrientedProcess m n) => { process := a • A.process, orientation := A.orientation } }
The product BA of two convex processes with like orientation, given that same
orientation.
Instances For
The inner product ⟨Au, x*⟩ of an oriented convex process, the value A u being read with
A's orientation.
Equations
- A.bracket u y = A.orientation.bracketSet (A.process.eval u) y
Instances For
The supremum-oriented inner product is §33's bracket of the indicator bifunction of A, which
is where every clause of Theorem 39.3 about a supremum-oriented process comes from.
The infimum-oriented inner product is ConvexProcess.coBracket.
bracket_sup as an equation between functions on the product, the shape Theorems 39.3 and 39.4
state their closure identities in.
When A is a linear transformation, the adjoint of A as a convex process — in either
orientation — is the adjoint linear transformation.
Theorem 39.2 #
Theorem 39.2, first assertion: A* has the opposite orientation to A. This holds by
construction, and it is the clause that forces the orientation to be data.
Theorem 39.2, first assertion: A* is a closed convex process from ℝⁿ to ℝᵐ, in
either orientation, being an intersection of homogeneous closed half-spaces.
Theorem 39.2, second assertion: A** = cl A. Read through the graph this is the bipolar
theorem K°° = cl K of §14; the two sign flips cancel because the second adjoint is taken in the
opposite orientation.
Theorem 39.2, last assertion: the adjoint of the indicator bifunction of a
supremum-oriented convex process A is the indicator bifunction of A*. The indicator appears
negated because A* carries the opposite orientation, and an infimum-oriented set is identified
with -δ(· | ·). The infimum-oriented mirror is not formalized.
Theorem 39.3 #
Theorem 39.3, first assertion: ⟨Au, x*⟩ is positively homogeneous in x* for each
u, in either orientation.
Theorem 39.3, first assertion: for a supremum-oriented A, ⟨Au, x*⟩ is convex in
x*, being the support function of A u.
Theorem 39.3, first assertion: for a supremum-oriented A, ⟨Au, x*⟩ is closed in
x*.
Theorem 39.3, "likewise when A is infimum oriented, except that then convexity and
concavity are reversed": ⟨Au, x*⟩ is concave in x*.
Theorem 39.3, infimum-oriented mirror: ⟨Au, x*⟩ is closed concave in x*.
Theorem 39.3, first assertion: ⟨Au, x*⟩ is positively homogeneous in u for each
x*, in either orientation. This is the one clause that uses the definition of a convex process
rather than §33: it is axiom (b), A(λu) = λ(Au).
Theorem 39.3, first assertion: for a supremum-oriented A, ⟨Au, x*⟩ is concave in
u for each x*.
Theorem 39.3, infimum-oriented mirror: ⟨Au, x*⟩ is convex in u. Reversing the
orientation exchanges convexity and concavity in both variables at once.
Theorem 39.3, third assertion: ⟨u, A* x*⟩ = cl_u ⟨Au, x*⟩ for a supremum-oriented A,
the closure being the concave one because ⟨A ·, x*⟩ is concave. No closedness of A is
needed.
Theorem 39.3, third assertion, infimum-oriented mirror: the closure is now the ordinary
convex one, because ⟨A ·, x*⟩ is convex.
Theorem 39.3, fourth assertion: if A is closed then ⟨Au, x*⟩ = cl_{x*} ⟨u, A* x*⟩, the
closure in the dual variable being the ordinary convex one. Closedness is genuinely needed here: it
is Theorem 33.2's second equation.
Theorem 39.3, last assertion: ⟨Au, x*⟩ = ⟨u, A* x*⟩ whenever u ∈ ri (dom A). The book
prefixes this and its dual with "if A is closed"; this half is Corollary 33.2.1, whose only input
is that a concave function agrees with its closure on ri (dom), so no closedness is needed.
Theorem 39.3, last assertion, dual half: for a closed A, ⟨Au, x*⟩ = ⟨u, A* x*⟩
whenever x* ∈ ri (dom A*).
Theorem 39.4 #
Theorem 39.4. The relations K (u, x*) = ⟨Au, x*⟩ and Au = {x | ⟨x, x*⟩ ≤ K (u, x*) ∀ x*}
are a one-to-one correspondence between the lower closed concave-convex functions K on
ℝᵐ × ℝⁿ with K (0, 0) = 0 that are positively homogeneous in each variable separately, and the
supremum-oriented closed convex processes from ℝᵐ to ℝⁿ. Closedness sits inside the ∃!
because uniqueness is uniqueness among closed processes.
Theorem 39.4, second displayed relation: a closed convex process is recovered from its
inner product by Au = {x | ⟨x, x*⟩ ≤ K (u, x*) for every x*}.
Theorem 39.5 #
Theorem 39.5. For convex processes A₁, A₂ from ℝᵐ to ℝⁿ with the same
orientation, (A₁ + A₂)* = A₁* + A₂*. The agreement of orientations is load-bearing and is the
reason orientation has to be data.
Where the book asks for ri (dom A₁) ∩ ri (dom A₂) ≠ ∅, the hypothesis here is the exactness of
the sum of the two support functions u ↦ -⟨Aᵢ u, x*⟩, one instance per x* — strictly stronger;
see the module docstring.
Theorem 39.5, second statement, first half: for closed A₁ and A₂, A₁ + A₂ is closed.
Where the book asks that ri (dom A₁*) and ri (dom A₂*) meet, the hypothesis here is again an
IsExactSum. The proof does not use Corollary 38.2.1: A₁ + A₂ is the infimum-oriented adjoint
of A₁* + A₂*.
Theorem 39.5, second statement, second half: (A₁ + A₂)* is the closure of
A₁* + A₂*.
Theorem 39.6 #
Theorem 39.7 #
Theorem 39.7, first assertion: for a supremum-oriented convex process A and a proper
convex f on ℝᵐ, (Af)* = A*⁻¹ f*. Where the book asks for ri (dom f) ∩ ri (dom A) ≠ ∅, the
hypothesis here is the exactness of f + (-⟨A ·, x*⟩); see the module docstring.
Theorem 39.7, second assertion: the infimum defining (A*⁻¹ f*)(x*) is attained.
Theorem 39.7, third assertion: for closed A and f, Af is closed. Where the book asks
that ri (dom f*) meet ri (dom A*⁻¹), the hypothesis here is again an IsExactSum.
Theorem 39.7, fourth assertion, in the book's own form: wherever Af is finite there is a
u with x ∈ Au and f u = (Af)(x).
Theorem 39.7, last assertion: (Af)* is the closure of A*⁻¹ f*.
Corollary 39.7.1 #
Corollary 39.7.1. For a closed convex process A and a nonempty closed convex C ⊆ ℝᵐ, if
no nonzero vector of A⁻¹0 lies in the recession cone of C, then AC is closed.
Proved as Theorem 9.1 for the projection (u, x) ↦ x rather than by specialising Theorem 39.7:
AC is the image of graph A ∩ (C × ℝⁿ), whose recession cone is graph A ∩ (0⁺C × ℝⁿ).
Corollary 39.7.1, the parenthesis "which is true in particular if C is bounded": the
image of a nonempty compact convex set under a closed convex process is closed.
Theorem 39.8 #
Theorem 39.8. For a convex process A from ℝᵐ to ℝⁿ and B from ℝⁿ to ℝᵖ with the
same orientation, (BA)* = A* B*. As in Theorem 39.5, the agreement of orientations is a
hypothesis only a formal orientation pair can express.
Where the book asks for ri (range A) ∩ ri (dom B) ≠ ∅, the hypothesis here is the exactness of
the corresponding sum, one instance per (z*, u*). The proof does not go through Theorem 38.5: it
is a linear sandwich produced by Fenchel's duality theorem.
Theorem 39.8, second statement, first half: for closed A and B, BA is closed. Where
the book asks that ri (range B*) meet ri (dom A*), the hypothesis here is again an
IsExactSum.
Theorem 39.8, second statement, second half: (BA)* is the closure of A* B*.