The algebra of bifunctions

The adjoint of a convex bifunction generalizes the adjoint of a linear transformation. This file generalizes the rest of the linear algebra — addition, scalar multiplication, application to a vector, composition, the inner product — and describes how each behaves under taking adjoints.

operation	here	linear-algebra analogue
F₁ □ F₂	infConvBifun	A₁ + A₂
H₁ ⊡ H₂	infConvFstBifun	the same, in the first variable
Fλ	smulRightBifun	λ A
Ff	imageBifun	A x
GF	compBifun	B ∘ A
F⁎, F⁎*	inverseBifun, lowerAdjointBifun	A⁻¹, (A⁻¹)*
⟨f, g⟩	fenchelSup / fenchelInf / HasFenchelPairing	⟨x, y⟩

Main results

• Sums and scalar multiples — adjointBifun_infConvBifun: (F₁ □ F₂)* = F₁* □ F₂*, the right side a supremal convolution (supConvBifun) of concave bifunctions, with bracket_infConvBifun the bracket identity behind it; and adjointBifun_smulRightBifun, (Fλ)* = F*λ for λ > 0.
• The conjugate of an image — conj_imageBifun, exists_conj_imageBifun_eq: (Ff)* = F⁎* f*, infimum attained (Theorem 38.4 in [^1]); conj_imageBifun_of_bracket_eq_top is the degenerate branch y ∉ dom F*, and closedBifun_lowerAdjointBifun says F⁎* is closed for any F.
• The adjoint of a product — inverseBifun_compBifun, adjointBifun_compBifun, lowerAdjointBifun_compBifun: (GF)⁎ = F⁎ G⁎, (GF)* = F* G* with the supremum attained, and (GF)⁎* = (G⁎*)(F⁎*) (Theorem 38.5 in [^1]); lowerAdjointBifun_infConvFstBifun is (H₁ ⊡ H₂)⁎* = H₁⁎* □ H₂⁎*.
• The closed case — for closed proper convex arguments each operation is closed, its defining extremum is attained, and the adjoint of the result is the closure of the corresponding product or convolution (closedBifun_compBifun and the _eq_clBifun results).
• The inner product — fenchelSup_le_fenchelInf is weak duality, with no hypothesis; fenchelPairing_conj says conjugation reverses ⟨f, g⟩; conj_imageBifun_eq_fenchelPairing (⟨Ff, y⟩ = ⟨f, F* y⟩) and bracket_compBifun_eq_fenchelPairing move an adjoint across it; and fenchelSup_imageBifun_lowerAdjointBifun gives ⟨Ff, g*⟩ = ⟨f, F* g*⟩ (Theorem 38.7 in [^1]).

Implementation notes

Rockafellar's hypotheses throughout are "ri (dom …) and ri (dom …) have a point in common", whose conclusion is that (f + g)* is an exact infimal convolution of f* and g*. That conclusion is taken here as the hypothesis, in the form IsExactSum — one instance per dual vector where the book has a single relative-interior condition. It also demands that both summands be proper, so it is stronger than the book's hypothesis, and needs no topology, no finite dimension.

lowerAdjointBifun Bu Bx F v y is defined as -(adjointBifun Bu Bx F y v); working through F⁎* rather than a second, concave adjoint keeps the closed-case corollaries between convex bifunctions and avoids needing a concave clBifun.

Rockafellar leaves ⟨f, g⟩ undefined when the two extrema differ, so they are kept apart here as fenchelSup, fenchelInf and the predicate HasFenchelPairing that they agree. He also restricts them to dom f ∩ dom g* to avoid ∞ - ∞; for proper f and proper concave g the excluded terms are ⊥ on the sup side and ⊤ on the inf side, so the plain ⨆/⨅ used here agree with his.

References

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

Infimal convolution of bifunctions

noncomputable def Tdaf.ConvexAnalysis.infConvBifun {U : Type u_1} {X : Type u_2} [AddCommGroup X] (F₁ F₂ : Bifun U X) : Bifun U X

Rockafellar's F₁ □ F₂: infimal convolution in the second variable, pointwise in the first.

This is the bifunction analogue of the sum of two linear transformations: if Fᵢ is the convex indicator bifunction of Aᵢ, then F₁ □ F₂ is the convex indicator bifunction of A₁ + A₂.

Equations

• Tdaf.ConvexAnalysis.infConvBifun F₁ F₂ u = Tdaf.ConvexAnalysis.infConv (F₁ u) (F₂ u)

theorem Tdaf.ConvexAnalysis.infConvBifun_apply {U : Type u_1} {X : Type u_2} [AddCommGroup X] (F₁ F₂ : Bifun U X) (u : U) : infConvBifun F₁ F₂ u = infConv (F₁ u) (F₂ u)

theorem Tdaf.ConvexAnalysis.infConvBifun_comm {U : Type u_1} {X : Type u_2} [AddCommGroup X] (F₁ F₂ : Bifun U X) : infConvBifun F₁ F₂ = infConvBifun F₂ F₁

theorem Tdaf.ConvexAnalysis.infConvBifun_assoc {U : Type u_1} {X : Type u_2} [AddCommGroup X] (F₁ F₂ F₃ : Bifun U X) : infConvBifun (infConvBifun F₁ F₂) F₃ = infConvBifun F₁ (infConvBifun F₂ F₃)

theorem Tdaf.ConvexAnalysis.mem_domBifun_iff_dom_nonempty {U : Type u_1} {X : Type u_2} {F : Bifun U X} {u : U} : u ∈ domBifun F ↔ (dom (F u)).Nonempty

theorem Tdaf.ConvexAnalysis.domBifun_infConvBifun {U : Type u_1} {X : Type u_2} [AddCommGroup X] (F₁ F₂ : Bifun U X) : domBifun (infConvBifun F₁ F₂) = domBifun F₁ ∩ domBifun F₂

The effective domain of F₁ □ F₂ is dom F₁ ∩ dom F₂.

No hypothesis at all is needed: dom (f □ g) = dom f + dom g is unconditional, and a sum of sets is nonempty exactly when both summands are.

def Tdaf.ConvexAnalysis.infConvSubLeft (U : Type u_4) (X : Type u_5) [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] : (U × X) × X →ₗ[ℝ] U × X

The linear map ((u, x), y) ↦ (u, x - y), the left half of the change of variables that turns a partial infimal convolution into a partial minimisation.

Equations

• Tdaf.ConvexAnalysis.infConvSubLeft U X = (LinearMap.fst ℝ U X ∘ₗ LinearMap.fst ℝ (U × X) X).prod (LinearMap.snd ℝ U X ∘ₗ LinearMap.fst ℝ (U × X) X - LinearMap.snd ℝ (U × X) X)

@[simp]

