The two inner products of a convex process

A convex process A carries two inner products,

⟨Au, x*⟩ = sup {⟨x, x*⟩ | x ∈ A u} and ⟨u, A* x*⟩ = inf {⟨u, u*⟩ | u* ∈ A* x*},

the first a maximisation over a value of A, the second a minimisation over a value of A*. They are the bracket and the concave bracket of the indicator bifunction of A and of its adjoint, so everything that separates them is a partial closure. Bifunction/Process.lean proves the clauses needing only the closure in u; this module adds those needing the closure in x* — where closedness of A enters — and those needing relative interiors.

Main results

• ConvexProcess.closedBifun_indicatorBifun_iff — A is a closed convex process exactly when its indicator bifunction is closed. domConcaveBifun_adjointBifun_indicatorBifun: dom F* = dom A*.
• ConvexProcess.partialCl₂_concaveBracket_adjointBifun_indicatorBifun — ⟨Au, x*⟩ = cl_{x*} ⟨u, A* x*⟩ for a closed convex process.
• ConvexProcess.bracket_eq_concaveBracket_of_mem_relint_dom and …_of_mem_relint_dom_adjoint — ⟨Au, x*⟩ = ⟨u, A* x*⟩ whenever u ∈ ri (dom A) or x* ∈ ri (dom A*) (Theorem 39.3 in [^1]); bracket_eq_concaveBracket_adjointBifun_of_mem_relint_domConcaveBifun is the dual half of that, for a general closed convex bifunction.
• exists_unique_convexProcess_bracket_indicatorBifun_eq — a lower closed concave-convex K with K (0, 0) = 0 that is positively homogeneous in each variable separately is ⟨Au, x*⟩ for exactly one closed convex process A (Theorem 39.4 in [^1]). ConvexProcess.isClosed_eval and the …_bracket_indicatorBifun results beside it are the four properties it inverts.
• ConvexProcess.closedFn_imageBifun_indicatorBifun and the results beside it — for a closed convex process A and a closed proper convex f, the image Af is closed, the infimum defining (Af)(x) is attained, and (Af)* = cl (A*⁻¹ f*). The open half is in Bifunction/Process.lean.

Implementation notes

Rockafellar prefixes both halves of the last assertion with "if A is closed", but the u half needs only that a concave function agrees with its concave closure on the relative interior of its effective domain. Closedness is genuinely needed only on the x* side, where the closure in x* — which rests on F** = cl F — identifies cl_{x*} ⟨u, A* x*⟩ with ⟨Au, x*⟩; there it is Y, not U, that must be finite-dimensional.

A process is closed exactly when its indicator bifunction is, since cl δ(· | S) = δ(· | cl S). That is what lets the bifunction theorems be read for processes without a separate closedness argument. The correspondence is stated as a ∃! with closedness inside it: it is between closed convex processes and kernels, so uniqueness is uniqueness among closed processes.

References

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

Closedness, and the effective domain of the adjoint

theorem Tdaf.ConvexAnalysis.ConvexProcess.closedBifun_indicatorBifun_iff {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [TopologicalSpace U] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] (A : ConvexProcess U X) : ClosedBifun A.indicatorBifun ↔ IsClosed ↑A.graph

A convex process is closed exactly when its indicator bifunction is a closed convex bifunction: ClosedBifun for an indicator bifunction is closure (graph A) = graph A.

theorem Tdaf.ConvexAnalysis.ConvexProcess.isClosed_eval {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [TopologicalSpace U] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] {A : ConvexProcess U X} (hA : IsClosed ↑A.graph) (u : U) : IsClosed (A.eval u)

Every value of a closed convex process is a closed set: A u is the preimage of the graph under the continuous map x ↦ (u, x).

@[simp]

theorem Tdaf.ConvexAnalysis.ConvexProcess.domConcaveBifun_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) : domConcaveBifun (adjointBifun Bu Bx A.indicatorBifun) = (adjointProcess Bu Bx A).dom

The concave effective domain of the adjoint of an indicator bifunction is the effective domain of the adjoint process: ⟨u, A* x*⟩ is +∞ exactly where A* x* is empty.

The two inner products for a closed convex process

theorem Tdaf.ConvexAnalysis.ConvexProcess.partialCl₂_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] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (A : ConvexProcess U X) (hA : IsClosed ↑A.graph) : (partialCl₂ fun (p : U × Y) => concaveBracket Bu (adjointBifun Bu Bx A.indicatorBifun) p.1 p.2) = fun (p : U × Y) => bracket Bx A.indicatorBifun p.1 p.2

