The correspondence between saddle-functions and bifunctions

The two brackets ⟨Fu, y⟩ = cl₂ K and ⟨u, F* y⟩ = cl₁ K set up a one-to-one correspondence between the lower closed concave-convex functions on U × Y and the closed convex bifunctions from U to X; the rest of the saddle-function theory is built on it.

Three refinements follow. Weakening closedness to image-closedness on the bifunction side and to convex-closedness on the function side keeps the bijection; the closure pairs (K̲, K̄) are exactly the pairs of brackets of a closed convex bifunction; and cl₁ and cl₂ are inverse bijections between the lower closed and the upper closed functions. The first has a polyhedral form, with properness in place of closedness.

Main definitions

• saddleOfBifun Bx F — ⟨Fu, x*⟩ uncurried, so that the correspondence is about a map.
• bifunSaddleEquiv — the image-closed form of the correspondence, as an Equiv.
• lowerUpperClosedEquiv — cl₁ and cl₂ as inverse bijections, as an Equiv.

Main results

• eq_of_bracket_eq — the bracket determines an image-closed convex bifunction. This is why image-closedness has to be named: bracket Bx F u = conj Bx (F u) sees only cl (F u).
• lowerClosedFn_bracket, exists_unique_convexBifun_bracket_eq — the bracket of a closed convex bifunction is lower closed, and every lower closed concave-convex function is the bracket of exactly one closed convex bifunction (Theorem 33.3 in [^1]).
• exists_unique_bifun_of_closure_pair — a pair with cl₁ K̲ = K̄ and cl₂ K̄ = K̲ is exactly a bracket pair; le_of_partialCl₂_eq adds K̲ ≤ K̄.
• polyhedralFn_bracket, polyhedralFn_neg_bracket, imageClosedBifun_of_polyhedralBifun, eq_conj_bracket_of_polyhedralBifun — the polyhedral case: both variables of the bracket are polyhedral, and a proper polyhedral bifunction is recovered from its bracket.

Implementation notes

Given a lower closed K, the bifunction bifunOfSaddle Bx K has the right bracket at once, but its closedness still has to be argued: cl F and F are both image-closed and convex and have the same bracket, so they are equal.

References

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

The bracket is injective on image-closed convex bifunctions

theorem Tdaf.ConvexAnalysis.eq_of_bracket_eq {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] {F G : Bifun U X} (hF : ConvexBifun F) (hG : ConvexBifun G) (hFi : ImageClosedBifun F) (hGi : ImageClosedBifun G) (h : bracket Bx F = bracket Bx G) : F = G

Two image-closed convex bifunctions with the same bracket are equal. The bracket sees only cl (F u), and image-closedness says that is all of F u.

The correspondence

theorem Tdaf.ConvexAnalysis.partialCl₁_bracket {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] {F : Bifun U X} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (hF : ConvexBifun F) : (partialCl₁ fun (p : U × Y) => bracket Bx F p.1 p.2) = fun (p : U × Y) => concaveBracket Bu (adjointBifun Bu Bx F) p.1 p.2

The two brackets of a bifunction are related by cl₁ ⟨Fu, y⟩ = ⟨u, F* y⟩.

theorem Tdaf.ConvexAnalysis.partialCl₂_concaveBracket_adjoint {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] {F : Bifun U X} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hF : ConvexBifun F) (hcl : ClosedBifun F) : (partialCl₂ fun (p : U × Y) => concaveBracket Bu (adjointBifun Bu Bx F) p.1 p.2) = fun (p : U × Y) => bracket Bx F p.1 p.2

For a closed bifunction, cl₂ ⟨u, F* y⟩ = ⟨Fu, y⟩: the two brackets of a closed convex bifunction are a closure pair.

theorem Tdaf.ConvexAnalysis.lowerClosedFn_bracket {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] {F : Bifun U X} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hF : ConvexBifun F) (hcl : ClosedBifun F) : LowerClosedFn fun (p : U × Y) => bracket Bx F p.1 p.2

One direction of the correspondence: the bracket of a closed convex bifunction is a lower closed concave-convex function. Each closure step exchanges the two brackets, and the loop closes because F** = cl F = F.