theorem Tdaf.ConvexAnalysis.infConvSubLeft_apply {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (q : (U × X) × X) : (infConvSubLeft U X) q = (q.1.1, q.1.2 - q.2)

def Tdaf.ConvexAnalysis.infConvSubRight (U : Type u_4) (X : Type u_5) [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] : (U × X) × X →ₗ[ℝ] U × X

The linear map ((u, x), y) ↦ (u, y), the right half of the same change of variables.

Equations

• Tdaf.ConvexAnalysis.infConvSubRight U X = (LinearMap.fst ℝ U X ∘ₗ LinearMap.fst ℝ (U × X) X).prod (LinearMap.snd ℝ (U × X) X)

@[simp]

theorem Tdaf.ConvexAnalysis.infConvSubRight_apply {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (q : (U × X) × X) : (infConvSubRight U X) q = (q.1.1, q.2)

theorem Tdaf.ConvexAnalysis.graphFn_infConvBifun {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {F₁ F₂ : Bifun U X} (hb₁ : ∀ (u : U) (x : X), F₁ u x ≠ ⊥) (hb₂ : ∀ (u : U) (x : X), F₂ u x ≠ ⊥) (p : U × X) : graphFn (infConvBifun F₁ F₂) p = ⨅ (y : X), (compLin (graphFn F₁) (infConvSubLeft U X) + compLin (graphFn F₂) (infConvSubRight U X)) (p, y)

The graph function of F₁ □ F₂ is a partial minimisation of a convex function on (U × X) × X: the infimum formula for □, read jointly in (u, x).

theorem Tdaf.ConvexAnalysis.convexBifun_infConvBifun {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {F₁ F₂ : Bifun U X} (hb₁ : ∀ (u : U) (x : X), F₁ u x ≠ ⊥) (hb₂ : ∀ (u : U) (x : X), F₂ u x ≠ ⊥) (hF₁ : ConvexBifun F₁) (hF₂ : ConvexBifun F₂) : ConvexBifun (infConvBifun F₁ F₂)

An infimal convolute of convex bifunctions is convex.

F₁ □ F₂ is a partial infimal convolution of the graph functions, so this is convexFn_iInf_right applied to the sum of the two graph functions after the linear change of variables ((u, x), y) ↦ ((u, x - y), (u, y)).

theorem Tdaf.ConvexAnalysis.bracket_infConvBifun {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (F₁ F₂ : Bifun U X) (u : U) : bracket Bx (infConvBifun F₁ F₂) u = bracket Bx F₁ u + bracket Bx F₂ u

The bracket of an infimal convolute is the sum of the brackets, ⟨(F₁ □ F₂) u, x*⟩ = ⟨F₁ u, x*⟩ + ⟨F₂ u, x*⟩.

This is conj_infConv, the unconditional identity (f □ g)* = f* + g*, read slice by slice; no hypothesis is needed, and Rockafellar's convention ∞ - ∞ = -∞ is EReal's own ⊤ + ⊥ = ⊥.

The adjoint of an infimal convolute

noncomputable def Tdaf.ConvexAnalysis.supConvBifun {V : Type u_1} {Y : Type u_2} [AddCommGroup V] (G₁ G₂ : Bifun Y V) : Bifun Y V

The concave analogue of infConvBifun: (G₁ □ G₂) y = G₁ y □ G₂ y, with the supremal convolution in the second variable. Rockafellar writes □ for both, the orientation of the bifunction deciding which is meant.

Equations

• Tdaf.ConvexAnalysis.supConvBifun G₁ G₂ y = Tdaf.ConvexAnalysis.supConv (G₁ y) (G₂ y)

theorem Tdaf.ConvexAnalysis.supConvBifun_apply {V : Type u_1} {Y : Type u_2} [AddCommGroup V] (G₁ G₂ : Bifun Y V) (y : Y) : supConvBifun G₁ G₂ y = supConv (G₁ y) (G₂ y)

theorem Tdaf.ConvexAnalysis.adjointBifun_infConvBifun {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₁ F₂ : Bifun U X) {y : Y} (hex : IsExactSum Bu (fun (u : U) => -bracket Bx F₁ u y) fun (u : U) => -bracket Bx F₂ u y) : adjointBifun Bu Bx (infConvBifun F₁ F₂) y = supConv (adjointBifun Bu Bx F₁ y) (adjointBifun Bu Bx F₂ y)

The adjoint of an infimal convolute is the supremal convolute of the adjoints, (F₁ □ F₂)* = F₁* □ F₂*, one dual vector at a time.

The proof is the concave conjugate of a sum, applied to the two concave functions u ↦ ⟨Fᵢ u, y⟩: the adjoint at y is their concave conjugate, and the bracket of F₁ □ F₂ is their sum. The two properness fields of IsExactSum say that neither u ↦ ⟨Fᵢ u, y⟩ takes the value +∞, which is Rockafellar's branch condition y ∈ dom F₁* ∩ dom F₂*; the exactness field is what his relative-interior condition supplies.

theorem Tdaf.ConvexAnalysis.adjointBifun_infConvBifun_eq_supConvBifun {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₁ F₂ : Bifun U X) (hex : ∀ (y : Y), IsExactSum Bu (fun (u : U) => -bracket Bx F₁ u y) fun (u : U) => -bracket Bx F₂ u y) : adjointBifun Bu Bx (infConvBifun F₁ F₂) = supConvBifun (adjointBifun Bu Bx F₁) (adjointBifun Bu Bx F₂)

The adjoint of an infimal convolute, as an identity of bifunctions rather than pointwise.

EReal bookkeeping

The image of a convex function under a bifunction

def Tdaf.ConvexAnalysis.swapLin (E : Type u_3) (G : Type u_4) [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] : E × G →ₗ[ℝ] G × E

Prod.swap as a linear map.

Equations

• Tdaf.ConvexAnalysis.swapLin E G = (LinearMap.snd ℝ E G).prod (LinearMap.fst ℝ E G)

@[simp]

theorem Tdaf.ConvexAnalysis.swapLin_apply {E : Type u_3} {G : Type u_4} [AddCommGroup E] [Module ℝ E] [AddCommGroup G] [Module ℝ G] (q : E × G) : (swapLin E G) q = (q.2, q.1)

noncomputable def Tdaf.ConvexAnalysis.imageBifun {U : Type u_1} {X : Type u_2} (F : Bifun U X) (f : U → EReal) : X → EReal

Rockafellar's Ff, the image of a convex function under a convex bifunction: (Ff)(x) = ⨅ u, f u + (Fu)(x).

When F is the convex indicator bifunction of a linear map A, this is the image mapLin A f.

Equations

• Tdaf.ConvexAnalysis.imageBifun F f x = ⨅ (u : U), f u + F u x

theorem Tdaf.ConvexAnalysis.imageBifun_apply {U : Type u_1} {X : Type u_2} (F : Bifun U X) (f : U → EReal) (x : X) : imageBifun F f x = ⨅ (u : U), f u + F u x

noncomputable def Tdaf.ConvexAnalysis.concaveImageBifun {U : Type u_1} {X : Type u_2} (G : Bifun U X) (g : U → EReal) : X → EReal

The image of a concave function under a concave bifunction: the mirror of imageBifun, with the infimum replaced by a supremum. Rockafellar's Gg for concave G and g.

Equations

• Tdaf.ConvexAnalysis.concaveImageBifun G g x = ⨆ (u : U), g u + G u x

theorem Tdaf.ConvexAnalysis.concaveImageBifun_apply {U : Type u_1} {X : Type u_2} (G : Bifun U X) (g : U → EReal) (x : X) : concaveImageBifun G g x = ⨆ (u : U), g u + G u x

theorem Tdaf.ConvexAnalysis.convexFn_imageBifun {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {F : Bifun U X} {f : U → EReal} (hbF : ∀ (u : U) (x : X), F u x ≠ ⊥) (hbf : ∀ (u : U), f u ≠ ⊥) (hF : ConvexBifun F) (hf : ConvexFn f) : ConvexFn (imageBifun F f)

The image of a convex function under a convex bifunction is convex on X.

(u, x) ↦ f u + (Fu)(x) is convex on U × X, and Ff is its image under the projection (u, x) ↦ x.

noncomputable def Tdaf.ConvexAnalysis.lowerAdjointBifun {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 V Y

Rockafellar's F⁎*: the adjoint of the inverse of F, a convex bifunction from V to Y.

It is the reflected negative of the adjoint, (F⁎* v)(y) = -(F* y)(v); that identity is lowerAdjointBifun_eq_concaveAdjointBifun, and it is the reason F⁎* needs no separate construction.

Equations

• Tdaf.ConvexAnalysis.lowerAdjointBifun Bu Bx F v y = -Tdaf.ConvexAnalysis.adjointBifun Bu Bx F y v

@[simp]

theorem Tdaf.ConvexAnalysis.lowerAdjointBifun_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) (y : Y) : lowerAdjointBifun Bu Bx F v y = -adjointBifun Bu Bx F y v

theorem Tdaf.ConvexAnalysis.lowerAdjointBifun_eq_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 →ₗ[ℝ] ℝ) (F : Bifun U X) : lowerAdjointBifun Bu Bx F = concaveAdjointBifun Bu.flip Bx.flip (inverseBifun F)

F⁎* really is the adjoint of the inverse bifunction F⁎: the concave adjoint of F⁎, taken for the flipped pairings, is the reflected negative of F*.

Both sides are the same extremum over U × X, read once through Prod.swap; the only arithmetic is -(z + c) = -z + (-c) for a real constant c, which needs no side condition.

theorem Tdaf.ConvexAnalysis.convexBifun_lowerAdjointBifun {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 (lowerAdjointBifun Bu Bx F)

F⁎* is a convex bifunction, with no hypothesis on F: it is the negative of the concave F*, read through the swap of the two factors.

The lower adjoint is closed

theorem Tdaf.ConvexAnalysis.closedBifun_lowerAdjointBifun {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 (lowerAdjointBifun Bu Bx F)

F⁎* is a closed convex bifunction, with no hypothesis on F at all.

The adjoint F* is concave-closed for any F; F⁎* is its reflected negative, and closedness carries across the reflection. This is what makes a bifunction exhibited as some H⁎* closed.

The conjugate of an image

theorem Tdaf.ConvexAnalysis.conj_imageBifun_eq_iSup {U : Type u_1} {X : Type u_3} {Y : Type u_4} [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} {F : Bifun U X} {f : U → EReal} (hbF : ∀ (u : U) (x : X), F u x ≠ ⊥) (hbf : ∀ (u : U), f u ≠ ⊥) (y : Y) : conj Bx (imageBifun F f) y = ⨆ (u : U), bracket Bx F u y - f u

The conjugate of the image Ff is the supremum over u of the bracket ⟨Fu, y⟩ offset by f u. This is the whole computational content of the formula for (Ff)*; what remains is Fenchel's duality theorem applied to the concave function u ↦ ⟨Fu, y⟩.

theorem Tdaf.ConvexAnalysis.conj_imageBifun_eq_neg_iInf {U : Type u_1} {X : Type u_3} {Y : Type u_4} [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} {F : Bifun U X} {f : U → EReal} (hbF : ∀ (u : U) (x : X), F u x ≠ ⊥) (hbf : ∀ (u : U), f u ≠ ⊥) {y : Y} (hgt : ∀ (u : U), bracket Bx F u y ≠ ⊤) : conj Bx (imageBifun F f) y = -⨅ (u : U), f u - bracket Bx F u y

The same supremum as conj_imageBifun_eq_iSup, turned around: when no bracket value is ⊤, (Ff)*(y) is minus the infimum of f - ⟨F·, y⟩, which is the primal side of Fenchel's duality theorem.

theorem Tdaf.ConvexAnalysis.conj_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] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} {F : Bifun U X} {f : U → EReal} (hbF : ∀ (u : U) (x : X), F u x ≠ ⊥) (hf : Proper f) {y : Y} (hex : IsExactSum Bu f fun (u : U) => -bracket Bx F u y) : conj Bx (imageBifun F f) y = ⨅ (v : V), conj Bu f v - adjointBifun Bu Bx F y v

The conjugate of an image is the image under the lower adjoint, (Ff)* = F⁎* f*, in the pointwise form (Ff)*(y) = ⨅ v, f*(v) - (F* y)(v).

The hypothesis is that Fenchel's duality theorem applies to f and to the concave function u ↦ ⟨Fu, y⟩ — Rockafellar's "ri (dom f) and ri (dom F) have a point in common", as an IsExactSum. It also carries Proper (-⟨F·, y⟩), i.e. his side condition y ∈ dom F*; the degenerate branch is conj_imageBifun_of_bracket_eq_top.

theorem Tdaf.ConvexAnalysis.exists_conj_imageBifun_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 →ₗ[ℝ] ℝ} {F : Bifun U X} {f : U → EReal} (hbF : ∀ (u : U) (x : X), F u x ≠ ⊥) (hf : Proper f) {y : Y} (hex : IsExactSum Bu f fun (u : U) => -bracket Bx F u y) : ∃ (v : V), conj Bu f v - adjointBifun Bu Bx F y v = conj Bx (imageBifun F f) y

The infimum defining (F⁎* f*)(y) is attained, under the hypothesis of conj_imageBifun.

theorem Tdaf.ConvexAnalysis.conj_imageBifun_of_bracket_eq_top {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} {f : U → EReal} (hbF : ∀ (u : U) (x : X), F u x ≠ ⊥) (hf : Proper f) {u₀ : U} {y : Y} (htop : bracket Bx F u₀ y = ⊤) (hfin : f u₀ ≠ ⊤) : conj Bx (imageBifun F f) y = ⊤ ∧ imageBifun (lowerAdjointBifun Bu Bx F) (conj Bu f) y = ⊤

The degenerate branch of (Ff)* = F⁎* f*, y ∉ dom F*: if the bracket ⟨Fu, y⟩ is +∞ at some u where f is finite, both sides are +∞.

With the finiteness of f u₀ as an explicit hypothesis this is unconditional, where Rockafellar reaches the case from a relative-interior hypothesis instead.

The image of a closed proper convex function

theorem Tdaf.ConvexAnalysis.adjointBifun_ne_top {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] {F : Bifun U X} {u₀ : U} {x₀ : X} (hF : F u₀ x₀ ≠ ⊤) (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (y : Y) (v : V) : adjointBifun Bu Bx F y v ≠ ⊤

The adjoint of a bifunction that is finite somewhere is nowhere ⊤: the infimum defining it is bounded above by the single term at (u₀, x₀).

theorem Tdaf.ConvexAnalysis.lowerAdjointBifun_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] {F : Bifun U X} {u₀ : U} {x₀ : X} (hF : F u₀ x₀ ≠ ⊤) (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (v : V) (y : Y) : lowerAdjointBifun Bu Bx F v y ≠ ⊥

F⁎* never takes the value -∞ when F is finite somewhere. This is the hypothesis hbF of conj_imageBifun, for the bifunction F⁎*.

theorem Tdaf.ConvexAnalysis.conj_imageBifun_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] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} {F : Bifun U X} {f : U → EReal} (hbF : ∀ (u : U) (x : X), F u x ≠ ⊥) (hf : Proper f) {y : Y} (hex : IsExactSum Bu f fun (u : U) => -bracket Bx F u y) : conj Bx (imageBifun F f) y = imageBifun (lowerAdjointBifun Bu Bx F) (conj Bu f) y

(Ff)* = F⁎* f* packaged as an identity of functions rather than as a formula for the values. The two sides differ only by a - b = a + (-b).

theorem Tdaf.ConvexAnalysis.lowerAdjointBifun_lowerAdjointBifun_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) : lowerAdjointBifun Bu.flip Bx.flip (lowerAdjointBifun Bu Bx F) = clBifun F

F⁎*⁎* = cl F, the biadjoint identity in the F⁎* packaging.

Rockafellar states the biadjoint as F** = cl F for the concave adjoint of F*; taking F⁎* twice is the same computation with the two negations moved outside, so nothing concave is built.

theorem Tdaf.ConvexAnalysis.conj_imageBifun_lowerAdjointBifun {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} {f : U → EReal} (hF : ConvexBifun F) (hFcl : ClosedBifun F) {u₀ : U} {x₀ : X} (hFp : F u₀ x₀ ≠ ⊤) (hf : ClosedProperConvexFn f) {x : X} (hex : IsExactSum Bu.flip (conj Bu f) fun (v : V) => -bracket Bx.flip (lowerAdjointBifun Bu Bx F) v x) : conj Bx.flip (imageBifun (lowerAdjointBifun Bu Bx F) (conj Bu f)) x = imageBifun F f x

(F⁎* f*)* = Ff for a closed proper convex F and a closed proper convex f — the identity the rest of the closed case follows from.

This is conj_imageBifun applied to F⁎* and f*, whose own adjoint and conjugate are F and f again. Rockafellar's ri (dom f*) ∩ ri (dom F⁎*) ≠ ∅ is the IsExactSum hypothesis.

theorem Tdaf.ConvexAnalysis.closedFn_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] {F : Bifun U X} {f : U → EReal} (hF : ConvexBifun F) (hFcl : ClosedBifun F) {u₀ : U} {x₀ : X} (hFp : F u₀ x₀ ≠ ⊤) (hf : ClosedProperConvexFn f) (hex : ∀ (x : X), IsExactSum Bu.flip (conj Bu f) fun (v : V) => -bracket Bx.flip (lowerAdjointBifun Bu Bx F) v x) : ClosedFn (imageBifun F f)

The image Ff of a closed proper convex function is closed. It is a conjugate.

theorem Tdaf.ConvexAnalysis.exists_imageBifun_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] {F : Bifun U X} {f : U → EReal} (hF : ConvexBifun F) (hFcl : ClosedBifun F) {u₀ : U} {x₀ : X} (hFp : F u₀ x₀ ≠ ⊤) (hf : ClosedProperConvexFn f) {x : X} (hex : IsExactSum Bu.flip (conj Bu f) fun (v : V) => -bracket Bx.flip (lowerAdjointBifun Bu Bx F) v x) : ∃ (u : U), f u + F u x = imageBifun F f x

