Adjoint bifunctions and dual programs

The adjoint of a convex bifunction F : U → X → EReal is the concave bifunction

(F* y)(v) = ⨅ (u, x) {F u x - ⟨x, y⟩ + ⟨u, v⟩},

and the concave program (P*) dual to (P) is "maximise F* 0 over V". Everything here follows from one computation: F* is the conjugate of the graph function of F, negated and read at the reflected point (-v, y). So F* is closed concave with no hypothesis on F, F** = cl F, and the dual objective is the concave conjugate of -inf F. The same view shows that cl F is computed slice by slice on ri (dom F), and that closing a strongly consistent program changes neither its value, its solutions, nor its Kuhn–Tucker vectors.

Main definitions

• adjointBifun Bu Bx F, concaveAdjointBifun Bu Bx G — the adjoint of a convex bifunction, and of a concave one (the same formula with a supremum).
• ConcaveBifun, ClosedBifun, ImageClosedBifun — the graph function is concave, it is closed, the slices F u are each closed; clBifun F is the closure of the graph function.

Main results

• adjointBifun_eq_neg_conj_graphFn — the computation above; concaveFn_graphFn_adjointBifun, closedConcaveFn_graphFn_adjointBifun, concaveAdjointBifun_adjointBifun_eq_clBifun, properConcave_graphFn_adjointBifun_iff — F* is closed concave, F** = cl F, and F* is proper exactly when F is (Theorem 30.1 in [^1]).
• adjointBifun_zero_eq_concaveConj — the dual objective as a concave conjugate; adjointBifun_zero_le — weak duality.
• mem_kuhnTucker_iff_adjointBifun_zero_eq — the Kuhn–Tucker vectors are the points where the dual objective attains the optimal value, with no normality needed.
• clBifun_apply_eq_clFn, infBifun_clBifun_eq and the two domBifun inclusions — the closure of a bifunction, slice by slice (Theorem 29.4 in [^1]).

Implementation notes

The sign flip is carried in the argument rather than in a reflected pairing: ⟨u, -v⟩ + ⟨x, y⟩ is read as the pairing of (u, x) with (-v, y), so F* is conj at a reflected point and conj's own lemmas apply verbatim. The two real terms are grouped inside one coercion, so no ∞ - ∞ can arise, and the dual objective uses the concave conjugate, since g* ≠ -(-g)*. The closedness of F* asks for IsContinuousPairing (prodPairing Bu Bx).flip rather than the un-flipped class: closedFn_conj needs continuity on the side the conjugate lives on, and the un-flipped form would demand a topology on U × X that this development never supplies.

References

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

noncomputable def Tdaf.ConvexAnalysis.adjointBifun {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 →ₗ[ℝ] ℝ) (F : Bifun U X) : Bifun Y V

The adjoint of a convex bifunction: (F* y)(v) = ⨅ (u, x) {F u x - ⟨x, y⟩ + ⟨u, v⟩}, a concave bifunction from Y to V.

Equations

• Tdaf.ConvexAnalysis.adjointBifun Bu Bx F y v = ⨅ (p : U × X), F p.1 p.2 + ↑((Bu p.1) v - (Bx p.2) y)

theorem Tdaf.ConvexAnalysis.adjointBifun_apply {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 →ₗ[ℝ] ℝ) (F : Bifun U X) (y : Y) (v : V) : adjointBifun Bu Bx F y v = ⨅ (p : U × X), F p.1 p.2 + ↑((Bu p.1) v - (Bx p.2) y)

theorem Tdaf.ConvexAnalysis.adjointBifun_eq_neg_conj_graphFn {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 →ₗ[ℝ] ℝ) (F : Bifun U X) (y : Y) (v : V) : adjointBifun Bu Bx F y v = -conj (prodPairing Bu Bx) (graphFn F) (-v, y)

The computation everything here rests on: the adjoint is the conjugate of the graph function, negated and evaluated at a reflected point.

The adjoint is a closed concave bifunction

def Tdaf.ConvexAnalysis.ConcaveBifun {U : Type u_1} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (G : Bifun U X) : Prop

A bifunction is concave when its graph function is.

Equations

• Tdaf.ConvexAnalysis.ConcaveBifun G = Tdaf.ConvexAnalysis.ConcaveFn (Tdaf.ConvexAnalysis.graphFn G)

theorem Tdaf.ConvexAnalysis.concaveBifun_iff {U : Type u_1} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {G : Bifun U X} : ConcaveBifun G ↔ ConcaveFn (graphFn G)