theorem Tdaf.ConvexAnalysis.exists_unique_convexBifun_bracket_eq {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] {K : U × Y → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hK : ConcaveConvexFn K) (hlc : LowerClosedFn K) : ∃! F : Bifun U X, ConvexBifun F ∧ ClosedBifun F ∧ (fun (p : U × Y) => bracket Bx F p.1 p.2) = K

The other direction: a lower closed concave-convex function is the bracket of one and only one closed convex bifunction, namely F u = K(u, ·)*.

Closure pairs are bracket pairs

theorem Tdaf.ConvexAnalysis.le_of_partialCl₂_eq {U : Type u_1} {Y : Type u_2} [TopologicalSpace Y] {Klow Kup : U × Y → EReal} (h2 : partialCl₂ Kup = Klow) : Klow ≤ Kup

A closure pair is ordered, K̲ ≤ K̄. Only the cl₂ relation is needed, because cl₂ lowers.

theorem Tdaf.ConvexAnalysis.exists_unique_bifun_of_closure_pair {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] {Klow Kup : U × Y → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hK : ConcaveConvexFn Klow) (h1 : partialCl₁ Klow = Kup) (h2 : partialCl₂ Kup = Klow) : ∃! F : Bifun U X, ConvexBifun F ∧ ClosedBifun F ∧ (fun (p : U × Y) => bracket Bx F p.1 p.2) = Klow ∧ (fun (p : U × Y) => concaveBracket Bu (adjointBifun Bu Bx F) p.1 p.2) = Kup

The pairs (K̲, K̄) of concave-convex functions with cl₁ K̲ = K̄ and cl₂ K̄ = K̲ are exactly the pairs of brackets (⟨Fu, y⟩, ⟨u, F* y⟩) of a closed convex bifunction, and F is unique.

The correspondence under image-closedness

The two round trips are the two halves of the bracket construction, and each needs the closedness hypothesis on its own side: image-closedness of F, convex-closedness of K.

noncomputable def Tdaf.ConvexAnalysis.saddleOfBifun {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (F : Bifun U X) : U × Y → EReal

The saddle-function attached to a convex bifunction, ⟨Fu, x*⟩ read as a function of the pair: bracket uncurried, named because the correspondence is a statement about it as a map.

Equations

• Tdaf.ConvexAnalysis.saddleOfBifun Bx F p = Tdaf.ConvexAnalysis.bracket Bx F p.1 p.2

theorem Tdaf.ConvexAnalysis.saddleOfBifun_apply {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (F : Bifun U X) (p : U × Y) : saddleOfBifun Bx F p = bracket Bx F p.1 p.2

theorem Tdaf.ConvexAnalysis.convexClosedFn_saddleOfBifun {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace Y] [IsTopologicalAddGroup Y] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsContinuousPairing Bx.flip] {F : Bifun U X} : ConvexClosedFn (saddleOfBifun Bx F)

The saddle-function of a bifunction is convex-closed: every slice is a conjugate.

theorem Tdaf.ConvexAnalysis.concaveConvexFn_saddleOfBifun {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} (hF : ConvexBifun F) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) : ConcaveConvexFn (saddleOfBifun Bx F)

The saddle-function of a convex bifunction is concave-convex.

theorem Tdaf.ConvexAnalysis.imageClosedBifun_bifunOfSaddle {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace X] [IsTopologicalAddGroup X] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsContinuousPairing Bx] {K : U × Y → EReal} : ImageClosedBifun (bifunOfSaddle Bx K)

The bifunction of a saddle-function is image-closed: every slice is a conjugate.

theorem Tdaf.ConvexAnalysis.saddleOfBifun_bifunOfSaddle {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx.flip] {K : U × Y → EReal} (hK : ConcaveConvexFn K) (hcc : ConvexClosedFn K) : saddleOfBifun Bx (bifunOfSaddle Bx K) = K

One round trip: a convex-closed concave-convex K is the saddle-function of the bifunction it defines.

theorem Tdaf.ConvexAnalysis.bifunOfSaddle_saddleOfBifun {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] {F : Bifun U X} (hF : ConvexBifun F) (hFi : ImageClosedBifun F) : bifunOfSaddle Bx (saddleOfBifun Bx F) = F