The infimum defining (Ff)(x) is attained, for a closed proper convex F and f. This is exists_conj_imageBifun_eq read at F⁎* and f*.

theorem Tdaf.ConvexAnalysis.conj_imageBifun_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] {F : Bifun U X} {f : U → EReal} [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] [IsCompatiblePairing Bx.flip] (hF : ConvexBifun F) (hFcl : ClosedBifun F) {u₀ : U} {x₀ : X} (hFp : F u₀ x₀ ≠ ⊤) (hf : ClosedProperConvexFn f) (hex : ∀ (x : X), IsExactSum Bu.flip (conj Bu f) fun (v : V) => -bracket Bx.flip (lowerAdjointBifun Bu Bx F) v x) : conj Bx (imageBifun F f) = clFn (imageBifun (lowerAdjointBifun Bu Bx F) (conj Bu f))

(Ff)* = cl (F⁎* f*) for a closed proper convex F and f.

Ff is the conjugate of F⁎* f*, so (Ff)* is its biconjugate, which is its closure.

The inner product of a convex and a concave function

noncomputable def Tdaf.ConvexAnalysis.fenchelSup {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (g : F → EReal) : EReal

The sup side of Rockafellar's inner product ⟨f, g⟩ of a convex f on E and a concave g on the paired space F: sup_x {g*(x) - f(x)}.

Equations

• Tdaf.ConvexAnalysis.fenchelSup B f g = ⨆ (x : E), Tdaf.ConvexAnalysis.concaveConj B.flip g x - f x

noncomputable def Tdaf.ConvexAnalysis.fenchelInf {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (g : F → EReal) : EReal

The inf side of ⟨f, g⟩: inf_y {f*(y) - g(y)}.

Equations

• Tdaf.ConvexAnalysis.fenchelInf B f g = ⨅ (y : F), Tdaf.ConvexAnalysis.conj B f y - g y

theorem Tdaf.ConvexAnalysis.fenchelSup_apply {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (g : F → EReal) : fenchelSup B f g = ⨆ (x : E), concaveConj B.flip g x - f x

theorem Tdaf.ConvexAnalysis.fenchelInf_apply {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (g : F → EReal) : fenchelInf B f g = ⨅ (y : F), conj B f y - g y

def Tdaf.ConvexAnalysis.HasFenchelPairing {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (g : F → EReal) : Prop

Rockafellar's inner product ⟨f, g⟩ exists exactly when the two extrema agree; when they do not, ⟨f, g⟩ is undefined.

Equations

• Tdaf.ConvexAnalysis.HasFenchelPairing B f g = (Tdaf.ConvexAnalysis.fenchelSup B f g = Tdaf.ConvexAnalysis.fenchelInf B f g)

noncomputable def Tdaf.ConvexAnalysis.fenchelPairing {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (g : F → EReal) : EReal

The value of Rockafellar's ⟨f, g⟩, represented by the inf side.

Only under HasFenchelPairing is this Rockafellar's inner product; HasFenchelPairing.fenchelSup_eq is the statement that the sup side then agrees.

Equations

• Tdaf.ConvexAnalysis.fenchelPairing B f g = Tdaf.ConvexAnalysis.fenchelInf B f g

theorem Tdaf.ConvexAnalysis.HasFenchelPairing.fenchelSup_eq {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {g : F → EReal} (h : HasFenchelPairing B f g) : fenchelSup B f g = fenchelPairing B f g

theorem Tdaf.ConvexAnalysis.fenchelPairing_eq_fenchelInf {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (g : F → EReal) : fenchelPairing B f g = fenchelInf B f g

theorem Tdaf.ConvexAnalysis.fenchelSup_le_fenchelInf {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (g : F → EReal) : fenchelSup B f g ≤ fenchelInf B f g

Weak duality for the inner product: the sup side never exceeds the inf side.

No hypothesis at all; both ∞ - ∞ collisions are absorbed on the correct side, exactly as in concaveConj_sub_conj_le_sub.

theorem Tdaf.ConvexAnalysis.hasFenchelPairing_of_le {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {g : F → EReal} (h : fenchelInf B f g ≤ fenchelSup B f g) : HasFenchelPairing B f g

Conjugation reverses the inner product

theorem Tdaf.ConvexAnalysis.fenchelInf_conj_le_neg_fenchelSup {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {g : F → EReal} (hf : Proper f) (hg : ProperConcave g) : fenchelInf B.flip (conj B f) (concaveConj B.flip g) ≤ -fenchelSup B f g

One of the two outer steps of the four-term chain below: the inf side of ⟨f*, g*⟩ is at most -⟨f, g⟩ read on the sup side. It rests only on f** ≤ f.

theorem Tdaf.ConvexAnalysis.neg_fenchelInf_le_fenchelSup_conj {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {g : F → EReal} (hf : Proper f) (hg : ProperConcave g) : -fenchelInf B f g ≤ fenchelSup B.flip (conj B f) (concaveConj B.flip g)

The other outer step: -⟨f, g⟩ read on the inf side is at most the sup side of ⟨f*, g*⟩. It rests only on g ≤ g**.

theorem Tdaf.ConvexAnalysis.hasFenchelPairing_conj {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {g : F → EReal} (hf : Proper f) (hg : ProperConcave g) (h : HasFenchelPairing B f g) : HasFenchelPairing B.flip (conj B f) (concaveConj B.flip g)

If ⟨f, g⟩ exists then so does ⟨f*, g*⟩.

The proof is the chain -⟨f, g⟩ ≤ ⟨f*, g*⟩_sup ≤ ⟨f*, g*⟩_inf ≤ -⟨f, g⟩, the middle link being weak duality; when the two ends coincide all four terms do.

theorem Tdaf.ConvexAnalysis.fenchelPairing_conj {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {g : F → EReal} (hf : Proper f) (hg : ProperConcave g) (h : HasFenchelPairing B f g) : fenchelPairing B.flip (conj B f) (concaveConj B.flip g) = -fenchelPairing B f g

Conjugation reverses the inner product: ⟨f*, g*⟩ = -⟨f, g⟩.

An adjoint moves across the inner product

theorem Tdaf.ConvexAnalysis.fenchelSup_conj_eq_neg_fenchelInf {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {f h : E → EReal} (hd : (dom f).Nonempty) (hh : (domConcave h).Nonempty) : fenchelSup B.flip (conj B f) h = -fenchelInf B f (concaveConj B h)

⟨f*, g⟩ read on the sup side is minus ⟨f, g*⟩ read on the inf side.

This is pure sign bookkeeping, and it is the step that lets an adjoint move across the inner product.

theorem Tdaf.ConvexAnalysis.bracket_le_concaveConj_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) (y : Y) (u : U) : bracket Bx F u y ≤ concaveConj Bu.flip (adjointBifun Bu Bx F y) u

The bracket ⟨Fu, y⟩ is below the concave biconjugate that ⟨f, F* y⟩ sees. This is le_biconcaveConj after adjointBifun_eq_concaveConj_bracket, and it is what makes the existence of ⟨f, F* y⟩ free.

theorem Tdaf.ConvexAnalysis.hasFenchelPairing_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} {f : U → EReal} (hbF : ∀ (u : U) (x : X), F u x ≠ ⊥) (hf : Proper f) {y : Y} (hex : IsExactSum Bu f fun (u : U) => -bracket Bx F u y) : HasFenchelPairing Bu f (adjointBifun Bu Bx F y)

The inner product ⟨f, F* y⟩ exists, its two extrema agreeing.

Weak duality gives one inequality for free; the other is conj_imageBifun together with bracket_le_concaveConj_adjointBifun.

theorem Tdaf.ConvexAnalysis.conj_imageBifun_eq_fenchelPairing {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} {f : U → EReal} (hbF : ∀ (u : U) (x : X), F u x ≠ ⊥) (hf : Proper f) {y : Y} (hex : IsExactSum Bu f fun (u : U) => -bracket Bx F u y) : conj Bx (imageBifun F f) y = fenchelPairing Bu f (adjointBifun Bu Bx F y)

An adjoint moves across the inner product: ⟨Ff, y⟩ = ⟨f, F* y⟩.

The left-hand side is the bracket ⟨Ff, x*⟩, i.e. (Ff)*(x*); the right-hand side is the inner product of the convex f with the concave function F* x*.

theorem Tdaf.ConvexAnalysis.concaveImageBifun_adjointBifun_ne_top {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] {F : Bifun U X} {g : X → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) {u₀ : U} {x₀ : X} (hF : F u₀ x₀ ≠ ⊤) (hgb : g x₀ ≠ ⊥) (hgt : g x₀ ≠ ⊤) (v : V) : concaveImageBifun (adjointBifun Bu Bx F) (concaveConj Bx g) v ≠ ⊤

The image F* g* of a concave conjugate under the adjoint is nowhere ⊤, provided F is finite at some (u₀, x₀) at which g is finite.

The bound is uniform in y because the two occurrences of ⟨x₀, y⟩ cancel: every term of the supremum is bounded by F u₀ x₀ + ⟨u₀, v⟩ - g x₀.

theorem Tdaf.ConvexAnalysis.fenchelSup_imageBifun_lowerAdjointBifun {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} {f : U → EReal} {g : X → EReal} (hf : Proper f) (hgd : (domConcave g).Nonempty) {u₀ : U} {x₀ : X} (hF : F u₀ x₀ ≠ ⊤) (hgb : g x₀ ≠ ⊥) (hgt : g x₀ ≠ ⊤) : fenchelSup Bx.flip (imageBifun (lowerAdjointBifun Bu Bx F) (conj Bu f)) g = -fenchelInf Bu f (concaveImageBifun (adjointBifun Bu Bx F) (concaveConj Bx g))

The "by definition" identity behind ⟨Ff, g*⟩ = ⟨f, F* g*⟩: ⟨F⁎* f*, g⟩ on the sup side is minus ⟨f, F* g*⟩ on the inf side.

Both unwind to the same double extremum over V × Y, term by term ⟨F* y, g*⟩ - f*(v) = (g*(y) + (F* y)(v)) - f*(v).

theorem Tdaf.ConvexAnalysis.dom_imageBifun_nonempty {U : Type u_1} {X : Type u_3} {F : Bifun U X} {f : U → EReal} (hbF : ∀ (u : U) (x : X), F u x ≠ ⊥) (hf : Proper f) {u₀ : U} {x₀ : X} (hF : F u₀ x₀ ≠ ⊤) (hfu : f u₀ ≠ ⊤) : (dom (imageBifun F f)).Nonempty

If f and F are both finite at some common u₀, the image Ff is not identically ⊤.

theorem Tdaf.ConvexAnalysis.fenchelSup_imageBifun_lowerAdjointBifun_eq_neg {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} {f : U → EReal} {g : X → EReal} (hbF : ∀ (u : U) (x : X), F u x ≠ ⊥) (hf : Proper f) (hgd : (domConcave g).Nonempty) {u₀ : U} {x₀ : X} (hF : F u₀ x₀ ≠ ⊤) (hfu : f u₀ ≠ ⊤) (hex : ∀ (y : Y), IsExactSum Bu f fun (u : U) => -bracket Bx F u y) : fenchelSup Bx.flip (imageBifun (lowerAdjointBifun Bu Bx F) (conj Bu f)) g = -fenchelInf Bx (imageBifun F f) (concaveConj Bx g)

⟨F⁎* f*, g⟩ = -⟨Ff, g*⟩, the third equality of the chain below.

This is fenchelSup_conj_eq_neg_fenchelInf composed with conj_imageBifun.

theorem Tdaf.ConvexAnalysis.fenchelInf_imageBifun_eq_fenchelInf_concaveImageBifun {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} {f : U → EReal} {g : X → EReal} (hbF : ∀ (u : U) (x : X), F u x ≠ ⊥) (hf : Proper f) (hgd : (domConcave g).Nonempty) {u₀ : U} {x₀ : X} (hF : F u₀ x₀ ≠ ⊤) (hfu : f u₀ ≠ ⊤) (hgb : g x₀ ≠ ⊥) (hgt : g x₀ ≠ ⊤) (hex : ∀ (y : Y), IsExactSum Bu f fun (u : U) => -bracket Bx F u y) : fenchelInf Bx (imageBifun F f) (concaveConj Bx g) = fenchelInf Bu f (concaveImageBifun (adjointBifun Bu Bx F) (concaveConj Bx g))

Adjoints move across the inner product, ⟨Ff, g*⟩ = ⟨f, F* g*⟩.

Rockafellar's route is ⟨Ff, g*⟩ = ⟨f, F* g*⟩ = -⟨f*, F⁎ g⟩ = -⟨F⁎* f*, g⟩, the last step being fenchelSup_imageBifun_lowerAdjointBifun and the other bridge conj_imageBifun. The book's relative-interior hypothesis is carried by hex together with a common point (u₀, x₀) at which f, F and g are all finite. The equation is stated between the two inf sides; each is Rockafellar's inner product as soon as the corresponding pairing exists.

Right scalar multiplication

noncomputable def Tdaf.ConvexAnalysis.smulRightBifun {U : Type u_1} {X : Type u_2} [AddCommGroup X] [Module ℝ X] (F : Bifun U X) (l : ℝ) : Bifun U X

Rockafellar's Fλ: right scalar multiplication of a bifunction, ((Fλ) u)(x) = λ (Fu)(λ⁻¹ x), applied slice by slice.

Equations

• Tdaf.ConvexAnalysis.smulRightBifun F l u = Tdaf.ConvexAnalysis.smulRight (F u) l

theorem Tdaf.ConvexAnalysis.smulRightBifun_apply {U : Type u_1} {X : Type u_2} [AddCommGroup X] [Module ℝ X] (F : Bifun U X) (l : ℝ) (u : U) : smulRightBifun F l u = smulRight (F u) l

def Tdaf.ConvexAnalysis.scaleFst {U : Type u_1} [AddCommGroup U] [Module ℝ U] (X : Type u_4) [AddCommGroup X] [Module ℝ X] (l : ℝ) : U × X →ₗ[ℝ] U × X

The linear map (u, x) ↦ (l • u, x).

Equations

• Tdaf.ConvexAnalysis.scaleFst X l = (l • LinearMap.fst ℝ U X).prod (LinearMap.snd ℝ U X)

@[simp]

theorem Tdaf.ConvexAnalysis.scaleFst_apply {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (l : ℝ) (p : U × X) : (scaleFst X l) p = (l • p.1, p.2)

theorem Tdaf.ConvexAnalysis.graphFn_smulRightBifun {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {l : ℝ} (hl : 0 < l) (F : Bifun U X) : graphFn (smulRightBifun F l) = smulRight (compLin (graphFn F) (scaleFst X l)) l

The graph function of Fλ is a right scalar multiple of the graph function of F, read after the shear (u, x) ↦ (λu, x). This is the linear change of variables (u, x, μ) ↦ (u, λx, λμ) of Rockafellar's proof.

theorem Tdaf.ConvexAnalysis.convexBifun_smulRightBifun {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {F : Bifun U X} {l : ℝ} (hl : 0 < l) (hF : ConvexBifun F) : ConvexBifun (smulRightBifun F l)

Fλ is a convex bifunction when F is, for every λ > 0.

theorem Tdaf.ConvexAnalysis.bracket_smulRightBifun {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] {l : ℝ} (hl : 0 < l) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (F : Bifun U X) (u : U) : bracket Bx (smulRightBifun F l) u = fun (y : Y) => ↑l * bracket Bx F u y

The bracket scales with the bifunction: ⟨(Fλ) u, x*⟩ = λ ⟨Fu, x*⟩. It is the conjugation rule conj_smulRight, slice by slice.

theorem Tdaf.ConvexAnalysis.adjointBifun_smulRightBifun {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] {l : ℝ} (hl : 0 < l) (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (F : Bifun U X) (y : Y) (v : V) : adjointBifun Bu Bx (smulRightBifun F l) y v = smulRight (adjointBifun Bu Bx F y) l v

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

Right scalar multiplication commutes with taking adjoints, with no hypothesis beyond 0 < l: the infimum defining ((Fλ)* y)(v) becomes the one defining ((F* y)λ)(v) under x ↦ l • x.

Composition of bifunctions

noncomputable def Tdaf.ConvexAnalysis.compBifun {U : Type u_1} {X : Type u_2} {Y : Type u_3} (G : Bifun X Y) (F : Bifun U X) : Bifun U Y

Rockafellar's product GF of bifunctions: ((GF) u)(y) = ⨅ x, (Fu)(x) + (Gx)(y).

When F and G are the convex indicator bifunctions of linear maps A and B, GF is the indicator bifunction of B ∘ A.

Equations

• Tdaf.ConvexAnalysis.compBifun G F u y = ⨅ (x : X), F u x + G x y

theorem Tdaf.ConvexAnalysis.compBifun_apply {U : Type u_1} {X : Type u_2} {Y : Type u_3} (G : Bifun X Y) (F : Bifun U X) (u : U) (y : Y) : compBifun G F u y = ⨅ (x : X), F u x + G x y

noncomputable def Tdaf.ConvexAnalysis.concaveCompBifun {U : Type u_1} {X : Type u_2} {Y : Type u_3} (G : Bifun Y X) (F : Bifun X U) : Bifun Y U

The composition of concave bifunctions: the same formula with a supremum.

Equations

• Tdaf.ConvexAnalysis.concaveCompBifun G F y u = ⨆ (x : X), G y x + F x u

theorem Tdaf.ConvexAnalysis.concaveCompBifun_apply {U : Type u_1} {X : Type u_2} {Y : Type u_3} (G : Bifun Y X) (F : Bifun X U) (y : Y) (u : U) : concaveCompBifun G F y u = ⨆ (x : X), G y x + F x u

theorem Tdaf.ConvexAnalysis.inverseBifun_compBifun {U : Type u_1} {X : Type u_2} {Y : Type u_3} (G : Bifun X Y) (F : Bifun U X) (hbF : ∀ (u : U) (x : X), F u x ≠ ⊥) (hbG : ∀ (x : X) (y : Y), G x y ≠ ⊥) : inverseBifun (compBifun G F) = concaveCompBifun (inverseBifun G) (inverseBifun F)

The inverse of a product is the product of the inverses in the opposite order, with the concave orientation: (GF)⁎ = F⁎ G⁎.

def Tdaf.ConvexAnalysis.compLeft (U : Type u_4) (X : Type u_5) (Y : Type u_6) [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] : (U × Y) × X →ₗ[ℝ] U × X

The linear map ((u, y), x) ↦ (u, x).

Equations

• Tdaf.ConvexAnalysis.compLeft U X Y = (LinearMap.fst ℝ U Y ∘ₗ LinearMap.fst ℝ (U × Y) X).prod (LinearMap.snd ℝ (U × Y) X)

@[simp]

theorem Tdaf.ConvexAnalysis.compLeft_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] (q : (U × Y) × X) : (compLeft U X Y) q = (q.1.1, q.2)

def Tdaf.ConvexAnalysis.compRight (U : Type u_4) (X : Type u_5) (Y : Type u_6) [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] : (U × Y) × X →ₗ[ℝ] X × Y

The linear map ((u, y), x) ↦ (x, y).

Equations

• Tdaf.ConvexAnalysis.compRight U X Y = (LinearMap.snd ℝ (U × Y) X).prod (LinearMap.snd ℝ U Y ∘ₗ LinearMap.fst ℝ (U × Y) X)

@[simp]

theorem Tdaf.ConvexAnalysis.compRight_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] (q : (U × Y) × X) : (compRight U X Y) q = (q.2, q.1.2)

theorem Tdaf.ConvexAnalysis.convexBifun_compBifun {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] {F : Bifun U X} {G : Bifun X Y} (hbF : ∀ (u : U) (x : X), F u x ≠ ⊥) (hbG : ∀ (x : X) (y : Y), G x y ≠ ⊥) (hF : ConvexBifun F) (hG : ConvexBifun G) : ConvexBifun (compBifun G F)

A product of convex bifunctions is convex.

(u, x, y) ↦ (Fu)(x) + (Gx)(y) is convex on U × X × Y, and the graph function of GF is its image under the projection (u, x, y) ↦ (u, y).

The adjoint of a product

theorem Tdaf.ConvexAnalysis.concaveBracket_inverseBifun_eq_imageBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (F : Bifun U X) (v : V) : concaveBracket Bu.flip (inverseBifun F) v = imageBifun F fun (u : U) => ↑((Bu u) v)

Rockafellar's f(x) = ⟨u*, F⁎x⟩ is the image Fℓ of the linear function ℓ u = ⟨u, u*⟩ under F. Both sides are ⨅ u, ⟨u, u*⟩ + (Fu)(x); the only step is -(-(Fu)(x)) = (Fu)(x).

theorem Tdaf.ConvexAnalysis.conj_concaveBracket_inverseBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {W : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup W] [Module ℝ W] {F : Bifun U X} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] W →ₗ[ℝ] ℝ) (hbF : ∀ (u : U) (x : X), F u x ≠ ⊥) (v : V) (w : W) : conj Bx (concaveBracket Bu.flip (inverseBifun F) v) w = -adjointBifun Bu Bx F w v

The conjugate of ⟨u*, F⁎·⟩ is -(F* ·)(u*). This is the entry that turns Fenchel's dual value into the adjoint of F; it is conj_imageBifun_eq_iSup read at a linear f.

theorem Tdaf.ConvexAnalysis.adjointBifun_compBifun_eq_iInf {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_5} {Z : Type u_6} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup Y] [Module ℝ Y] [AddCommGroup Z] [Module ℝ Z] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (By : Y →ₗ[ℝ] Z →ₗ[ℝ] ℝ) (F : Bifun U X) (G : Bifun X Y) {z : Z} {v : V} (hfb : ∀ (x : X), concaveBracket Bu.flip (inverseBifun F) v x ≠ ⊥) (hgt : ∀ (x : X), bracket By G x z ≠ ⊤) : adjointBifun Bu By (compBifun G F) z v = ⨅ (x : X), concaveBracket Bu.flip (inverseBifun F) v x - bracket By G x z

The primal problem behind the adjoint of a product. ((GF)* z)(v) is the infimum over x of the difference between the convex ⟨v, F⁎x⟩ and the concave ⟨Gx, z⟩.

This is the whole EReal content of Rockafellar's proof: the triple infimum defining ((GF)* z)(v) is reindexed as ⨅ x ⨅ u ⨅ y, and the inner double infimum splits because neither half is -∞ — exactly the properness Fenchel's duality theorem will demand.

theorem Tdaf.ConvexAnalysis.adjointBifun_compBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {W : Type u_4} {Y : Type u_5} {Z : Type u_6} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup W] [Module ℝ W] [AddCommGroup Y] [Module ℝ Y] [AddCommGroup Z] [Module ℝ Z] {F : Bifun U X} {G : Bifun X Y} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] W →ₗ[ℝ] ℝ) (By : Y →ₗ[ℝ] Z →ₗ[ℝ] ℝ) (hbF : ∀ (u : U) (x : X), F u x ≠ ⊥) {z : Z} {v : V} (hex : IsExactSum Bx (concaveBracket Bu.flip (inverseBifun F) v) fun (x : X) => -bracket By G x z) : adjointBifun Bu By (compBifun G F) z v = concaveCompBifun (adjointBifun Bx By G) (adjointBifun Bu Bx F) z v

The adjoint of a product is the product of the adjoints, (GF)* = F* G*, the right-hand side being the concave product, ((F* G*) z)(v) = ⨆ w, ((G* z)(w) + (F* w)(v)).

The proof is Rockafellar's: Fenchel's duality theorem applied to f(x) = ⟨v, F⁎x⟩ and g(x) = ⟨Gx, z⟩, with adjointBifun_compBifun_eq_iInf for the primal side. His ri (dom F⁎) ∩ ri (dom G) ≠ ∅ is again an IsExactSum — one instance per (z, v), since f and g depend on them, where his single condition does not. Like conj_imageBifun it carries the properness selecting the main branch; his degenerate branches z ∉ dom G* and v ∉ dom F⁎* are where f or g fails to be proper.

theorem Tdaf.ConvexAnalysis.lowerAdjointBifun_compBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {W : Type u_4} {Y : Type u_5} {Z : Type u_6} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup W] [Module ℝ W] [AddCommGroup Y] [Module ℝ Y] [AddCommGroup Z] [Module ℝ Z] {F : Bifun U X} {G : Bifun X Y} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] W →ₗ[ℝ] ℝ) (By : Y →ₗ[ℝ] Z →ₗ[ℝ] ℝ) (hbF : ∀ (u : U) (x : X), F u x ≠ ⊥) {u₀ : U} {x₀ : X} (hFp : F u₀ x₀ ≠ ⊤) {x₁ : X} {y₁ : Y} (hGp : G x₁ y₁ ≠ ⊤) {z : Z} {v : V} (hex : IsExactSum Bx (concaveBracket Bu.flip (inverseBifun F) v) fun (x : X) => -bracket By G x z) : lowerAdjointBifun Bu By (compBifun G F) v z = compBifun (lowerAdjointBifun Bx By G) (lowerAdjointBifun Bu Bx F) v z

The adjoint of a product in the F⁎* packaging: (GF)⁎* = (G⁎*)(F⁎*).

Inversion reverses the order twice, so the composite on the right is taken in the same order as GF, and both sides are convex bifunctions — no concave product is needed. The two ≠ ⊤ hypotheses are what let the negation split across the sum.

theorem Tdaf.ConvexAnalysis.exists_adjointBifun_compBifun_eq {U : Type u_1} {V : Type u_2} {X : Type u_3} {W : Type u_4} {Y : Type u_5} {Z : Type u_6} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup W] [Module ℝ W] [AddCommGroup Y] [Module ℝ Y] [AddCommGroup Z] [Module ℝ Z] {F : Bifun U X} {G : Bifun X Y} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] W →ₗ[ℝ] ℝ) (By : Y →ₗ[ℝ] Z →ₗ[ℝ] ℝ) (hbF : ∀ (u : U) (x : X), F u x ≠ ⊥) {z : Z} {v : V} (hex : IsExactSum Bx (concaveBracket Bu.flip (inverseBifun F) v) fun (x : X) => -bracket By G x z) : ∃ (w : W), adjointBifun Bx By G z w + adjointBifun Bu Bx F w v = adjointBifun Bu By (compBifun G F) z v

The supremum defining ((F* G*) z)(v) is attained, under the hypothesis of adjointBifun_compBifun.

Products of closed proper convex bifunctions

theorem Tdaf.ConvexAnalysis.exists_lowerAdjointBifun_ne_top {U : Type u_1} {V : Type u_2} {X : Type u_3} {W : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup W] [Module ℝ W] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] {F : Bifun U X} (hF : ClosedProperConvexFn (graphFn F)) (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] (Bx : X →ₗ[ℝ] W →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] : ∃ (v : V) (w : W), lowerAdjointBifun Bu Bx F v w ≠ ⊤

F⁎* is somewhere < ⊤, for a closed proper convex F: that is properness of F* (exists_adjointBifun_ne_bot) read through the reflection.

theorem Tdaf.ConvexAnalysis.lowerAdjointBifun_compBifun_lowerAdjointBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {W : Type u_4} {Y : Type u_5} {Z : Type u_6} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup W] [Module ℝ W] [AddCommGroup Y] [Module ℝ Y] [AddCommGroup Z] [Module ℝ Z] [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 →ₗ[ℝ] W →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] {By : Y →ₗ[ℝ] Z →ₗ[ℝ] ℝ} [IsCompatiblePairing By] {F : Bifun U X} {G : Bifun X Y} (hF : ClosedProperConvexFn (graphFn F)) (hG : ClosedProperConvexFn (graphFn G)) {u : U} {y : Y} (hex : IsExactSum Bx.flip (concaveBracket Bu (inverseBifun (lowerAdjointBifun Bu Bx F)) u) fun (w : W) => -bracket By.flip (lowerAdjointBifun Bx By G) w y) : lowerAdjointBifun Bu.flip By.flip (compBifun (lowerAdjointBifun Bx By G) (lowerAdjointBifun Bu Bx F)) u y = compBifun G F u y

(G⁎* F⁎*)⁎* = GF for closed proper convex F and G — the identity the rest of the closed case follows from.

This is lowerAdjointBifun_compBifun applied to the pair (F⁎*, G⁎*), whose own lower adjoints are F and G again. Rockafellar's condition that ri (dom F*) and ri (dom G⁎*) have a point in common is the IsExactSum hypothesis, one instance per (u, y).

theorem Tdaf.ConvexAnalysis.closedBifun_compBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {W : Type u_4} {Y : Type u_5} {Z : Type u_6} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup W] [Module ℝ W] [AddCommGroup Y] [Module ℝ Y] [AddCommGroup Z] [Module ℝ Z] [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 →ₗ[ℝ] W →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] {By : Y →ₗ[ℝ] Z →ₗ[ℝ] ℝ} [IsCompatiblePairing By] {F : Bifun U X} {G : Bifun X Y} (hF : ClosedProperConvexFn (graphFn F)) (hG : ClosedProperConvexFn (graphFn G)) (hex : ∀ (u : U) (y : Y), IsExactSum Bx.flip (concaveBracket Bu (inverseBifun (lowerAdjointBifun Bu Bx F)) u) fun (w : W) => -bracket By.flip (lowerAdjointBifun Bx By G) w y) : ClosedBifun (compBifun G F)