def Tdaf.ConvexAnalysis.adjointSwap (V : Type u_5) (Y : Type u_6) [AddCommGroup V] [Module ℝ V] [AddCommGroup Y] [Module ℝ Y] : Y × V →ₗ[ℝ] V × Y

The reflection (y, v) ↦ (-v, y) that turns the adjoint into a conjugate.

Equations

• Tdaf.ConvexAnalysis.adjointSwap V Y = (-LinearMap.snd ℝ Y V).prod (LinearMap.fst ℝ Y V)

@[simp]

theorem Tdaf.ConvexAnalysis.adjointSwap_apply (V : Type u_5) (Y : Type u_6) [AddCommGroup V] [Module ℝ V] [AddCommGroup Y] [Module ℝ Y] (q : Y × V) : (adjointSwap V Y) q = (-q.2, q.1)

theorem Tdaf.ConvexAnalysis.graphFn_adjointBifun {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 →ₗ[ℝ] ℝ) (F : Bifun U X) : graphFn (adjointBifun Bu Bx F) = fun (q : Y × V) => -compLin (conj (prodPairing Bu Bx) (graphFn F)) (adjointSwap V Y) q

The graph function of the adjoint is minus a conjugate composed with a linear reflection.

theorem Tdaf.ConvexAnalysis.concaveFn_graphFn_adjointBifun {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 →ₗ[ℝ] ℝ) (F : Bifun U X) : ConcaveFn (graphFn (adjointBifun Bu Bx F))

The adjoint of any bifunction is concave. No convexity, properness or closedness of F is needed.

theorem Tdaf.ConvexAnalysis.concaveBifun_adjointBifun {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 →ₗ[ℝ] ℝ) (F : Bifun U X) : ConcaveBifun (adjointBifun Bu Bx F)

The same, packaged as a statement about bifunctions.

theorem Tdaf.ConvexAnalysis.convexBifun_neg_adjointBifun {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 →ₗ[ℝ] ℝ) (F : Bifun U X) : ConvexBifun fun (y : Y) (v : V) => -adjointBifun Bu Bx F y v

The same negated: -F* is a convex bifunction. This is the shape in which the concave normality criteria consume the adjoint.

theorem Tdaf.ConvexAnalysis.continuous_adjointSwap {V : Type u_2} {Y : Type u_4} [AddCommGroup V] [Module ℝ V] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace V] [IsTopologicalAddGroup V] [TopologicalSpace Y] : Continuous ⇑(adjointSwap V Y)

theorem Tdaf.ConvexAnalysis.closedConcaveFn_graphFn_adjointBifun {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 (prodPairing Bu Bx).flip] {F : Bifun U X} : ClosedConcaveFn (graphFn (adjointBifun Bu Bx F))

The adjoint of any bifunction is concave-closed. The conjugate is closed, and closedness survives the linear reflection.

The closure of a bifunction

noncomputable def Tdaf.ConvexAnalysis.clBifun {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] (F : Bifun U X) : Bifun U X

The closure of a bifunction: the bifunction whose graph function is the closure of that of F. Two applications of the adjoint return exactly this.

Equations

• Tdaf.ConvexAnalysis.clBifun F u x = Tdaf.ConvexAnalysis.clFn (Tdaf.ConvexAnalysis.graphFn F) (u, x)

theorem Tdaf.ConvexAnalysis.clBifun_apply {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] (F : Bifun U X) (u : U) (x : X) : clBifun F u x = clFn (graphFn F) (u, x)

@[simp]

theorem Tdaf.ConvexAnalysis.graphFn_clBifun {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] (F : Bifun U X) : graphFn (clBifun F) = clFn (graphFn F)

def Tdaf.ConvexAnalysis.ClosedBifun {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] (F : Bifun U X) : Prop

A bifunction is closed when its graph function is.

Equations

• Tdaf.ConvexAnalysis.ClosedBifun F = Tdaf.ConvexAnalysis.ClosedFn (Tdaf.ConvexAnalysis.graphFn F)

theorem Tdaf.ConvexAnalysis.closedBifun_iff {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] {F : Bifun U X} : ClosedBifun F ↔ ClosedFn (graphFn F)

theorem Tdaf.ConvexAnalysis.clBifun_le {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] (F : Bifun U X) : clBifun F ≤ F

theorem Tdaf.ConvexAnalysis.ClosedBifun.clBifun_eq {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] {F : Bifun U X} (hF : ClosedBifun F) : clBifun F = F

theorem Tdaf.ConvexAnalysis.closedBifun_iff_clBifun_eq {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] {F : Bifun U X} : ClosedBifun F ↔ clBifun F = F