For a closed convex process, ⟨Au, x*⟩ = cl_{x*} ⟨u, A* x*⟩.

This is the closure in x*, which is where closedness enters: it runs through F** = cl F = F, whereas the closure in u, ⟨u, A* x*⟩ = cl_u ⟨Au, x*⟩ (concaveBracket_adjointBifun_indicatorBifun_eq_partialCl₁), holds for every convex process.

Where the two brackets of a bifunction agree, on the dual side

theorem Tdaf.ConvexAnalysis.bracket_eq_concaveBracket_adjointBifun_of_mem_relint_domConcaveBifun {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] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] {F : Bifun U X} (hF : ConvexBifun F) (hcl : ClosedBifun F) (u : U) {y : Y} (hy : y ∈ intrinsicInterior ℝ (domConcaveBifun (adjointBifun Bu Bx F))) : bracket Bx F u y = concaveBracket Bu (adjointBifun Bu Bx F) u y

For a closed convex bifunction the two brackets ⟨Fu, y⟩ and ⟨u, F* y⟩ already agree at every relative interior point of dom F*.

The two differ by the convex closure in y; ⟨u, F*·⟩ is convex with effective domain dom F*, and a convex function agrees with its closure on the relative interior of its effective domain. It is Y, not U, that must be finite-dimensional.

Where the two inner products agree

theorem Tdaf.ConvexAnalysis.ConvexProcess.bracket_eq_concaveBracket_of_mem_relint_dom {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} (A : ConvexProcess U X) {u : U} (hu : u ∈ intrinsicInterior ℝ A.dom) (y : Y) : bracket Bx A.indicatorBifun u y = concaveBracket Bu (adjointBifun Bu Bx A.indicatorBifun) u y

⟨Au, x*⟩ = ⟨u, A* x*⟩ at every relative interior point of dom A.

Rockafellar prefixes the assertion with "if A is closed"; no closedness is needed here, the statement being bracket_eq_concaveBracket_adjointBifun_of_mem_relint for the indicator bifunction.

theorem Tdaf.ConvexAnalysis.ConvexProcess.bracket_eq_concaveBracket_of_mem_relint_dom_adjoint {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] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (A : ConvexProcess U X) (hA : IsClosed ↑A.graph) (u : U) {y : Y} (hy : y ∈ intrinsicInterior ℝ (adjointProcess Bu Bx A).dom) : bracket Bx A.indicatorBifun u y = concaveBracket Bu (adjointBifun Bu Bx A.indicatorBifun) u y

For a closed convex process, ⟨Au, x*⟩ = ⟨u, A* x*⟩ at every relative interior point of dom A*, and for every u.

Unlike the u side, this one really does need A closed: it goes through the closure in x*.

Which saddle-functions are inner products of processes

The lower closed concave-convex functions on U × Y match the closed convex bifunctions from U to X. Cutting that down to processes costs exactly two further conditions on K: it vanishes at the origin, and it is positively homogeneous in each variable separately.

theorem Tdaf.ConvexAnalysis.ConvexProcess.concaveConvexFn_bracket_indicatorBifun {U : Type u_1} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (A : ConvexProcess U X) : ConcaveConvexFn fun (p : U × Y) => bracket Bx A.indicatorBifun p.1 p.2

The inner product of a convex process is concave-convex.

theorem Tdaf.ConvexAnalysis.ConvexProcess.lowerClosedFn_bracket_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] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (A : ConvexProcess U X) (hA : IsClosed ↑A.graph) : LowerClosedFn fun (p : U × Y) => bracket Bx A.indicatorBifun p.1 p.2

The inner product of a closed convex process is lower closed. This is the saddle-function correspondence read at the indicator bifunction.

theorem Tdaf.ConvexAnalysis.ConvexProcess.eval_eq_supportSet_bracket_indicatorBifun {U : Type u_1} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] (A : ConvexProcess U X) (hA : IsClosed ↑A.graph) (u : U) : A.eval u = supportSet Bx.flip (bracket Bx A.indicatorBifun u)

A closed convex process is recovered from its inner product by A u = {x | ⟨x, x*⟩ ≤ K (u, x*) for every x*}.

This is the recovery of a closed convex set from its support function, at A u, whose support function is ⟨Au, ·⟩ (bracket_indicatorBifun).

theorem Tdaf.ConvexAnalysis.exists_unique_convexProcess_bracket_indicatorBifun_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] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] {K : U × Y → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hK : ConcaveConvexFn K) (hlc : LowerClosedFn K) (hK₀ : K (0, 0) = 0) (hhu : ∀ (y : Y), PosHomogeneous fun (u : U) => K (u, y)) (hhy : ∀ (u : U), PosHomogeneous fun (y : Y) => K (u, y)) : ∃! A : ConvexProcess U X, IsClosed ↑A.graph ∧ (fun (p : U × Y) => bracket Bx A.indicatorBifun p.1 p.2) = K