A product of closed proper convex bifunctions is closed. It is a lower adjoint.

theorem Tdaf.ConvexAnalysis.exists_compBifun_eq {U : Type u_1} {V : Type u_2} {X : Type u_3} {W : Type u_4} {Y : Type u_5} {Z : Type u_6} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup W] [Module ℝ W] [AddCommGroup Y] [Module ℝ Y] [AddCommGroup Z] [Module ℝ Z] [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 →ₗ[ℝ] W →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] {By : Y →ₗ[ℝ] Z →ₗ[ℝ] ℝ} [IsCompatiblePairing By] {F : Bifun U X} {G : Bifun X Y} (hF : ClosedProperConvexFn (graphFn F)) (hG : ClosedProperConvexFn (graphFn G)) {u : U} {y : Y} (hex : IsExactSum Bx.flip (concaveBracket Bu (inverseBifun (lowerAdjointBifun Bu Bx F)) u) fun (w : W) => -bracket By.flip (lowerAdjointBifun Bx By G) w y) : ∃ (x : X), F u x + G x y = compBifun G F u y

The infimum defining ((GF)u)(y) is attained, for closed proper convex F and G. This is exists_adjointBifun_compBifun_eq read at F⁎* and G⁎*.

theorem Tdaf.ConvexAnalysis.lowerAdjointBifun_compBifun_eq_clBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {W : Type u_4} {Y : Type u_5} {Z : Type u_6} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup W] [Module ℝ W] [AddCommGroup Y] [Module ℝ Y] [AddCommGroup Z] [Module ℝ Z] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] [LocallyConvexSpace ℝ V] [TopologicalSpace Z] [IsTopologicalAddGroup Z] [ContinuousSMul ℝ Z] [LocallyConvexSpace ℝ Z] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] {Bx : X →ₗ[ℝ] W →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] {By : Y →ₗ[ℝ] Z →ₗ[ℝ] ℝ} [IsCompatiblePairing By] [IsCompatiblePairing By.flip] {F : Bifun U X} {G : Bifun X Y} (hF : ClosedProperConvexFn (graphFn F)) (hG : ClosedProperConvexFn (graphFn G)) (hex : ∀ (u : U) (y : Y), IsExactSum Bx.flip (concaveBracket Bu (inverseBifun (lowerAdjointBifun Bu Bx F)) u) fun (w : W) => -bracket By.flip (lowerAdjointBifun Bx By G) w y) : lowerAdjointBifun Bu By (compBifun G F) = clBifun (compBifun (lowerAdjointBifun Bx By G) (lowerAdjointBifun Bu Bx F))