The other round trip: an image-closed convex bifunction is the bifunction of the saddle-function it defines.

noncomputable def Tdaf.ConvexAnalysis.bifunSaddleEquiv {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] : { F : Bifun U X // ConvexBifun F ∧ ImageClosedBifun F } ≃ { K : U × Y → EReal // ConcaveConvexFn K ∧ ConvexClosedFn K }

K (u, x*) = ⟨Fu, x*⟩ and Fu = K(u, ·)* are inverse bijections between the image-closed convex bifunctions from U to X and the convex-closed concave-convex functions on U × Y.

Equations

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

The bracket of a polyhedral bifunction

For a polyhedral convex bifunction both variables of the bracket sharpen from convex to polyhedral, and properness does the work that closedness does in the general correspondence: F is recovered from its bracket with no closedness hypothesis at all. "Polyhedral concave" is spelled PolyhedralFn (fun u => -(⟨Fu, y⟩)), there being no predicate for a polyhedral hypograph.

theorem Tdaf.ConvexAnalysis.PolyhedralFn.add_linear {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} (hf : PolyhedralFn f) (φ : E →ₗ[ℝ] ℝ) : PolyhedralFn fun (x : E) => f x + ↑(φ x)

Adding a linear functional preserves polyhedrality. The epigraph of f + φ is the preimage of epi f under the shear (x, μ) ↦ (x, μ - φ x), which needs nothing beyond a real vector space — no finite dimension, no topology.

theorem Tdaf.ConvexAnalysis.polyhedralFn_bracket {U : Type u_1} {X : Type u_2} {Y : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {F : Bifun U X} (hF : PolyhedralBifun F) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (u : U) : PolyhedralFn (bracket Bx F u)

⟨Fu, ·⟩ is polyhedral convex for each u: it is the conjugate of the slice F u, which is itself polyhedral.

theorem Tdaf.ConvexAnalysis.polyhedralFn_neg_bracket {U : Type u_1} {X : Type u_2} {Y : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {F : Bifun U X} (hF : PolyhedralBifun F) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (y : Y) : PolyhedralFn fun (u : U) => -bracket Bx F u y

⟨F·, y⟩ is polyhedral concave for each y. -⟨Fu, y⟩ = ⨅ x ((Fu)(x) - ⟨x, y⟩) is the image of a polyhedral convex function on U × X under (u, x) ↦ u, and such an image is polyhedral.

theorem Tdaf.ConvexAnalysis.imageClosedBifun_of_polyhedralBifun {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {F : Bifun U X} (hF : PolyhedralBifun F) (hp : Proper (graphFn F)) : ImageClosedBifun F

A proper polyhedral convex bifunction is image-closed — each slice has a closed epigraph and properness keeps it from taking -∞. This is the polyhedral substitute for the closedness hypothesis of the correspondence.

theorem Tdaf.ConvexAnalysis.eq_conj_bracket_of_polyhedralBifun {U : Type u_1} {X : Type u_2} {Y : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {F : Bifun U X} (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] (hF : PolyhedralBifun F) (hp : Proper (graphFn F)) (u : U) : F u = conj Bx.flip (bracket Bx F u)

A proper polyhedral convex bifunction is recovered from its bracket, Fu = ⟨Fu, ·⟩*.

theorem Tdaf.ConvexAnalysis.eq_iSup_sub_bracket_of_polyhedralBifun {U : Type u_1} {X : Type u_2} {Y : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {F : Bifun U X} (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] (hF : PolyhedralBifun F) (hp : Proper (graphFn F)) (u : U) (x : X) : F u x = ⨆ (y : Y), ↑((Bx x) y) - bracket Bx F u y

The same recovery written out: (Fu)(x) = sup_y {⟨x, y⟩ - ⟨Fu, y⟩}.

The bracket of the adjoint of a polyhedral bifunction

The adjoint of a polyhedral convex bifunction is polyhedral concave and its concave bracket is polyhedral convex in y. With the fact that a polyhedral function agrees with its closure throughout its effective domain, that pushes the equality of the two brackets out from the relative interior of an effective domain to all of it.

theorem Tdaf.ConvexAnalysis.clConcave_eq_of_mem_domConcave {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {g : E → EReal} (hg : PolyhedralFn fun (z : E) => -g z) {x : E} (hx : x ∈ domConcave g) : clConcave g x = g x

A polyhedral concave function agrees with its closure throughout its effective domain, not merely on the relative interior. The mirror of PolyhedralFn.clFn_eq_of_mem_dom, by negating twice.

theorem Tdaf.ConvexAnalysis.closedBifun_of_polyhedralBifun {U : Type u_1} {X : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {F : Bifun U X} (hF : PolyhedralBifun F) (hp : Proper (graphFn F)) : ClosedBifun F

A proper polyhedral convex bifunction is closed. Its graph function has a polyhedral, hence closed, epigraph, and properness rules out the -∞ branch of clFn.

theorem Tdaf.ConvexAnalysis.polyhedralFn_neg_graphFn_adjointBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {F : Bifun U X} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (hF : PolyhedralBifun F) : PolyhedralFn fun (q : Y × V) => -graphFn (adjointBifun Bu Bx F) q

The adjoint of a polyhedral convex bifunction is polyhedral concave. -F* is the conjugate of the graph function composed with the reflection (y, v) ↦ (-v, y). Neither properness nor closedness is needed, exactly as in the concavity half of the adjoint construction.

theorem Tdaf.ConvexAnalysis.dom_concaveBracket {U : Type u_1} {V : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (G : Bifun Y V) (u : U) : (dom fun (y : Y) => concaveBracket Bu G u y) = domConcaveBifun G

The effective domain of y ↦ ⟨u, G y⟩ is dom G, for every u: the concave bracket is +∞ exactly where the slice G y is identically -∞. Mirror of domConcave_bracket.

theorem Tdaf.ConvexAnalysis.polyhedralFn_concaveBracket {U : Type u_1} {V : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] {G : Bifun Y V} (hG : PolyhedralFn fun (q : Y × V) => -graphFn G q) (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (u : U) : PolyhedralFn fun (y : Y) => concaveBracket Bu G u y

The concave bracket of a polyhedral concave bifunction is polyhedral convex in its second variable: ⟨u, G y⟩ = ⨅ v (⟨u, v⟩ - (G y)(v)) is the image of a polyhedral convex function on Y × V under (y, v) ↦ y, and such an image is polyhedral.

The two closures as inverse bijections

theorem Tdaf.ConvexAnalysis.upperClosedFn_partialCl₁ {U : Type u_1} {Y : Type u_2} [TopologicalSpace U] [TopologicalSpace Y] {K : U × Y → EReal} (h : LowerClosedFn K) : UpperClosedFn (partialCl₁ K)

theorem Tdaf.ConvexAnalysis.lowerClosedFn_partialCl₂ {U : Type u_1} {Y : Type u_2} [TopologicalSpace U] [TopologicalSpace Y] {K : U × Y → EReal} (h : UpperClosedFn K) : LowerClosedFn (partialCl₂ K)

theorem Tdaf.ConvexAnalysis.partialCl₂_partialCl₁_of_lowerClosedFn {U : Type u_1} {Y : Type u_2} [TopologicalSpace U] [TopologicalSpace Y] {K : U × Y → EReal} (h : LowerClosedFn K) : partialCl₂ (partialCl₁ K) = K

theorem Tdaf.ConvexAnalysis.partialCl₁_partialCl₂_of_upperClosedFn {U : Type u_1} {Y : Type u_2} [TopologicalSpace U] [TopologicalSpace Y] {K : U × Y → EReal} (h : UpperClosedFn K) : partialCl₁ (partialCl₂ K) = K

noncomputable def Tdaf.ConvexAnalysis.lowerUpperClosedEquiv {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 Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx.flip] : { K : U × Y → EReal // ConcaveConvexFn K ∧ LowerClosedFn K } ≃ { K : U × Y → EReal // ConcaveConvexFn K ∧ UpperClosedFn K }

K̄ = cl₁ K̲ and K̲ = cl₂ K̄ are inverse bijections between the lower closed and the upper closed concave-convex functions on U × Y. The round trips are the definitions of LowerClosedFn and UpperClosedFn; the content is that each operator lands in the other class.

Equations

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