Convex processes

A convex process from U to X is a multivalued map A : u ↦ A u with A (u₁ + u₂) ⊇ A u₁ + A u₂, A (λ u) = λ (A u) for λ > 0, and 0 ∈ A 0. These conditions say exactly that the graph {(u, x) | x ∈ A u} is a convex cone containing the origin, so that is what ConvexProcess is: a bundled PointedCone ℝ (U × X), with A.eval u the u-slice of the cone and every elementary property a Submodule fact in disguise. Processes sit between linear transformations and convex bifunctions — ofLinearMap embeds the former, indicatorBifun embeds a process into the latter — and carry the adjoint, sum, product and inverse of that algebra.

The adjoint A* is the polar of the graph with a sign flip on one factor: (y, v) ∈ graph A* iff (-v, y) ∈ (graph A)° (mem_graph_adjointProcess_iff_mem_polarCone), the sign convention adjointBifun uses, so everything topological about A* comes from the theory of polar cones.

Rockafellar carries "supremum oriented" and "infimum oriented" as extra data on a convex set and defines the adjoint of an infimum-oriented process by reversing the inequality. Here the two are two definitions, adjointProcess and coadjointProcess, and A** uses one of each: with adjointProcess twice the sign flips add instead of cancelling, giving {p | ∀ w ∈ K°, 0 ≤ ⟨p, w⟩} in place of the bipolar K°°. Reflection through the origin (reflect) exchanges the two adjoints and commutes with sums and products, so every infimum-oriented statement below — they carry a co in their names — is the supremum-oriented one read back through it. The inner products are the exception: reflection flips the dual variable only, and coBracket_eq_neg_bracket records the sign.

Main definitions

• ConvexProcess U X — a convex process, carried by its graph. eval, dom, range, image, inv are A u, dom A, range A, A C, A⁻¹; comp with the Add and SMul instances are B A, A₁ + A₂ and λ A. ofLinearMap embeds a linear transformation, and indicatorBifun is the bifunction (F u)(x) = δ(x | A u).
• ConvexProcess.adjointProcess, coadjointProcess, reflect — the two adjoints and the reflection exchanging them; coBracket is the inner product ⟨Au, x*⟩ = inf {⟨x, x*⟩ | x ∈ A u} of an infimum-oriented process.

Main results

• exists_linearMap_of_isBounded — a convex process with full domain and bounded A 0 is a linear transformation (Theorem 39.1 in [^1]).
• isClosed_graph_adjointProcess, coadjointProcess_adjointProcess_eq_self_iff — A* is always closed, A** = cl A, and A** = A exactly for closed A.
• bracket_indicatorBifun and the results beside it — ⟨Au, x*⟩ is the support function of A u, hence closed convex in x* and concave in u, and ⟨u, A* x*⟩ is its convex closure in u (Theorem 39.3 in [^1]).
• adjointProcess_add, adjointProcess_comp, adjointProcess_smul — (A₁ + A₂)* = A₁* + A₂*, (BA)* = A* B* and (λ A)* = λ (A*) for λ > 0; isClosed_graph_add, graph_adjointProcess_add_eq_closure and the comp analogues are the closed halves.
• conj_imageBifun_indicatorBifun — (Af)* = A*⁻¹ f*, the infimum attained (Theorem 39.7 in [^1]).
• isClosed_image — A C is closed for closed A, nonempty closed convex C, and no non-zero vector of A⁻¹ 0 receding C.
• exists_pairing_sandwich — Fenchel duality at a positively homogeneous pair: a concave p below a convex q, both straddling 0 at the origin, admit a linear ⟨·, y⟩ between them.

Implementation notes

The adjoints of a sum and of a product take an IsExactSum hypothesis, one instance per dual vector, where Rockafellar assumes ri (dom A₁) ∩ ri (dom A₂) ≠ ∅. IsExactSum also requires both summands proper, so the hypothesis carried here is stronger than the book's.

References