(GF)* = cl (F* G*) for closed proper convex F and G, in the F⁎* packaging (GF)⁎* = cl (G⁎* F⁎*).

GF is the lower adjoint of G⁎* F⁎*, so (GF)⁎* is that bifunction's double lower adjoint, which is its closure. Rockafellar's cl (F* G*) is this with the two negations moved outside.

Infimal convolution in the first variable

noncomputable def Tdaf.ConvexAnalysis.infConvFstBifun {V : Type u_1} {Y : Type u_2} [AddCommGroup V] (H₁ H₂ : Bifun V Y) : Bifun V Y

Infimal convolution of bifunctions in the first variable, pointwise in the second: (H₁ ⊡ H₂) v y = ⨅ {v₁ + v₂ = v}, H₁ v₁ y + H₂ v₂ y.

infConvBifun convolves in the second variable; this is its mirror, and it is the operation the lower adjoints have to be combined by (lowerAdjointBifun_infConvFstBifun).

Equations

• Tdaf.ConvexAnalysis.infConvFstBifun H₁ H₂ v y = Tdaf.ConvexAnalysis.infConv (fun (w : V) => H₁ w y) (fun (w : V) => H₂ w y) v

theorem Tdaf.ConvexAnalysis.infConvFstBifun_slice {V : Type u_1} {Y : Type u_2} [AddCommGroup V] (H₁ H₂ : Bifun V Y) (y : Y) : (fun (v : V) => infConvFstBifun H₁ H₂ v y) = infConv (fun (w : V) => H₁ w y) fun (w : V) => H₂ w y