K (u, x*) = ⟨Au, x*⟩ is a one-to-one correspondence between the closed convex processes from U to X and the lower closed concave-convex functions on U × Y that vanish at the origin and are positively homogeneous in each variable separately. The inverse map is A u = {x | ⟨x, x*⟩ ≤ K (u, x*) for every x*} (ConvexProcess.eval_eq_supportSet_bracket_indicatorBifun).

The saddle-function correspondence does all the work on the bifunction side; what remains is that the closed convex bifunction it produces is an indicator bifunction. K (0, 0) = 0 bounds F 0 below by 0 and makes it finite somewhere, so the closed convex graphFn F cannot take -∞, and no slice K (u, ·) is identically +∞. The conjugate of a positively homogeneous function that is not identically +∞ is an indicator function, so each F u is one; positive homogeneity in u makes the resulting set a cone, its convexity coming from convexity of F.

The image under a closed convex process

theorem Tdaf.ConvexAnalysis.ConvexProcess.closedFn_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] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] {A : ConvexProcess U X} {f : U → EReal} (hA : IsClosed ↑A.graph) (hf : ClosedProperConvexFn f) (hex : ∀ (x : X), IsExactSum Bu.flip (conj Bu f) fun (v : V) => -bracket Bx.flip (adjointProcess Bu Bx A).inv.indicatorBifun v x) : ClosedFn (imageBifun A.indicatorBifun f)

For a closed convex process A and a closed proper convex f, the image Af is closed.

This is closedFn_imageBifun at the indicator bifunction of A, the closedness hypothesis passing through closedBifun_indicatorBifun_iff and the "finite somewhere" side condition being 0 ∈ A 0. Rockafellar's hypothesis ri (dom f*) ∩ ri (dom A*⁻¹) ≠ ∅ is the IsExactSum there, one instance per x; dom A*⁻¹ is range A*.

theorem Tdaf.ConvexAnalysis.ConvexProcess.exists_imageBifun_indicatorBifun_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] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] {A : ConvexProcess U X} {f : U → EReal} (hA : IsClosed ↑A.graph) (hf : ClosedProperConvexFn f) {x : X} (hex : IsExactSum Bu.flip (conj Bu f) fun (v : V) => -bracket Bx.flip (adjointProcess Bu Bx A).inv.indicatorBifun v x) : ∃ (u : U), f u + A.indicatorBifun u x = imageBifun A.indicatorBifun f x

The infimum defining (Af)(x) is attained, in the raw form ∃ u, f u + δ(x | A u) = (Af)(x).

theorem Tdaf.ConvexAnalysis.ConvexProcess.exists_mem_eval_and_eq_imageBifun {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 →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] {A : ConvexProcess U X} {f : U → EReal} (hA : IsClosed ↑A.graph) (hf : ClosedProperConvexFn f) {x : X} (hex : IsExactSum Bu.flip (conj Bu f) fun (v : V) => -bracket Bx.flip (adjointProcess Bu Bx A).inv.indicatorBifun v x) (hne : imageBifun A.indicatorBifun f x ≠ ⊤) : ∃ (u : U), x ∈ A.eval u ∧ f u = imageBifun A.indicatorBifun f x

Wherever Af is finite, the infimum inf {f u | x ∈ A u} is attained at an actual u with x ∈ A u.

The raw form exists_imageBifun_indicatorBifun_eq produces a u with f u + δ(x | A u) = (Af)(x); the indicator is 0 or ⊤, and ⊤ is excluded because f u ≠ ⊥ would then force (Af)(x) = ⊤.

theorem Tdaf.ConvexAnalysis.ConvexProcess.conj_imageBifun_indicatorBifun_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] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] {A : ConvexProcess U X} {f : U → EReal} [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] [IsCompatiblePairing Bx.flip] (hA : IsClosed ↑A.graph) (hf : ClosedProperConvexFn f) (hex : ∀ (x : X), IsExactSum Bu.flip (conj Bu f) fun (v : V) => -bracket Bx.flip (adjointProcess Bu Bx A).inv.indicatorBifun v x) : conj Bx (imageBifun A.indicatorBifun f) = clFn (imageBifun (adjointProcess Bu Bx A).inv.indicatorBifun (conj Bu f))

(Af)* = cl (A*⁻¹ f*), for a closed convex process and a closed proper convex f.