[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §39.

The definition

structure Tdaf.ConvexAnalysis.ConvexProcess (U : Type u_3) (X : Type u_4) [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] : Type (max u_3 u_4)

A convex process from U to X: a multivalued map A : u ↦ Au with

• A (u₁ + u₂) ⊇ A u₁ + A u₂,
• A (λ u) = λ (A u) for λ > 0,
• 0 ∈ A 0,

which Rockafellar shows is the same thing as a convex cone in U × X containing the origin — that is, a PointedCone ℝ (U × X), read as a relation.

• graph : PointedCone ℝ (U × X)

  The graph of the process.

def Tdaf.ConvexAnalysis.ConvexProcess.eval {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) (u : U) : Set X

The value A u of the process at u: the u-slice of its graph.

Equations

• A.eval u = {x : X | (u, x) ∈ A.graph}

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.mem_eval {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {A : ConvexProcess U X} {u : U} {x : X} : x ∈ A.eval u ↔ (u, x) ∈ A.graph

def Tdaf.ConvexAnalysis.ConvexProcess.toSetRel {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) : SetRel U X

The graph of a convex process, as a relation.

Equations

• A.toSetRel = ↑A.graph

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.mem_toSetRel {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {A : ConvexProcess U X} {p : U × X} : p ∈ A.toSetRel ↔ p ∈ A.graph

def Tdaf.ConvexAnalysis.ConvexProcess.dom {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) : Set U

The effective domain of a convex process: the u at which A u is nonempty.

Equations

• A.dom = {u : U | (A.eval u).Nonempty}

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.mem_dom {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {A : ConvexProcess U X} {u : U} : u ∈ A.dom ↔ (A.eval u).Nonempty

def Tdaf.ConvexAnalysis.ConvexProcess.range {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) : Set X

The range of a convex process.

Equations

• A.range = {x : X | ∃ (u : U), (u, x) ∈ A.graph}

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.mem_range {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {A : ConvexProcess U X} {x : X} : x ∈ A.range ↔ ∃ (u : U), (u, x) ∈ A.graph

def Tdaf.ConvexAnalysis.ConvexProcess.image {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) (C : Set U) : Set X

The image of a set under a convex process: A C = ⋃ {A u | u ∈ C}.

Equations

• A.image C = {x : X | ∃ u ∈ C, (u, x) ∈ A.graph}

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.mem_image {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {A : ConvexProcess U X} {x : X} {C : Set U} : x ∈ A.image C ↔ ∃ u ∈ C, (u, x) ∈ A.graph

theorem Tdaf.ConvexAnalysis.ConvexProcess.image_univ {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) : A.image Set.univ = A.range

theorem Tdaf.ConvexAnalysis.ConvexProcess.ext {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {A B : ConvexProcess U X} (h : A.graph = B.graph) : A = B

Two convex processes with the same graph are equal.

theorem Tdaf.ConvexAnalysis.ConvexProcess.ext_iff {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {A B : ConvexProcess U X} : A = B ↔ A.graph = B.graph

def Tdaf.ConvexAnalysis.ConvexProcess.ofLinearMap {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (T : U →ₗ[ℝ] X) : ConvexProcess U X

A linear transformation, read as a convex process. Its graph is the graph of T, a linear subspace and hence in particular a pointed convex cone.

Equations

• Tdaf.ConvexAnalysis.ConvexProcess.ofLinearMap T = { graph := { carrier := {p : U × X | p.2 = T p.1}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ } }

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.mem_graph_ofLinearMap {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {T : U →ₗ[ℝ] X} {p : U × X} : p ∈ (ofLinearMap T).graph ↔ p.2 = T p.1

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.eval_ofLinearMap {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (T : U →ₗ[ℝ] X) (u : U) : (ofLinearMap T).eval u = {T u}

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.dom_ofLinearMap {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (T : U →ₗ[ℝ] X) : (ofLinearMap T).dom = Set.univ

def Tdaf.ConvexAnalysis.ConvexProcess.inv {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) : ConvexProcess X U

The inverse of a convex process, again a convex process.

Equations

• A.inv = { graph := { carrier := {p : X × U | (p.2, p.1) ∈ A.graph}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ } }

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.mem_graph_inv {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {A : ConvexProcess U X} {p : X × U} : p ∈ A.inv.graph ↔ (p.2, p.1) ∈ A.graph

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.mem_eval_inv {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {A : ConvexProcess U X} {u : U} {x : X} : u ∈ A.inv.eval x ↔ (u, x) ∈ A.graph

theorem Tdaf.ConvexAnalysis.ConvexProcess.inv_inv {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) : A.inv.inv = A

theorem Tdaf.ConvexAnalysis.ConvexProcess.dom_inv {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) : A.inv.dom = A.range

theorem Tdaf.ConvexAnalysis.ConvexProcess.range_inv {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) : A.inv.range = A.dom

Elementary structure

theorem Tdaf.ConvexAnalysis.ConvexProcess.convex_graph {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) : Convex ℝ ↑A.graph

theorem Tdaf.ConvexAnalysis.ConvexProcess.smul_mem_graph {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {A : ConvexProcess U X} {a : ℝ} (ha : 0 ≤ a) {p : U × X} (hp : p ∈ A.graph) : a • p ∈ A.graph

Membership of a nonnegative multiple, in the form the PointedCone coercion hides.

theorem Tdaf.ConvexAnalysis.ConvexProcess.add_mem_graph {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {A : ConvexProcess U X} {p q : U × X} (hp : p ∈ A.graph) (hq : q ∈ A.graph) : p + q ∈ A.graph

theorem Tdaf.ConvexAnalysis.ConvexProcess.zero_mem_graph {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) : (0, 0) ∈ A.graph

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.zero_mem_eval_zero {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) : 0 ∈ A.eval 0

theorem Tdaf.ConvexAnalysis.ConvexProcess.convex_eval {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) (u : U) : Convex ℝ (A.eval u)

Each value A u of a convex process is a convex set.

theorem Tdaf.ConvexAnalysis.ConvexProcess.smul_mem_eval_zero {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {x : X} (A : ConvexProcess U X) {a : ℝ} (ha : 0 ≤ a) (hx : x ∈ A.eval 0) : a • x ∈ A.eval 0

A 0 is a cone: it is stable under multiplication by a nonnegative scalar.

theorem Tdaf.ConvexAnalysis.ConvexProcess.add_eval_zero_subset {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) (u : U) : A.eval u + A.eval 0 ⊆ A.eval u

A u + A 0 ⊆ A u, so A 0 is a set of directions along which every value of the process is invariant.

theorem Tdaf.ConvexAnalysis.ConvexProcess.convex_dom {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) : Convex ℝ A.dom

The effective domain of a convex process is convex.

theorem Tdaf.ConvexAnalysis.ConvexProcess.convex_range {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) : Convex ℝ A.range

theorem Tdaf.ConvexAnalysis.ConvexProcess.convex_image {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) {C : Set U} (hC : Convex ℝ C) : Convex ℝ (A.image C)

The image of a convex set under a convex process is convex.

theorem Tdaf.ConvexAnalysis.ConvexProcess.image_eq_image_snd {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) (C : Set U) : A.image C = ⇑(LinearMap.snd ℝ U X) '' (↑A.graph ∩ C ×ˢ Set.univ)

The image A C is the projection of graph A ∩ (C × X) on the second factor. This is what turns closedness of A C into a statement about the image of a convex set under a linear map.

The indicator bifunction

theorem Tdaf.ConvexAnalysis.indicatorFn_injective {W : Type u_1} : Function.Injective indicatorFn

The indicator function determines its set.

Proof idea: δ(· | S) takes the value 0 exactly on S and ⊤ off it, and 0 ≠ ⊤ in EReal.

noncomputable def Tdaf.ConvexAnalysis.ConvexProcess.indicatorBifun {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) : Bifun U X

The indicator bifunction of a supremum-oriented convex process: (F u)(x) = δ(x | A u). This is the dictionary entry making every result about processes one about bifunctions.

Equations

• A.indicatorBifun u = Tdaf.ConvexAnalysis.indicatorFn (A.eval u)

theorem Tdaf.ConvexAnalysis.ConvexProcess.indicatorBifun_apply {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) (u : U) (x : X) : A.indicatorBifun u x = indicatorFn (A.eval u) x

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.graphFn_indicatorBifun {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) : graphFn A.indicatorBifun = indicatorFn ↑A.graph

The graph function of the indicator bifunction of A is the indicator function of the graph of A.

theorem Tdaf.ConvexAnalysis.ConvexProcess.indicatorBifun_ne_bot {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) (u : U) (x : X) : A.indicatorBifun u x ≠ ⊥

theorem Tdaf.ConvexAnalysis.ConvexProcess.indicatorBifun_injective {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] : Function.Injective indicatorBifun

A convex process is determined by its indicator bifunction. A process is its graph, and the indicator function of a set determines the set, so this is indicatorFn_injective read through graphFn_indicatorBifun. It is what makes the correspondence with bifunctions one-to-one.

theorem Tdaf.ConvexAnalysis.ConvexProcess.convexBifun_indicatorBifun {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) : ConvexBifun A.indicatorBifun

The indicator bifunction of a convex process is a convex bifunction.

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.domBifun_indicatorBifun {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) : domBifun A.indicatorBifun = A.dom

The effective domain of the indicator bifunction is the effective domain of the process.

theorem Tdaf.ConvexAnalysis.ConvexProcess.smul_graph {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) {a : ℝ} (ha : 0 < a) : a • ↑A.graph = ↑A.graph

Positive multiples do not move the graph of a convex process: it is a cone.

theorem Tdaf.ConvexAnalysis.ConvexProcess.eval_smul_arg {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) {a : ℝ} (ha : 0 < a) (u : U) : A.eval (a • u) = a • A.eval u

A (λ u) = λ (A u) for λ > 0, the positive-homogeneity axiom of a convex process.

Both inclusions are one application of smul_mem_graph, to a and to a⁻¹: a cone is stable under both directions of a positive scaling, which is what turns the inclusion Rockafellar's axiom would give into an equality.

The algebra of convex processes, and its bifunction dictionary

theorem Tdaf.ConvexAnalysis.infConv_indicatorFn {X : Type u_2} [AddCommGroup X] (S T : Set X) : infConv (indicatorFn S) (indicatorFn T) = indicatorFn (S + T)

The infimal convolute of two indicator functions is the indicator function of the sum of the sets. Operations/InfConv.lean has only the special case of a singleton, so it is proved here.

@[instance_reducible]

instance Tdaf.ConvexAnalysis.ConvexProcess.instAdd {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] : Add (ConvexProcess U X)

The sum of two convex processes, (A₁ + A₂) u = A₁ u + A₂ u.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.mem_graph_add {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {A₁ A₂ : ConvexProcess U X} {p : U × X} : p ∈ (A₁ + A₂).graph ↔ ∃ x ∈ A₁.eval p.1, ∃ y ∈ A₂.eval p.1, p.2 = x + y

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.eval_add {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A₁ A₂ : ConvexProcess U X) (u : U) : (A₁ + A₂).eval u = A₁.eval u + A₂.eval u

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.dom_add {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A₁ A₂ : ConvexProcess U X) : (A₁ + A₂).dom = A₁.dom ∩ A₂.dom

The effective domain of a sum is the intersection: dom (A₁ + A₂) = dom A₁ ∩ dom A₂.

@[instance_reducible]

instance Tdaf.ConvexAnalysis.ConvexProcess.instSMulReal {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] : SMul ℝ (ConvexProcess U X)

The scalar multiple λ A, defined by (λ A) u = λ (A u).

The graph {(u, λ x) | (u, x) ∈ graph A} is a pointed convex cone for every real λ, so the definition needs no positivity; λ > 0 is needed only from adjointProcess_smul on, where the inverse scaling is used. The action is a MulAction — 1 • A = A and (ab) • A = a • (b • A) both hold — but it is not additive: 2 • A and A + A differ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.mem_graph_smul {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {a : ℝ} {A : ConvexProcess U X} {p : U × X} : p ∈ (a • A).graph ↔ ∃ (x : X), (p.1, x) ∈ A.graph ∧ p.2 = a • x

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.eval_smul {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (a : ℝ) (A : ConvexProcess U X) (u : U) : (a • A).eval u = a • A.eval u

(λ A) u = λ (A u), the defining equation of the scalar multiple.

def Tdaf.ConvexAnalysis.ConvexProcess.comp {U : Type u_1} {X : Type u_2} {Z : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Z] [Module ℝ Z] (B : ConvexProcess X Z) (A : ConvexProcess U X) : ConvexProcess U Z

The product of convex processes, (B A) u = B (A u).

Equations

• B.comp A = { graph := { carrier := {p : U × Z | ∃ (x : X), (p.1, x) ∈ A.graph ∧ (x, p.2) ∈ B.graph}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ } }

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.mem_graph_comp {U : Type u_1} {X : Type u_2} {Z : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Z] [Module ℝ Z] {B : ConvexProcess X Z} {A : ConvexProcess U X} {p : U × Z} : p ∈ (B.comp A).graph ↔ ∃ (x : X), (p.1, x) ∈ A.graph ∧ (x, p.2) ∈ B.graph

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.eval_comp {U : Type u_1} {X : Type u_2} {Z : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Z] [Module ℝ Z] (B : ConvexProcess X Z) (A : ConvexProcess U X) (u : U) : (B.comp A).eval u = B.image (A.eval u)

theorem Tdaf.ConvexAnalysis.ConvexProcess.inv_comp {U : Type u_1} {X : Type u_2} {Z : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Z] [Module ℝ Z] (B : ConvexProcess X Z) (A : ConvexProcess U X) : (B.comp A).inv = A.inv.comp B.inv

The inverse of a product is the product of the inverses: (B A)⁻¹ = A⁻¹ B⁻¹.

theorem Tdaf.ConvexAnalysis.ConvexProcess.indicatorBifun_add {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A₁ A₂ : ConvexProcess U X) : (A₁ + A₂).indicatorBifun = infConvBifun A₁.indicatorBifun A₂.indicatorBifun

The indicator bifunction of A₁ + A₂ is the infimal convolute F₁ □ F₂.

theorem Tdaf.ConvexAnalysis.ConvexProcess.indicatorBifun_comp {U : Type u_1} {X : Type u_2} {Z : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Z] [Module ℝ Z] (B : ConvexProcess X Z) (A : ConvexProcess U X) : (B.comp A).indicatorBifun = compBifun B.indicatorBifun A.indicatorBifun

The indicator bifunction of B A is the product G F of the indicator bifunctions.

The adjoint of a convex process

def Tdaf.ConvexAnalysis.ConvexProcess.adjointProcess {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) : ConvexProcess Y V

The adjoint of a supremum-oriented convex process: A* x* = {u* | ⟨u, u*⟩ ≥ ⟨x, x*⟩ for every x ∈ A u and every u}. It is a convex process from Y to V, and it is infimum oriented.

Equations

• One or more equations did not get rendered due to their size.

def Tdaf.ConvexAnalysis.ConvexProcess.coadjointProcess {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) : ConvexProcess Y V

The adjoint of an infimum-oriented convex process: the same definition with the inequality reversed. Keeping the two apart is what makes A** = cl A come out right.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.mem_graph_adjointProcess {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} {A : ConvexProcess U X} {q : Y × V} : q ∈ (adjointProcess Bu Bx A).graph ↔ ∀ p ∈ A.graph, (Bx p.2) q.1 ≤ (Bu p.1) q.2

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.mem_graph_coadjointProcess {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} {A : ConvexProcess U X} {q : Y × V} : q ∈ (coadjointProcess Bu Bx A).graph ↔ ∀ p ∈ A.graph, (Bu p.1) q.2 ≤ (Bx p.2) q.1

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.mem_eval_adjointProcess {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} {A : ConvexProcess U X} {y : Y} {v : V} : v ∈ (adjointProcess Bu Bx A).eval y ↔ ∀ p ∈ A.graph, (Bx p.2) y ≤ (Bu p.1) v

theorem Tdaf.ConvexAnalysis.ConvexProcess.mem_graph_adjointProcess_iff_mem_polarCone {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} {A : ConvexProcess U X} {q : Y × V} : q ∈ (adjointProcess Bu Bx A).graph ↔ (-q.2, q.1) ∈ polarCone (prodPairing Bu Bx) ↑A.graph

The graph of A* is the polar of the graph of A, up to the sign flip on the first factor that the adjoint of a bifunction carries.

theorem Tdaf.ConvexAnalysis.ConvexProcess.adjointBifun_indicatorBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) (y : Y) (v : V) : adjointBifun Bu Bx A.indicatorBifun y v = -(adjointProcess Bu Bx A).indicatorBifun y v

The adjoint of the indicator bifunction of A is the indicator bifunction of A*. A* carries the opposite orientation, which is why the indicator appears negated: an infimum-oriented set is identified with -δ(· | ·).

theorem Tdaf.ConvexAnalysis.ConvexProcess.graph_coadjointProcess_adjointProcess {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) : ↑(coadjointProcess Bx.flip Bu.flip (adjointProcess Bu Bx A)).graph = polarCone (prodPairing Bu Bx).flip (polarCone (prodPairing Bu Bx) ↑A.graph)

The graph of A** is the bipolar of the graph of A. The two sign flips cancel, which is why the second adjoint must be the infimum-oriented one.

theorem Tdaf.ConvexAnalysis.ConvexProcess.adjointProcess_smul {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) {a : ℝ} (ha : 0 < a) (A : ConvexProcess U X) : adjointProcess Bu Bx (a • A) = a • adjointProcess Bu Bx A

The adjoint of a scalar multiple: (λ A)* = λ (A*) for λ > 0.

Rockafellar deduces this from the adjoint formula for Fλ. It is cheaper here as a direct computation on cones: (y, v) ∈ graph (λA)* says λ⟨x, y⟩ ≤ ⟨u, v⟩ on graph A, which is (y, λ⁻¹ v) ∈ graph A* after dividing by λ, and that is exactly v ∈ λ (A* y). Positivity of λ is used only to divide.

theorem Tdaf.ConvexAnalysis.ConvexProcess.coadjointProcess_smul {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) {a : ℝ} (ha : 0 < a) (A : ConvexProcess U X) : coadjointProcess Bu Bx (a • A) = a • coadjointProcess Bu Bx A

The adjoint of a scalar multiple, for an infimum-oriented process: (λ A)* = λ (A*), with the adjoint taken in the reversed sense. The proof is adjointProcess_smul with both inequalities turned round.

A* is closed, and A** = cl A

theorem Tdaf.ConvexAnalysis.ConvexProcess.isClosed_graph_adjointProcess {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace V] [TopologicalSpace Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsContinuousPairing Bu.flip] [IsContinuousPairing Bx.flip] (A : ConvexProcess U X) : IsClosed ↑(adjointProcess Bu Bx A).graph

The adjoint of a convex process is a closed convex process, being an intersection of homogeneous closed half-spaces.

theorem Tdaf.ConvexAnalysis.ConvexProcess.graph_coadjointProcess_adjointProcess_eq_closure {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [TopologicalSpace X] [IsTopologicalAddGroup U] [IsTopologicalAddGroup X] [ContinuousSMul ℝ U] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ U] [LocallyConvexSpace ℝ X] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bx] (A : ConvexProcess U X) : ↑(coadjointProcess Bx.flip Bu.flip (adjointProcess Bu Bx A)).graph = closure ↑A.graph

A** = cl A. Read through graph_coadjointProcess_adjointProcess, this is exactly the bipolar theorem K°° = cl K for the graph.

theorem Tdaf.ConvexAnalysis.ConvexProcess.coadjointProcess_adjointProcess_eq_self_iff {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [TopologicalSpace X] [IsTopologicalAddGroup U] [IsTopologicalAddGroup X] [ContinuousSMul ℝ U] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ U] [LocallyConvexSpace ℝ X] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bx] (A : ConvexProcess U X) : coadjointProcess Bx.flip Bu.flip (adjointProcess Bu Bx A) = A ↔ IsClosed ↑A.graph

A convex process is closed exactly when it is its own second adjoint.

The two inner products

⟨Au, x*⟩ is the bracket of the indicator bifunction of A, and ⟨u, A* x*⟩ is the concave bracket of its adjoint. Both are ordinary extremum problems over the values of a process: a maximisation of ⟨·, x*⟩ over A u, and a minimisation of ⟨u, ·⟩ over A* x*.

theorem Tdaf.ConvexAnalysis.ConvexProcess.bracket_indicatorBifun {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) (u : U) : bracket Bx A.indicatorBifun u = supportFn Bx (A.eval u)

The inner product ⟨Au, x*⟩ is the support function of the convex set A u. Every clause about the x* variable below is then a property of support functions; the identity itself is supportFn_eq_conj_indicatorFn read backwards, since ⟨Fu, ·⟩ is by definition the conjugate of F u = δ(· | A u).

theorem Tdaf.ConvexAnalysis.ConvexProcess.bracket_indicatorBifun_apply {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) (u : U) (y : Y) : bracket Bx A.indicatorBifun u y = ⨆ x ∈ A.eval u, ↑((Bx x) y)

The first of Rockafellar's two extremum problems: ⟨Au, x*⟩ = sup {⟨x, x*⟩ | x ∈ A u}.

theorem Tdaf.ConvexAnalysis.ConvexProcess.posHomogeneous_bracket_indicatorBifun {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) (u : U) : PosHomogeneous (bracket Bx A.indicatorBifun u)

⟨Au, ·⟩ is positively homogeneous, being a support function.

theorem Tdaf.ConvexAnalysis.ConvexProcess.convexFn_bracket_indicatorBifun {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) (u : U) : ConvexFn (bracket Bx A.indicatorBifun u)

⟨Au, ·⟩ is convex, being a conjugate.

theorem Tdaf.ConvexAnalysis.ConvexProcess.posHomogeneous_bracket_indicatorBifun_arg {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) (y : Y) : PosHomogeneous fun (u : U) => bracket Bx A.indicatorBifun u y

⟨A ·, x*⟩ is positively homogeneous. This is the one clause that uses the definition of a convex process rather than the general theory of brackets: A (λ u) = λ (A u) (eval_smul_arg), and the support function of a positive multiple of a set is the corresponding multiple of the support function.

theorem Tdaf.ConvexAnalysis.ConvexProcess.concaveFn_bracket_indicatorBifun {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) (y : Y) : ConcaveFn fun (u : U) => bracket Bx A.indicatorBifun u y

⟨A ·, x*⟩ is concave, the bracket of a convex bifunction being concave in its first variable.

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.bracket_indicatorBifun_zero_zero {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) : bracket Bx A.indicatorBifun 0 0 = 0

The inner product ⟨Au, x*⟩ vanishes at the origin, because A 0 contains 0 and the support function of a nonempty set is 0 at 0.

theorem Tdaf.ConvexAnalysis.ConvexProcess.closedFn_bracket_indicatorBifun {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace Y] [IsTopologicalAddGroup Y] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsContinuousPairing Bx.flip] (A : ConvexProcess U X) (u : U) : ClosedFn (bracket Bx A.indicatorBifun u)

⟨Au, ·⟩ is closed as well as convex and positively homogeneous.

theorem Tdaf.ConvexAnalysis.ConvexProcess.concaveBracket_adjointBifun_indicatorBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) (u : U) (y : Y) : concaveBracket Bu (adjointBifun Bu Bx A.indicatorBifun) u y = ⨅ v ∈ (adjointProcess Bu Bx A).eval y, ↑((Bu u) v)

The second of Rockafellar's two extremum problems: ⟨u, A* x*⟩ = inf {⟨u, u*⟩ | u* ∈ A* x*}.

Together with bracket_indicatorBifun_apply this is a dual pair of linear programs; the two values differ only by a closure in u (concaveBracket_adjointBifun_indicatorBifun_eq_partialCl₁). The proof is the definition of the concave bracket plus adjointBifun_indicatorBifun: the indicator of A* x* turns the unrestricted infimum into a restricted one.

theorem Tdaf.ConvexAnalysis.ConvexProcess.concaveBracket_adjointBifun_indicatorBifun_eq_partialCl₁ {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} (A : ConvexProcess U X) (y : Y) : (fun (u : U) => concaveBracket Bu (adjointBifun Bu Bx A.indicatorBifun) u y) = fun (u : U) => partialCl₁ (fun (p : U × Y) => bracket Bx A.indicatorBifun p.1 p.2) (u, y)

⟨u, A* x*⟩ = cl_u ⟨Au, x*⟩: the two inner products differ by a closure in u.

The concave closure in the first variable is the only difference between them, for every convex process — closedness of A plays no part. This is concaveBracket_adjointBifun_eq_partialCl₁ applied to the indicator bifunction.

The adjoint of a sum of processes

theorem Tdaf.ConvexAnalysis.supConv_neg_indicatorFn {X : Type u_1} [AddCommGroup X] (S T : Set X) : (supConv (fun (x : X) => -indicatorFn S x) fun (x : X) => -indicatorFn T x) = fun (x : X) => -indicatorFn (S + T) x

The concave mirror of infConv_indicatorFn: the supremal convolute of two negated indicator functions is the negated indicator function of the sum of the sets. Infimum-oriented convex sets are carried by -δ(· | ·) (see ConvexProcess.adjointBifun_indicatorBifun), so this is the form in which the adjoint of an infimal convolute speaks about processes.

Proof idea: supConv is infConv conjugated by negation, so the two negations inside cancel and infConv_indicatorFn applies verbatim.

theorem Tdaf.ConvexAnalysis.ConvexProcess.adjointProcess_add {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A₁ A₂ : ConvexProcess U X) (hex : ∀ (y : Y), IsExactSum Bu (fun (u : U) => -supportFn Bx (A₁.eval u) y) fun (u : U) => -supportFn Bx (A₂.eval u) y) : adjointProcess Bu Bx (A₁ + A₂) = adjointProcess Bu Bx A₁ + adjointProcess Bu Bx A₂

The adjoint of a sum is the sum of the adjoints: (A₁ + A₂)* = A₁* + A₂*.

Where the book assumes ri (dom A₁) ∩ ri (dom A₂) ≠ ∅, the hypothesis here is exactness of the sum of the two support functions u ↦ ⟨Aᵢ u, y⟩, one instance per y. Since IsExactSum also requires both summands proper, this is stronger than the book's hypothesis.

The adjoint of a product of processes

theorem Tdaf.ConvexAnalysis.exists_pairing_sandwich {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {p q : E → EReal} (hex : IsExactSum B q fun (x : E) => -p x) (hle : ∀ (x : E), p x ≤ q x) (hp0 : 0 ≤ p 0) (hq0 : q 0 ≤ 0) : ∃ (y : F), (∀ (x : E), p x ≤ ↑((B x) y)) ∧ ∀ (x : E), ↑((B x) y) ≤ q x

A linear sandwich. If a concave p lies below a convex q, the two add exactly, and each straddles 0 at the origin from its own side, then some ⟨·, y⟩ runs between them.

This is Fenchel's duality theorem read at a positively homogeneous pair. The two extrema are p*(y) ≤ 0 and q*(y) ≥ 0 for free, so the attained dual value p*(y) - q*(y) ≥ 0 forces both to vanish, and p*(y) = 0 and q*(y) = 0 say precisely p ≤ ⟨·, y⟩ and ⟨·, y⟩ ≤ q. No convexity hypothesis appears: IsExactSum already carries it.

theorem Tdaf.ConvexAnalysis.ConvexProcess.comp_adjointProcess_le {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} {Z : Type u_5} {W : Type u_6} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [AddCommGroup Z] [Module ℝ Z] [AddCommGroup W] [Module ℝ W] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (Bz : Z →ₗ[ℝ] W →ₗ[ℝ] ℝ) (A : ConvexProcess U X) (B : ConvexProcess X Z) : ((adjointProcess Bu Bx A).comp (adjointProcess Bx Bz B)).graph ≤ (adjointProcess Bu Bz (B.comp A)).graph

The inclusion that costs nothing: A* B* ⊆ (BA)*.

A pair (z*, u*) that factors through B* and then A* chains the two defining inequalities, ⟨z, z*⟩ ≤ ⟨x, x*⟩ ≤ ⟨u, u*⟩, for every factorisation u ↦ x ↦ z in BA.

theorem Tdaf.ConvexAnalysis.ConvexProcess.adjointProcess_comp {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} {Z : Type u_5} {W : Type u_6} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [AddCommGroup Z] [Module ℝ Z] [AddCommGroup W] [Module ℝ W] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (Bz : Z →ₗ[ℝ] W →ₗ[ℝ] ℝ) (A : ConvexProcess U X) (B : ConvexProcess X Z) (hex : ∀ (w : W) (v : V), IsExactSum Bx (fun (x : X) => ⨅ u ∈ A.inv.eval x, ↑((Bu u) v)) fun (x : X) => -⨆ z ∈ B.eval x, ↑((Bz z) w)) : adjointProcess Bu Bz (B.comp A) = (adjointProcess Bu Bx A).comp (adjointProcess Bx Bz B)

The adjoint of a product is the product of the adjoints: (BA)* = A* B*.

Read directly this is a sandwich: (x*, u*) ∈ (BA)* says the concave x ↦ ⟨Bx, z*⟩ lies below the convex x ↦ ⟨u*, A⁻¹x⟩, and a factorisation through A* and B* is exactly a linear functional running between them, which exists_pairing_sandwich supplies.

Where the book assumes ri (range A) ∩ ri (dom B) ≠ ∅, the hypothesis here is that condition in IsExactSum form, one instance per (z*, u*) — the two effective domains involved are range A and dom B. As IsExactSum also requires both summands proper, it is stronger than the book's hypothesis.

The conjugate of an image under a convex process

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.indicatorBifun_inv {U : Type u_1} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) (x : X) (u : U) : A.inv.indicatorBifun x u = A.indicatorBifun u x

The indicator bifunction of A⁻¹ is the indicator bifunction of A read backwards: both values are δ(· | ·) of the same membership (u, x) ∈ graph A.

theorem Tdaf.ConvexAnalysis.ConvexProcess.coadjointProcess_inv {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) : coadjointProcess Bx Bu A.inv = (adjointProcess Bu Bx A).inv

(A⁻¹)* = A*⁻¹. The inverse of a supremum-oriented process is infimum oriented, so its adjoint is the coadjointProcess; with that reading the identity is an unfolding, both sides being {(v, y) | ⟨x, y⟩ ≤ ⟨u, v⟩ for every (u, x) ∈ graph A}.

theorem Tdaf.ConvexAnalysis.ConvexProcess.lowerAdjointBifun_indicatorBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) : lowerAdjointBifun Bu Bx A.indicatorBifun = (adjointProcess Bu Bx A).inv.indicatorBifun

The F⁎* entry of the process/bifunction dictionary: the lower adjoint of the indicator bifunction of A is the indicator bifunction of A*⁻¹.

This is adjointBifun_indicatorBifun with the two negations of lowerAdjointBifun cancelling against the negation the opposite orientation of A* puts on its indicator, and the reversal indicatorBifun_inv absorbing the transposition. It is the last thing (Af)* = A*⁻¹ f* needs.

theorem Tdaf.ConvexAnalysis.ConvexProcess.indicatorBifun_zero_zero_ne_top {U : Type u_1} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) : A.indicatorBifun 0 0 ≠ ⊤

The indicator bifunction of a convex process is finite at the origin, 0 being in A 0. This is the "finite somewhere" side condition the closed-image results ask of F.

theorem Tdaf.ConvexAnalysis.ConvexProcess.conj_imageBifun_indicatorBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) {f : U → EReal} (hf : Proper f) {y : Y} (hex : IsExactSum Bu f fun (u : U) => -bracket Bx A.indicatorBifun u y) : conj Bx (imageBifun A.indicatorBifun f) y = imageBifun (adjointProcess Bu Bx A).inv.indicatorBifun (conj Bu f) y

(Af)* = A*⁻¹ f*, where Af is the image Ff of f under the indicator bifunction F of A, i.e. (Af)(x) = inf {f u | x ∈ A u}.

This specialises the conjugate of an image under a bifunction; the only work is the dictionary lowerAdjointBifun_indicatorBifun. Rockafellar's ri (dom f) ∩ ri (dom A) ≠ ∅ becomes the IsExactSum of conj_imageBifun, dom F being dom A.

theorem Tdaf.ConvexAnalysis.ConvexProcess.exists_imageBifun_indicatorBifun_adjointProcess_eq {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) {f : U → EReal} (hf : Proper f) {y : Y} (hex : IsExactSum Bu f fun (u : U) => -bracket Bx A.indicatorBifun u y) : ∃ (v : V), conj Bu f v + (adjointProcess Bu Bx A).inv.indicatorBifun v y = imageBifun (adjointProcess Bu Bx A).inv.indicatorBifun (conj Bu f) y

The infimum defining (A*⁻¹ f*)(x*) is attained. This is exists_conj_imageBifun_eq read through the same dictionary.

Bounded values force a linear transformation

theorem Tdaf.ConvexAnalysis.ConvexProcess.eval_zero_eq_zero_of_isBounded {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] (A : ConvexProcess U X) (hb : Bornology.IsBounded (A.eval 0)) : A.eval 0 = {0}

A 0 is a convex cone containing the origin, so if it is bounded it is {0}.

theorem Tdaf.ConvexAnalysis.ConvexProcess.exists_eval_eq_singleton {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] (A : ConvexProcess U X) (hdom : A.dom = Set.univ) (hb : Bornology.IsBounded (A.eval 0)) (u : U) : ∃ (x : X), A.eval u = {x}

If A 0 is bounded and A has full domain, every value of A is a single point.

theorem Tdaf.ConvexAnalysis.ConvexProcess.exists_linearMap_of_isBounded {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] (A : ConvexProcess U X) (hdom : A.dom = Set.univ) (hb : Bornology.IsBounded (A.eval 0)) : ∃ (T : U →ₗ[ℝ] X), ∀ (u : U), A.eval u = {T u}

A convex process whose domain is everything and whose value at the origin is bounded is (the graph of) a linear transformation.

Linear transformations are exactly the convex processes all of whose values are nonempty and bounded; the converse direction is ConvexProcess.dom_ofLinearMap together with ConvexProcess.eval_ofLinearMap.

Closedness of the image

theorem Tdaf.ConvexAnalysis.ConvexProcess.isClosed_image {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {A : ConvexProcess U X} {C : Set U} (hA : IsClosed ↑A.graph) (hC : Convex ℝ C) (hC' : IsClosed C) (hCne : C.Nonempty) (h : ∀ (v : U), (v, 0) ∈ A.graph → v ∈ recessionCone C → v = 0) : IsClosed (A.image C)

If A is a closed convex process, C is a nonempty closed convex set, and no non-zero vector of A⁻¹ 0 recedes C, then A C is closed. In particular this holds when C is bounded, since then 0⁺C = {0}.

This is the recession-cone criterion for a linear image, at the projection (u, x) ↦ x: A C is the image of graph A ∩ (C × X), whose recession cone is graph A ∩ (0⁺C × X) — the graph is its own recession cone, being a pointed convex cone — and whose intersection with the kernel of the projection is {(v, 0) | v ∈ A⁻¹ 0 ∩ 0⁺C}. No duality is needed.

theorem Tdaf.ConvexAnalysis.ConvexProcess.isClosed_image_of_isBounded {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {A : ConvexProcess U X} {C : Set U} (hA : IsClosed ↑A.graph) (hC : Convex ℝ C) (hC' : IsClosed C) (hCne : C.Nonempty) (hb : Bornology.IsBounded C) : IsClosed (A.image C)

The image of a nonempty compact convex set under a closed convex process is closed, the bounded case of isClosed_image.

The reflected process, and the dictionary between the two orientations

def Tdaf.ConvexAnalysis.ConvexProcess.reflect {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) : ConvexProcess U X

The reflection of a convex process: the process whose graph is the reflection of graph A through the origin, so that (A.reflect) u = -(A (-u)).

Reflection is what exchanges the two orientations: reversing the inequality in the definition of the adjoint is the same as reflecting the graph, so adjointProcess Bu Bx A.reflect = coadjointProcess Bu Bx A (adjointProcess_reflect). Read the other way round (coadjointProcess_eq_reflect_adjointProcess) it puts the reflection on the conclusion, where reflect_add and reflect_comp cancel it, so the infimum-oriented mirrors carry the supremum-oriented hypotheses unchanged.

Equations

• A.reflect = { graph := { carrier := {p : U × X | -p ∈ A.graph}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ } }

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.mem_graph_reflect {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {A : ConvexProcess U X} {p : U × X} : p ∈ A.reflect.graph ↔ -p ∈ A.graph

theorem Tdaf.ConvexAnalysis.ConvexProcess.reflect_involutive {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] : Function.Involutive reflect

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.reflect_reflect {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) : A.reflect.reflect = A

theorem Tdaf.ConvexAnalysis.ConvexProcess.reflect_injective {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] : Function.Injective reflect

theorem Tdaf.ConvexAnalysis.ConvexProcess.eval_reflect {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) (u : U) : A.reflect.eval u = -A.eval (-u)

theorem Tdaf.ConvexAnalysis.ConvexProcess.reflect_add {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A₁ A₂ : ConvexProcess U X) : (A₁ + A₂).reflect = A₁.reflect + A₂.reflect

theorem Tdaf.ConvexAnalysis.ConvexProcess.reflect_comp {U : Type u_1} {X : Type u_2} {Z : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Z] [Module ℝ Z] (B : ConvexProcess X Z) (A : ConvexProcess U X) : (B.comp A).reflect = B.reflect.comp A.reflect

def Tdaf.ConvexAnalysis.ConvexProcess.reflectAut {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] : AddAut (ConvexProcess U X)

Reflection bundled: an additive automorphism of the convex processes from U to X.

It is involutive (reflect_involutive) and additive (reflect_add), so .injective, .eq_iff and .toPerm come from the bundled form instead of being re-proved.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.reflectAut_apply {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (A : ConvexProcess U X) : reflectAut A = A.reflect

theorem Tdaf.ConvexAnalysis.ConvexProcess.adjointProcess_reflect {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) : adjointProcess Bu Bx A.reflect = coadjointProcess Bu Bx A

Reversing the inequality is reflecting the graph: the supremum-oriented adjoint of the reflected process is the infimum-oriented adjoint of the original one.

theorem Tdaf.ConvexAnalysis.ConvexProcess.coadjointProcess_reflect {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) : coadjointProcess Bu Bx A.reflect = adjointProcess Bu Bx A

The mirror of adjointProcess_reflect: reflection also carries the infimum-oriented adjoint back to the supremum-oriented one.

theorem Tdaf.ConvexAnalysis.ConvexProcess.coadjointProcess_eq_reflect_adjointProcess {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) : coadjointProcess Bu Bx A = (adjointProcess Bu Bx A).reflect

The infimum-oriented adjoint is the reflection of the supremum-oriented one. Together with adjointProcess_reflect this is the whole content of "the adjoint of an infimum-oriented process is defined in the same way, except that the inequality is reversed".

theorem Tdaf.ConvexAnalysis.ConvexProcess.isClosed_graph_reflect {U : Type u_1} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [TopologicalSpace U] [IsTopologicalAddGroup U] [TopologicalSpace X] [IsTopologicalAddGroup X] {A : ConvexProcess U X} (hA : IsClosed ↑A.graph) : IsClosed ↑A.reflect.graph

Reflection preserves closedness: it is a preimage under the homeomorphism p ↦ -p.

theorem Tdaf.ConvexAnalysis.ConvexProcess.isClosed_graph_coadjointProcess {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace V] [IsTopologicalAddGroup V] [TopologicalSpace Y] [IsTopologicalAddGroup Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsContinuousPairing Bu.flip] [IsContinuousPairing Bx.flip] (A : ConvexProcess U X) : IsClosed ↑(coadjointProcess Bu Bx A).graph

The adjoint of an infimum-oriented convex process is closed, as in the supremum-oriented case.

theorem Tdaf.ConvexAnalysis.ConvexProcess.graph_adjointProcess_coadjointProcess_eq_closure {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [TopologicalSpace X] [IsTopologicalAddGroup U] [IsTopologicalAddGroup X] [ContinuousSMul ℝ U] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ U] [LocallyConvexSpace ℝ X] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bx] (A : ConvexProcess U X) : ↑(adjointProcess Bx.flip Bu.flip (coadjointProcess Bu Bx A)).graph = closure ↑A.graph

Taking the infimum-oriented adjoint and then the supremum-oriented one also returns cl A.

This is graph_coadjointProcess_adjointProcess_eq_closure read through adjointProcess_reflect; the two sign flips still cancel, and it is what turns the closed halves of the sum and product theorems into corollaries of their open halves.

theorem Tdaf.ConvexAnalysis.ConvexProcess.adjointProcess_coadjointProcess_eq_self_iff {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [TopologicalSpace X] [IsTopologicalAddGroup U] [IsTopologicalAddGroup X] [ContinuousSMul ℝ U] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ U] [LocallyConvexSpace ℝ X] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bx] (A : ConvexProcess U X) : adjointProcess Bx.flip Bu.flip (coadjointProcess Bu Bx A) = A ↔ IsClosed ↑A.graph

A convex process is closed exactly when the supremum-oriented adjoint of its infimum-oriented adjoint is itself.

Sums and products for infimum-oriented processes

theorem Tdaf.ConvexAnalysis.ConvexProcess.coadjointProcess_add {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A₁ A₂ : ConvexProcess U X) (hex : ∀ (y : Y), IsExactSum Bu (fun (u : U) => -supportFn Bx (A₁.eval u) y) fun (u : U) => -supportFn Bx (A₂.eval u) y) : coadjointProcess Bu Bx (A₁ + A₂) = coadjointProcess Bu Bx A₁ + coadjointProcess Bu Bx A₂

The adjoint of a sum, for two infimum-oriented processes: (A₁ + A₂)* = A₁* + A₂*.

Rockafellar states the result for two processes "with the same orientation" and leaves the infimum-oriented case implicit. It is the supremum-oriented theorem read through coadjointProcess_eq_reflect_adjointProcess, reflection distributing over sums; the hypothesis is adjointProcess_add's own, verbatim.

theorem Tdaf.ConvexAnalysis.ConvexProcess.coadjointProcess_comp {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} {Z : Type u_5} {W : Type u_6} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [AddCommGroup Z] [Module ℝ Z] [AddCommGroup W] [Module ℝ W] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (Bz : Z →ₗ[ℝ] W →ₗ[ℝ] ℝ) (A : ConvexProcess U X) (B : ConvexProcess X Z) (hex : ∀ (w : W) (v : V), IsExactSum Bx (fun (x : X) => ⨅ u ∈ A.inv.eval x, ↑((Bu u) v)) fun (x : X) => -⨆ z ∈ B.eval x, ↑((Bz z) w)) : coadjointProcess Bu Bz (B.comp A) = (coadjointProcess Bu Bx A).comp (coadjointProcess Bx Bz B)

The adjoint of a product, for two infimum-oriented processes: (BA)* = A* B*.

Like coadjointProcess_add, this reflects the adjoints rather than the processes, so the hypothesis is adjointProcess_comp's own; reflect_comp is what makes the product come out in the same order.

The closed halves of the sum and product theorems

theorem Tdaf.ConvexAnalysis.ConvexProcess.add_eq_coadjointProcess_add {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bx] {A₁ A₂ : ConvexProcess U X} (hA₁ : IsClosed ↑A₁.graph) (hA₂ : IsClosed ↑A₂.graph) (hex : ∀ (u : U), IsExactSum Bx.flip (fun (y : Y) => -supportFn Bu.flip ((adjointProcess Bu Bx A₁).eval y) u) fun (y : Y) => -supportFn Bu.flip ((adjointProcess Bu Bx A₂).eval y) u) : A₁ + A₂ = coadjointProcess Bx.flip Bu.flip (adjointProcess Bu Bx A₁ + adjointProcess Bu Bx A₂)

The sum of two closed convex processes is the infimum-oriented adjoint of the sum of their adjoints, provided the two adjoints add exactly. This is the identity both closed-half results about sums come from.

theorem Tdaf.ConvexAnalysis.ConvexProcess.isClosed_graph_add {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bx] {A₁ A₂ : ConvexProcess U X} (hA₁ : IsClosed ↑A₁.graph) (hA₂ : IsClosed ↑A₂.graph) (hex : ∀ (u : U), IsExactSum Bx.flip (fun (y : Y) => -supportFn Bu.flip ((adjointProcess Bu Bx A₁).eval y) u) fun (y : Y) => -supportFn Bu.flip ((adjointProcess Bu Bx A₂).eval y) u) : IsClosed ↑(A₁ + A₂).graph

The sum of two closed convex processes is closed. It is an adjoint, and an adjoint is always closed.

theorem Tdaf.ConvexAnalysis.ConvexProcess.graph_adjointProcess_add_eq_closure {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] [LocallyConvexSpace ℝ V] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bx] [IsCompatiblePairing Bu.flip] [IsCompatiblePairing Bx.flip] {A₁ A₂ : ConvexProcess U X} (hA₁ : IsClosed ↑A₁.graph) (hA₂ : IsClosed ↑A₂.graph) (hex : ∀ (u : U), IsExactSum Bx.flip (fun (y : Y) => -supportFn Bu.flip ((adjointProcess Bu Bx A₁).eval y) u) fun (y : Y) => -supportFn Bu.flip ((adjointProcess Bu Bx A₂).eval y) u) : ↑(adjointProcess Bu Bx (A₁ + A₂)).graph = closure ↑(adjointProcess Bu Bx A₁ + adjointProcess Bu Bx A₂).graph

(A₁ + A₂)* is the closure of A₁* + A₂*, for closed A₁ and A₂.

theorem Tdaf.ConvexAnalysis.ConvexProcess.comp_eq_coadjointProcess_comp {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} {Z : Type u_5} {W : Type u_6} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [AddCommGroup Z] [Module ℝ Z] [AddCommGroup W] [Module ℝ W] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [TopologicalSpace Z] [IsTopologicalAddGroup Z] [ContinuousSMul ℝ Z] [LocallyConvexSpace ℝ Z] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (Bz : Z →ₗ[ℝ] W →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bx] [IsCompatiblePairing Bz] {A : ConvexProcess U X} {B : ConvexProcess X Z} (hA : IsClosed ↑A.graph) (hB : IsClosed ↑B.graph) (hex : ∀ (u : U) (z : Z), IsExactSum Bx.flip (fun (y : Y) => ⨅ w ∈ (adjointProcess Bx Bz B).inv.eval y, ↑((Bz z) w)) fun (y : Y) => -⨆ v ∈ (adjointProcess Bu Bx A).eval y, ↑((Bu u) v)) : B.comp A = coadjointProcess Bz.flip Bu.flip ((adjointProcess Bu Bx A).comp (adjointProcess Bx Bz B))

The product of two closed convex processes is the infimum-oriented adjoint of the product of their adjoints. This is the identity both closed-half results about products come from.

theorem Tdaf.ConvexAnalysis.ConvexProcess.isClosed_graph_comp {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} {Z : Type u_5} {W : Type u_6} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [AddCommGroup Z] [Module ℝ Z] [AddCommGroup W] [Module ℝ W] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [TopologicalSpace Z] [IsTopologicalAddGroup Z] [ContinuousSMul ℝ Z] [LocallyConvexSpace ℝ Z] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (Bz : Z →ₗ[ℝ] W →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bx] [IsCompatiblePairing Bz] {A : ConvexProcess U X} {B : ConvexProcess X Z} (hA : IsClosed ↑A.graph) (hB : IsClosed ↑B.graph) (hex : ∀ (u : U) (z : Z), IsExactSum Bx.flip (fun (y : Y) => ⨅ w ∈ (adjointProcess Bx Bz B).inv.eval y, ↑((Bz z) w)) fun (y : Y) => -⨆ v ∈ (adjointProcess Bu Bx A).eval y, ↑((Bu u) v)) : IsClosed ↑(B.comp A).graph

The product of two closed convex processes is closed.

theorem Tdaf.ConvexAnalysis.ConvexProcess.graph_adjointProcess_comp_eq_closure {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} {Z : Type u_5} {W : Type u_6} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [AddCommGroup Z] [Module ℝ Z] [AddCommGroup W] [Module ℝ W] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [TopologicalSpace Z] [IsTopologicalAddGroup Z] [ContinuousSMul ℝ Z] [LocallyConvexSpace ℝ Z] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] [LocallyConvexSpace ℝ V] [TopologicalSpace W] [IsTopologicalAddGroup W] [ContinuousSMul ℝ W] [LocallyConvexSpace ℝ W] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (Bz : Z →ₗ[ℝ] W →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bx] [IsCompatiblePairing Bz] [IsCompatiblePairing Bu.flip] [IsCompatiblePairing Bz.flip] {A : ConvexProcess U X} {B : ConvexProcess X Z} (hA : IsClosed ↑A.graph) (hB : IsClosed ↑B.graph) (hex : ∀ (u : U) (z : Z), IsExactSum Bx.flip (fun (y : Y) => ⨅ w ∈ (adjointProcess Bx Bz B).inv.eval y, ↑((Bz z) w)) fun (y : Y) => -⨆ v ∈ (adjointProcess Bu Bx A).eval y, ↑((Bu u) v)) : ↑(adjointProcess Bu Bz (B.comp A)).graph = closure ↑((adjointProcess Bu Bx A).comp (adjointProcess Bx Bz B)).graph

(BA)* is the closure of A* B*, for closed A and B.

The two inner products for infimum-oriented processes

For an infimum-oriented process the indicator bifunction is the concave function -δ(· | A u), and the inner product ⟨Au, x*⟩ is its concave conjugate: an infimum over A u rather than a supremum. As with adjointProcess/coadjointProcess, the two orientations are separate definitions rather than two branches of one flag, and the whole mirror is driven by the single sign dictionary coBracket_eq_neg_bracket.

noncomputable def Tdaf.ConvexAnalysis.ConvexProcess.coBracket {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) (u : U) (y : Y) : EReal

The inner product ⟨Au, x*⟩ of an infimum-oriented convex process: ⟨Au, x*⟩ = inf {⟨x, x*⟩ | x ∈ A u}.

This is the concave conjugate of the concave indicator -δ(· | A u), exactly as bracket _ A.indicatorBifun u is the convex conjugate of δ(· | A u).

Equations

• Tdaf.ConvexAnalysis.ConvexProcess.coBracket Bx A u y = ⨅ x ∈ A.eval u, ↑((Bx x) y)

theorem Tdaf.ConvexAnalysis.ConvexProcess.coBracket_apply {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) (u : U) (y : Y) : coBracket Bx A u y = ⨅ x ∈ A.eval u, ↑((Bx x) y)

The first of the two extremum problems, in infimum-oriented form: ⟨Au, x*⟩ = inf {⟨x, x*⟩ | x ∈ A u}.

theorem Tdaf.ConvexAnalysis.ConvexProcess.coBracket_eq_neg_bracket {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) (u : U) (y : Y) : coBracket Bx A u y = -bracket Bx A.indicatorBifun u (-y)

The sign dictionary between the two orientations: the infimum-oriented inner product is minus the supremum-oriented one, read at the reflected dual vector. Note that only the dual variable is reflected — the primal variable u is untouched, because reversing the orientation of a process does not reverse its argument.

theorem Tdaf.ConvexAnalysis.ConvexProcess.coBracket_eq_neg_bracket_fun {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) (y : Y) : (fun (u : U) => coBracket Bx A u y) = fun (u : U) => -bracket Bx A.indicatorBifun u (-y)

theorem Tdaf.ConvexAnalysis.ConvexProcess.coBracket_eq_neg_supportFn {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) (u : U) (y : Y) : coBracket Bx A u y = -supportFn Bx (A.eval u) (-y)

The infimum-oriented inner product is minus a support function, read at the reflected dual vector.

theorem Tdaf.ConvexAnalysis.ConvexProcess.neg_coBracket_eq_compLin {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) (u : U) : (fun (y : Y) => -coBracket Bx A u y) = compLin (bracket Bx A.indicatorBifun u) (-LinearMap.id)

The negative of ⟨Au, ·⟩ is the supremum-oriented inner product composed with the linear reflection x* ↦ -x*. This is the form in which the sign dictionary feeds the convexity and closedness lemmas for a composition with a linear map.

theorem Tdaf.ConvexAnalysis.ConvexProcess.posHomogeneous_coBracket {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) (u : U) : PosHomogeneous (coBracket Bx A u)

⟨Au, ·⟩ is positively homogeneous, in the infimum-oriented mirror.

theorem Tdaf.ConvexAnalysis.ConvexProcess.concaveFn_coBracket {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) (u : U) : ConcaveFn (coBracket Bx A u)

⟨Au, ·⟩ is concave in the infimum-oriented mirror, being a concave conjugate.

theorem Tdaf.ConvexAnalysis.ConvexProcess.posHomogeneous_coBracket_arg {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) (y : Y) : PosHomogeneous fun (u : U) => coBracket Bx A u y

⟨A ·, x*⟩ is positively homogeneous, in the infimum-oriented mirror.

theorem Tdaf.ConvexAnalysis.ConvexProcess.convexFn_coBracket_arg {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) (y : Y) : ConvexFn fun (u : U) => coBracket Bx A u y

⟨A ·, x*⟩ is convex in the infimum-oriented mirror, where in the supremum-oriented case it is concave. Reversing the orientation of a process exchanges convexity and concavity in both variables at once.

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.coBracket_zero_zero {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) : coBracket Bx A 0 0 = 0

The inner product vanishes at the origin, in the infimum-oriented mirror.

theorem Tdaf.ConvexAnalysis.ConvexProcess.closedConcaveFn_coBracket {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace Y] [IsTopologicalAddGroup Y] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsContinuousPairing Bx.flip] (A : ConvexProcess U X) (u : U) : ClosedConcaveFn (coBracket Bx A u)

⟨Au, ·⟩ is a closed concave function in the infimum-oriented mirror, the reflection x* ↦ -x* being a homeomorphism.

theorem Tdaf.ConvexAnalysis.ConvexProcess.iSup_coadjointProcess_eq_neg_concaveBracket {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) (u : U) (y : Y) : ⨆ v ∈ (coadjointProcess Bu Bx A).eval y, ↑((Bu u) v) = -concaveBracket Bu (adjointBifun Bu Bx A.indicatorBifun) u (-y)

The second of the two extremum problems, in infimum-oriented form: ⟨u, A* x*⟩ = sup {⟨u, u*⟩ | u* ∈ A* x*}, where A* is now the infimum-oriented adjoint coadjointProcess, whose values are the reflections of those of adjointProcess.

theorem Tdaf.ConvexAnalysis.ConvexProcess.iSup_coadjointProcess_eq_clFn {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} (A : ConvexProcess U X) (y : Y) : (fun (u : U) => ⨆ v ∈ (coadjointProcess Bu Bx A).eval y, ↑((Bu u) v)) = fun (u : U) => clFn (fun (u' : U) => coBracket Bx A u' y) u

⟨u, A* x*⟩ = cl_u ⟨Au, x*⟩, the infimum-oriented mirror.

The closure is now the ordinary convex closure clFn, because ⟨A ·, x*⟩ is convex rather than concave (convexFn_coBracket_arg); in the supremum-oriented statement concaveBracket_adjointBifun_indicatorBifun_eq_partialCl₁ it is the concave closure clConcave packaged as partialCl₁. As there, closedness of A plays no part.