theorem Tdaf.ConvexAnalysis.infConvFstBifun_comm {V : Type u_1} {Y : Type u_2} [AddCommGroup V] (H₁ H₂ : Bifun V Y) : infConvFstBifun H₁ H₂ = infConvFstBifun H₂ H₁

theorem Tdaf.ConvexAnalysis.infConvFstBifun_assoc {V : Type u_1} {Y : Type u_2} [AddCommGroup V] (H₁ H₂ H₃ : Bifun V Y) : infConvFstBifun (infConvFstBifun H₁ H₂) H₃ = infConvFstBifun H₁ (infConvFstBifun H₂ H₃)

def Tdaf.ConvexAnalysis.infConvFstLeft (V : Type u_3) (Y : Type u_4) [AddCommGroup V] [Module ℝ V] [AddCommGroup Y] [Module ℝ Y] : (V × Y) × V →ₗ[ℝ] V × Y

The linear map ((v, y), w) ↦ (v - w, y), the left half of the change of variables that turns a first-variable infimal convolution into a partial minimisation.

Equations

• Tdaf.ConvexAnalysis.infConvFstLeft V Y = (LinearMap.fst ℝ V Y ∘ₗ LinearMap.fst ℝ (V × Y) V - LinearMap.snd ℝ (V × Y) V).prod (LinearMap.snd ℝ V Y ∘ₗ LinearMap.fst ℝ (V × Y) V)