theorem Tdaf.ConvexAnalysis.closedBifun_clBifun {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [AddCommGroup U] [IsTopologicalAddGroup U] [TopologicalSpace X] [AddCommGroup X] [IsTopologicalAddGroup X] (F : Bifun U X) : ClosedBifun (clBifun F)

The closure of a bifunction, slice by slice

theorem Tdaf.ConvexAnalysis.domBifun_eq_image_dom_graphFn {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] (F : Bifun U X) : domBifun F = ⇑(LinearMap.fst ℝ U X) '' dom (graphFn F)

The effective domain of a bifunction is the projection of that of its graph function. Since ri and closure commute with a linear image, the slice-by-slice closure is a fact about graph F.

theorem Tdaf.ConvexAnalysis.mem_relint_slice {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {S : Set (U × X)} (hS : Convex ℝ S) {u : U} {x : X} (hux : (u, x) ∈ intrinsicInterior ℝ S) : x ∈ intrinsicInterior ℝ {y : X | (u, y) ∈ S}

Relative interiors pass to slices: if (u, x) is a relative interior point of a convex set of pairs, then x is one of the slice through u.

theorem Tdaf.ConvexAnalysis.clBifun_apply_eq_clFn {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {F : Bifun U X} (hF : ConvexBifun F) {u : U} (hu : u ∈ intrinsicInterior ℝ (domBifun F)) : clBifun F u = clFn (F u)

At a relative interior point of dom F the closure of a convex bifunction is computed slice by slice, (cl F) u = cl (F u). A relative interior point of dom (graph F) is placed over u with x in ri (dom (F u)), and both closures are then the same limit along a segment inside the slice.

theorem Tdaf.ConvexAnalysis.infBifun_clBifun_eq {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {F : Bifun U X} (hF : ConvexBifun F) {u : U} (hu : u ∈ intrinsicInterior ℝ (domBifun F)) : infBifun (clBifun F) u = infBifun F u

At a relative interior point of dom F the program (cl F) u has the same optimal value as F u. A convex function and its closure have the same infimum; the content is the slice formula, which makes (cl F) u a closure at all.

theorem Tdaf.ConvexAnalysis.domBifun_subset_domBifun_clBifun {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {F : Bifun U X} (hF : ConvexBifun F) (hp : Proper (graphFn F)) : domBifun F ⊆ domBifun (clBifun F)

Closing a proper convex bifunction can only enlarge its effective domain.

theorem Tdaf.ConvexAnalysis.domBifun_clBifun_subset_closure {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {F : Bifun U X} (hF : ConvexBifun F) (hp : Proper (graphFn F)) : domBifun (clBifun F) ⊆ closure (domBifun F)

Closing a proper convex bifunction cannot enlarge its effective domain beyond the closure of that domain.

def Tdaf.ConvexAnalysis.ImageClosedBifun {U : Type u_1} {X : Type u_2} [TopologicalSpace X] (F : Bifun U X) : Prop

A bifunction is image-closed when each F u is a closed function. This is all the correspondence with concave-convex functions sees of F.

Equations

• Tdaf.ConvexAnalysis.ImageClosedBifun F = ∀ (u : U), Tdaf.ConvexAnalysis.ClosedFn (F u)

theorem Tdaf.ConvexAnalysis.imageClosedBifun_iff {U : Type u_1} {X : Type u_2} [TopologicalSpace X] {F : Bifun U X} : ImageClosedBifun F ↔ ∀ (u : U), ClosedFn (F u)

theorem Tdaf.ConvexAnalysis.ClosedBifun.imageClosedBifun {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [AddCommGroup U] [IsTopologicalAddGroup U] [TopologicalSpace X] [AddCommGroup X] [IsTopologicalAddGroup X] {F : Bifun U X} (hF : ClosedBifun F) : ImageClosedBifun F

A closed bifunction is image-closed: a slice of a closed function is closed. The converse fails — image-closedness says nothing about the joint behaviour in (u, x).

theorem Tdaf.ConvexAnalysis.ConvexBifun.clBifun {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [AddCommGroup U] [Module ℝ U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [TopologicalSpace X] [AddCommGroup X] [Module ℝ X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] {F : Bifun U X} (hF : ConvexBifun F) : ConvexBifun (ConvexAnalysis.clBifun F)

theorem Tdaf.ConvexAnalysis.adjointBifun_clBifun {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] [TopologicalSpace X] [IsTopologicalAddGroup X] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsContinuousPairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsContinuousPairing Bx] {F : Bifun U X} : adjointBifun Bu Bx (clBifun F) = adjointBifun Bu Bx F

The adjoint sees only the closure: (cl F)* = F*, which is conj_clFn on the graph function.

theorem Tdaf.ConvexAnalysis.closedBifun_neg_adjointBifun {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 (prodPairing Bu Bx).flip] {F : Bifun U X} : ClosedBifun fun (y : Y) (v : V) => -adjointBifun Bu Bx F y v

Negated: -F* is a closed bifunction, with no hypothesis on F.

The second adjoint: F** = cl F

noncomputable def Tdaf.ConvexAnalysis.concaveAdjointBifun {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 →ₗ[ℝ] ℝ) (G : Bifun Y V) : Bifun U X

The adjoint of a concave bifunction: the formula of adjointBifun with the infimum replaced by a supremum. A concave G from Y to V has an adjoint from U to X.

Equations

• Tdaf.ConvexAnalysis.concaveAdjointBifun Bu Bx G u x = ⨆ (q : Y × V), G q.1 q.2 + ↑((Bx x) q.1 - (Bu u) q.2)

theorem Tdaf.ConvexAnalysis.concaveAdjointBifun_apply {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 →ₗ[ℝ] ℝ) (G : Bifun Y V) (u : U) (x : X) : concaveAdjointBifun Bu Bx G u x = ⨆ (q : Y × V), G q.1 q.2 + ↑((Bx x) q.1 - (Bu u) q.2)

theorem Tdaf.ConvexAnalysis.surjective_adjointSwap {V : Type u_2} {Y : Type u_4} [AddCommGroup V] [Module ℝ V] [AddCommGroup Y] [Module ℝ Y] : Function.Surjective ⇑(adjointSwap V Y)

The reflection is onto: (y, v) ↦ (-v, y) hits (v, y) at (y, -v).

theorem Tdaf.ConvexAnalysis.concaveAdjointBifun_adjointBifun_eq_biconj {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 →ₗ[ℝ] ℝ) (F : Bifun U X) (u : U) (x : X) : concaveAdjointBifun Bu Bx (adjointBifun Bu Bx F) u x = biconj (prodPairing Bu Bx) (graphFn F) (u, x)

The algebraic core of the biconjugation: the concave adjoint of F* is the biconjugate of the graph function of F, the two reflections cancelling by reindexing.

theorem Tdaf.ConvexAnalysis.concaveAdjointBifun_adjointBifun_eq_clBifun {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] {F : Bifun U X} (hF : ConvexBifun F) : concaveAdjointBifun Bu Bx (adjointBifun Bu Bx F) = clBifun F

The second adjoint is the closure: F** = cl F. The two adjoints compose to the biconjugate of the graph function, and Fenchel–Moreau turns that into its closure. Compatibility of the product pairing follows from compatibility of Bu and Bx.

theorem Tdaf.ConvexAnalysis.concaveAdjointBifun_adjointBifun_eq_self {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] {F : Bifun U X} (hF : ConvexBifun F) (hcl : ClosedBifun F) : concaveAdjointBifun Bu Bx (adjointBifun Bu Bx F) = F

Fixed-point form: F** = F for a closed convex bifunction.

theorem Tdaf.ConvexAnalysis.exists_adjointBifun_ne_bot {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] {F : Bifun U X} (hF : ClosedProperConvexFn (graphFn F)) : ∃ (y : Y) (v : V), adjointBifun Bu Bx F y v ≠ ⊥

The adjoint of a closed proper convex bifunction is finite somewhere. This is properness of a conjugate, read through adjointBifun_eq_neg_conj_graphFn: F* is somewhere > -∞ exactly when (graph F)* is somewhere < +∞.

theorem Tdaf.ConvexAnalysis.properConcave_graphFn_adjointBifun_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] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] {F : Bifun U X} (hF : ConvexBifun F) (hcl : ClosedBifun F) : ProperConcave (graphFn (adjointBifun Bu Bx F)) ↔ Proper (graphFn F)

The properness clause in full: for a closed convex F, the adjoint F* is a proper concave bifunction exactly when F is proper. This is properness of a conjugate read through the onto reflection (y, v) ↦ (-v, y); as there, closedness is used only for the direction "F proper ⇒ F* proper".

The dual objective

theorem Tdaf.ConvexAnalysis.adjointBifun_zero_apply {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 →ₗ[ℝ] ℝ) (F : Bifun U X) (v : V) : adjointBifun Bu Bx F 0 v = ⨅ (u : U), ↑((Bu u) v) + infBifun F u

The dual objective, unfolded: (F* 0)(v) = ⨅ u (⟨u, v⟩ + inf F u).

theorem Tdaf.ConvexAnalysis.adjointBifun_zero_eq_concaveConj {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 →ₗ[ℝ] ℝ) (F : Bifun U X) : adjointBifun Bu Bx F 0 = concaveConj Bu fun (u : U) => -infBifun F u

The dual objective is the concave conjugate of the concave function -inf F.

theorem Tdaf.ConvexAnalysis.adjointBifun_zero_le {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 →ₗ[ℝ] ℝ) (F : Bifun U X) (v : V) : adjointBifun Bu Bx F 0 v ≤ infBifun F 0

Weak duality: every value of the dual objective is at most the optimal value of (P), with no hypothesis at all.

theorem Tdaf.ConvexAnalysis.mem_kuhnTucker_iff_adjointBifun_zero_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 →ₗ[ℝ] ℝ} {F : Bifun U X} {v : V} (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) : v ∈ KuhnTucker Bu F ↔ infBifun F 0 ≠ ⊤ ∧ infBifun F 0 ≠ ⊥ ∧ adjointBifun Bu Bx F 0 v = infBifun F 0

The half that holds without normality: the Kuhn–Tucker vectors of (P) are the points at which the dual objective attains the optimal value of (P).

theorem Tdaf.ConvexAnalysis.iSup_adjointBifun_zero_le {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 →ₗ[ℝ] ℝ) (F : Bifun U X) : ⨆ (v : V), adjointBifun Bu Bx F 0 v ≤ infBifun F 0

Weak duality in the form normality uses: the supremum of the dual objective never exceeds the optimal value of (P).

Closing a strongly consistent program changes nothing

theorem Tdaf.ConvexAnalysis.relint_domBifun_clBifun {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {F : Bifun U X} (hF : ConvexBifun F) (hp : Proper (graphFn F)) : intrinsicInterior ℝ (domBifun (clBifun F)) = intrinsicInterior ℝ (domBifun F)

Domain clause: closing a proper convex bifunction leaves the relative interior of its effective domain alone. dom (cl F) is sandwiched between dom F and cl (dom F), and such a sandwich has the same relative interior.

theorem Tdaf.ConvexAnalysis.stronglyConsistent_clBifun {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {F : Bifun U X} (hF : ConvexBifun F) (hp : Proper (graphFn F)) (hs : StronglyConsistent F) : StronglyConsistent (clBifun F)

(cl P) is strongly consistent whenever (P) is.

theorem Tdaf.ConvexAnalysis.clBifun_zero_eq_clFn {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {F : Bifun U X} (hF : ConvexBifun F) (hs : StronglyConsistent F) : clBifun F 0 = clFn (F 0)

The objective of (cl P) is the closure of that of (P): the slice formula at the origin.

theorem Tdaf.ConvexAnalysis.infBifun_clBifun_zero_eq {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {F : Bifun U X} (hF : ConvexBifun F) (hs : StronglyConsistent F) : infBifun (clBifun F) 0 = infBifun F 0

(P) and (cl P) have the same optimal value.

theorem Tdaf.ConvexAnalysis.argmin_subset_argmin_clBifun {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {F : Bifun U X} (hF : ConvexBifun F) (hs : StronglyConsistent F) : argmin (F 0) ⊆ argmin (clBifun F 0)

Every optimal solution to (P) is one to (cl P). The inclusion is strict in general — closing can create new minimisers.

theorem Tdaf.ConvexAnalysis.eventually_infBifun_clBifun_eq {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {F : Bifun U X} (hF : ConvexBifun F) (hp : Proper (graphFn F)) (hs : StronglyConsistent F) : ∀ᶠ (u : U) in nhds 0, infBifun (clBifun F) u = infBifun F u

The perturbation functions of (P) and (cl P) agree on a neighbourhood of the origin.

The slice formula supplies agreement only on ri (dom F), a relative neighbourhood; the two are reconciled by the points outside aff (dom F), where both perturbation functions are +∞. Since ri (dom F) is relatively open and dom (cl F) ⊆ cl (dom F) ⊆ aff (dom F), a small enough ball around the origin meets no other kind of point.

theorem Tdaf.ConvexAnalysis.kuhnTucker_clBifun_eq {U : Type u_1} {V : Type u_2} {X : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [AddCommGroup V] [Module ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsContinuousPairing Bu] {F : Bifun U X} {Y : Type u_4} [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsContinuousPairing Bx] (hF : ConvexBifun F) (hs : StronglyConsistent F) : KuhnTucker Bu (clBifun F) = KuhnTucker Bu F

(P) and (cl P) have the same Kuhn–Tucker vectors. Such a vector is a point where the dual objective attains the optimal value, the adjoint does not see the closure, and strong consistency equates the two optimal values.