@[simp]

theorem Tdaf.ConvexAnalysis.infConvFstLeft_apply {V : Type u_1} {Y : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup Y] [Module ℝ Y] (q : (V × Y) × V) : (infConvFstLeft V Y) q = (q.1.1 - q.2, q.1.2)

def Tdaf.ConvexAnalysis.infConvFstRight (V : Type u_3) (Y : Type u_4) [AddCommGroup V] [Module ℝ V] [AddCommGroup Y] [Module ℝ Y] : (V × Y) × V →ₗ[ℝ] V × Y

The linear map ((v, y), w) ↦ (w, y), the right half of the same change of variables.

Equations

• Tdaf.ConvexAnalysis.infConvFstRight V Y = (LinearMap.snd ℝ (V × Y) V).prod (LinearMap.snd ℝ V Y ∘ₗ LinearMap.fst ℝ (V × Y) V)

@[simp]

theorem Tdaf.ConvexAnalysis.infConvFstRight_apply {V : Type u_1} {Y : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup Y] [Module ℝ Y] (q : (V × Y) × V) : (infConvFstRight V Y) q = (q.2, q.1.2)

theorem Tdaf.ConvexAnalysis.graphFn_infConvFstBifun {V : Type u_1} {Y : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup Y] [Module ℝ Y] {H₁ H₂ : Bifun V Y} (hb₁ : ∀ (v : V) (y : Y), H₁ v y ≠ ⊥) (hb₂ : ∀ (v : V) (y : Y), H₂ v y ≠ ⊥) (p : V × Y) : graphFn (infConvFstBifun H₁ H₂) p = ⨅ (w : V), (compLin (graphFn H₁) (infConvFstLeft V Y) + compLin (graphFn H₂) (infConvFstRight V Y)) (p, w)

The graph function of H₁ ⊡ H₂ is a partial minimisation of a convex function on (V × Y) × V: the infimum formula for ⊡, read jointly in (v, y).

theorem Tdaf.ConvexAnalysis.convexBifun_infConvFstBifun {V : Type u_1} {Y : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup Y] [Module ℝ Y] {H₁ H₂ : Bifun V Y} (hb₁ : ∀ (v : V) (y : Y), H₁ v y ≠ ⊥) (hb₂ : ∀ (v : V) (y : Y), H₂ v y ≠ ⊥) (hH₁ : ConvexBifun H₁) (hH₂ : ConvexBifun H₂) : ConvexBifun (infConvFstBifun H₁ H₂)

H₁ ⊡ H₂ is a convex bifunction, by the same partial-minimisation argument that makes H₁ □ H₂ one.

The lower adjoint of a first-variable convolute

theorem Tdaf.ConvexAnalysis.concaveBracket_inverseBifun_apply {U : Type u_1} {V : Type u_2} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (H : Bifun V Y) (u : U) (y : Y) : concaveBracket Bu (inverseBifun H) u y = ⨅ (v : V), H v y + ↑((Bu u) v)

The bracket that the lower adjoint conjugates: ⟨u, H⁎ y⟩ = ⨅ v, ((H v)(y) + ⟨u, v⟩).

theorem Tdaf.ConvexAnalysis.neg_concaveBracket_inverseBifun {U : Type u_1} {V : Type u_2} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (H : Bifun V Y) (u : U) (y : Y) : -concaveBracket Bu (inverseBifun H) u y = conj Bu.flip (fun (v : V) => H v y) (-u)

Minus the bracket is a conjugate in the first variable, taken at -u.

theorem Tdaf.ConvexAnalysis.lowerAdjointBifun_eq_conj_concaveBracket_inverseBifun {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 →ₗ[ℝ] ℝ) (H : Bifun V Y) (u : U) : lowerAdjointBifun Bu.flip Bx.flip H u = conj Bx.flip (concaveBracket Bu (inverseBifun H) u)

The lower adjoint at a fixed u is an ordinary conjugate — of the bracket y ↦ ⟨u, H⁎ y⟩. This is the identity the whole closed case for □ runs through.

theorem Tdaf.ConvexAnalysis.concaveBracket_inverseBifun_infConvFstBifun {U : Type u_1} {V : Type u_2} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (H₁ H₂ : Bifun V Y) (u : U) (h₁ : ∀ (y : Y), concaveBracket Bu (inverseBifun H₁) u y ≠ ⊥) (h₂ : ∀ (y : Y), concaveBracket Bu (inverseBifun H₂) u y ≠ ⊥) : concaveBracket Bu (inverseBifun (infConvFstBifun H₁ H₂)) u = concaveBracket Bu (inverseBifun H₁) u + concaveBracket Bu (inverseBifun H₂) u

The bracket of a first-variable convolute is the sum of the brackets: the unconditional identity (f □ g)* = f* + g*, read in the first variable of a bifunction.

theorem Tdaf.ConvexAnalysis.lowerAdjointBifun_infConvFstBifun {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 →ₗ[ℝ] ℝ) (H₁ H₂ : Bifun V Y) {u : U} (hex : IsExactSum Bx.flip (concaveBracket Bu (inverseBifun H₁) u) (concaveBracket Bu (inverseBifun H₂) u)) : lowerAdjointBifun Bu.flip Bx.flip (infConvFstBifun H₁ H₂) u = infConvBifun (lowerAdjointBifun Bu.flip Bx.flip H₁) (lowerAdjointBifun Bu.flip Bx.flip H₂) u

The lower adjoint turns a first-variable convolution into a second-variable one: (H₁ ⊡ H₂)⁎* = H₁⁎* □ H₂⁎*.

This is the one new theorem the closed case for □ needs. Written φᵢ y = ⨅ v, (Hᵢ v y + ⟨u, v⟩), the lower adjoint of Hᵢ at u is φᵢ*; φ = φ₁ + φ₂ for a first-variable convolute with no hypothesis at all, and an exact conjugate of a sum turns (φ₁ + φ₂)* into the infimal convolution. The hypothesis is Rockafellar's relative-interior condition in IsExactSum form, one per u.

Infimal convolutes of closed proper convex bifunctions

theorem Tdaf.ConvexAnalysis.lowerAdjointBifun_infConvFstBifun_lowerAdjointBifun {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₁ F₂ : Bifun U X} (hF₁ : ConvexBifun F₁) (hF₁cl : ClosedBifun F₁) (hF₂ : ConvexBifun F₂) (hF₂cl : ClosedBifun F₂) {u : U} (hex : IsExactSum Bx.flip (concaveBracket Bu (inverseBifun (lowerAdjointBifun Bu Bx F₁)) u) (concaveBracket Bu (inverseBifun (lowerAdjointBifun Bu Bx F₂)) u)) : lowerAdjointBifun Bu.flip Bx.flip (infConvFstBifun (lowerAdjointBifun Bu Bx F₁) (lowerAdjointBifun Bu Bx F₂)) u = infConvBifun F₁ F₂ u

(F₁⁎* ⊡ F₂⁎*)⁎* = F₁ □ F₂ for closed proper convex F₁ and F₂ — the identity the rest of the closed case follows from.

This is lowerAdjointBifun_infConvFstBifun applied to the pair (F₁⁎*, F₂⁎*), whose own lower adjoints are F₁ and F₂ again. Rockafellar's condition that ri (dom F₁*) and ri (dom F₂*) have a point in common is the IsExactSum hypothesis, one instance per u.

theorem Tdaf.ConvexAnalysis.infConvBifun_eq_lowerAdjointBifun_infConvFstBifun {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₁ F₂ : Bifun U X} (hF₁ : ConvexBifun F₁) (hF₁cl : ClosedBifun F₁) (hF₂ : ConvexBifun F₂) (hF₂cl : ClosedBifun F₂) (hex : ∀ (u : U), IsExactSum Bx.flip (concaveBracket Bu (inverseBifun (lowerAdjointBifun Bu Bx F₁)) u) (concaveBracket Bu (inverseBifun (lowerAdjointBifun Bu Bx F₂)) u)) : infConvBifun F₁ F₂ = lowerAdjointBifun Bu.flip Bx.flip (infConvFstBifun (lowerAdjointBifun Bu Bx F₁) (lowerAdjointBifun Bu Bx F₂))

theorem Tdaf.ConvexAnalysis.closedBifun_infConvBifun {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₁ F₂ : Bifun U X} (hF₁ : ConvexBifun F₁) (hF₁cl : ClosedBifun F₁) (hF₂ : ConvexBifun F₂) (hF₂cl : ClosedBifun F₂) (hex : ∀ (u : U), IsExactSum Bx.flip (concaveBracket Bu (inverseBifun (lowerAdjointBifun Bu Bx F₁)) u) (concaveBracket Bu (inverseBifun (lowerAdjointBifun Bu Bx F₂)) u)) : ClosedBifun (infConvBifun F₁ F₂)

An infimal convolute of closed proper convex bifunctions is closed. It is a lower adjoint, and a lower adjoint is closed with no hypothesis at all.

theorem Tdaf.ConvexAnalysis.lowerAdjointBifun_infConvBifun_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] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] [LocallyConvexSpace ℝ V] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] {F₁ F₂ : Bifun U X} (hF₁ : ClosedProperConvexFn (graphFn F₁)) (hF₂ : ClosedProperConvexFn (graphFn F₂)) (hex : ∀ (u : U), IsExactSum Bx.flip (concaveBracket Bu (inverseBifun (lowerAdjointBifun Bu Bx F₁)) u) (concaveBracket Bu (inverseBifun (lowerAdjointBifun Bu Bx F₂)) u)) : lowerAdjointBifun Bu Bx (infConvBifun F₁ F₂) = clBifun (infConvFstBifun (lowerAdjointBifun Bu Bx F₁) (lowerAdjointBifun Bu Bx F₂))

(F₁ □ F₂)* = cl (F₁* □ F₂*) for closed proper convex F₁ and F₂, in the F⁎* packaging (F₁ □ F₂)⁎* = cl (F₁⁎* ⊡ F₂⁎*).

F₁ □ F₂ is the lower adjoint of F₁⁎* ⊡ F₂⁎*, so (F₁ □ F₂)⁎* is that bifunction's double lower adjoint, its closure. The right-hand convolution is in the first variable, which is what Rockafellar's F₁* □ F₂* becomes once the two negations are moved outside.

The inner products of a product of bifunctions

theorem Tdaf.ConvexAnalysis.compBifun_slice {U : Type u_1} {X : Type u_2} {Y : Type u_4} (G : Bifun X Y) (F : Bifun U X) (u : U) : compBifun G F u = imageBifun G (F u)

A slice of a product is the image of a slice: (GF)u = G(Fu). Both sides are ⨅ x, (Fu)(x) + (Gx)(y), so this is rfl; it is what makes every statement about ⟨GFu, ·⟩ a statement about an image, and hence a case of conj_imageBifun and its inner-product form.

theorem Tdaf.ConvexAnalysis.hasFenchelPairing_adjointBifun_slice {U : Type u_1} {X : Type u_2} {W : Type u_3} {Y : Type u_4} {Z : Type u_5} [AddCommGroup X] [Module ℝ X] [AddCommGroup W] [Module ℝ W] [AddCommGroup Y] [Module ℝ Y] [AddCommGroup Z] [Module ℝ Z] {F : Bifun U X} {G : Bifun X Y} (Bx : X →ₗ[ℝ] W →ₗ[ℝ] ℝ) (By : Y →ₗ[ℝ] Z →ₗ[ℝ] ℝ) (hbG : ∀ (x : X) (y : Y), G x y ≠ ⊥) {u : U} (hFu : Proper (F u)) {z : Z} (hex : IsExactSum Bx (F u) fun (x : X) => -bracket By G x z) : HasFenchelPairing Bx (F u) (adjointBifun Bx By G z)

The inner product ⟨Fu, G* z⟩ exists, its two extrema agreeing.

Rockafellar derives the hypothesis, ri (dom (Fu)) meets ri (dom G), from his condition on ri (dom F⁎) ∩ ri (dom G) by a calculus of relative interiors that he leaves to the reader; here it is the IsExactSum the proof actually consumes, one instance per (u, z).

theorem Tdaf.ConvexAnalysis.bracket_compBifun_eq_fenchelPairing {U : Type u_1} {X : Type u_2} {W : Type u_3} {Y : Type u_4} {Z : Type u_5} [AddCommGroup X] [Module ℝ X] [AddCommGroup W] [Module ℝ W] [AddCommGroup Y] [Module ℝ Y] [AddCommGroup Z] [Module ℝ Z] {F : Bifun U X} {G : Bifun X Y} (Bx : X →ₗ[ℝ] W →ₗ[ℝ] ℝ) (By : Y →ₗ[ℝ] Z →ₗ[ℝ] ℝ) (hbG : ∀ (x : X) (y : Y), G x y ≠ ⊥) {u : U} (hFu : Proper (F u)) {z : Z} (hex : IsExactSum Bx (F u) fun (x : X) => -bracket By G x z) : bracket By (compBifun G F) u z = fenchelPairing Bx (F u) (adjointBifun Bx By G z)

⟨GFu, z⟩ = ⟨Fu, G* z⟩, an adjoint moving across the inner product at a slice.

This is conj_imageBifun_eq_fenchelPairing at the slice Fu, since (GF)u = G(Fu). The other equality ⟨GFu, z⟩ = ⟨u, F* G* z⟩ needs a relative interior; it is bracket_compBifun_eq_concaveBracket_concaveCompBifun in Bifunction/Cofinite.lean.