Saddle-functions and partial conjugacy

A concave-convex function on U × X is concave in its first argument for each value of the second and convex in the second for each value of the first; convex-concave functions are the mirror image, and both are called saddle-functions.

Concave-convex functions are the same data as convex bifunctions. A convex bifunction F from U to X gives the bracket ⟨Fu, y⟩ = (F u)*(y), concave-convex in (u, y) and closed convex in y; conversely every such function arises this way, from F u = K (u, ·)*. The bracket is the conjugate of the graph function of F in its second variable only — one-variable conjugacy applied uniformly in a parameter.

The two partial closures are not mirror images. partialCl₂ K closes K (u, ·) as a convex function of the second argument; partialCl₁ K closes K (·, x) as a concave function of the first.

Main definitions

• ConcaveConvexFn, ConvexConcaveFn, SaddleFn — the three predicates.
• dom₁ K = {u | ∀ x, K (u, x) > -∞} and dom₂ K = {x | ∀ u, K (u, x) < +∞} — the effective domains: intersections of one-variable domains, not unions.
• partialCl₁, partialCl₂ — Rockafellar's cl₁ and cl₂, with fixed points ConcaveClosedFn and ConvexClosedFn.
• bracket Bx F, concaveBracket Bu G — ⟨Fu, y⟩ and its concave counterpart ⟨u, G y⟩; partialConj₂ Bx f is the uncurried reading of the first.
• bifunOfSaddle Bx K — the convex bifunction F u = K (u, ·)* attached to a saddle-function.

Main results

• concaveConvexFn_bracket, closedFn_bracket, clFn_eq_conj_bracket — the bracket of a convex bifunction is concave-convex and closed in y, and inverts as cl (F u) = ⟨F u, ·⟩*.
• convexBifun_bifunOfSaddle, bracket_bifunOfSaddle — conversely, the bifunction attached to a concave-convex K is convex and its bracket is cl₂ K.
• convexFn_partialCl₂, concaveConvexFn_partialCl₂, concaveFn_partialCl₁ — the partial closures preserve concave-convexity.
• concaveBracket_adjointBifun_eq_partialCl₁, partialCl₂_concaveBracket_adjointBifun — the two equations ⟨u, F* y⟩ = cl₁ ⟨Fu, y⟩ and cl₂ ⟨u, F* y⟩ = ⟨(cl F) u, y⟩ (Theorem 33.2 in [^1]). One theorem in opposite variables, so the pairing hypotheses differ: U for the first, Y for the second.

References

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

Three rearrangements over EReal

The two effective domains

def Tdaf.ConvexAnalysis.dom₁ {U : Type u_1} {X : Type u_2} (K : U × X → EReal) : Set U

The first effective domain dom₁ K: the u at which K (u, ·) is nowhere -∞, an intersection of concave effective domains.

Equations

• Tdaf.ConvexAnalysis.dom₁ K = {u : U | ∀ (x : X), ⊥ < K (u, x)}

def Tdaf.ConvexAnalysis.dom₂ {U : Type u_1} {X : Type u_2} (K : U × X → EReal) : Set X

The second effective domain: the x at which K (·, x) is nowhere +∞.

Equations

• Tdaf.ConvexAnalysis.dom₂ K = {x : X | ∀ (u : U), K (u, x) < ⊤}

@[simp]

theorem Tdaf.ConvexAnalysis.mem_dom₁ {U : Type u_1} {X : Type u_2} {K : U × X → EReal} {u : U} : u ∈ dom₁ K ↔ ∀ (x : X), ⊥ < K (u, x)

@[simp]

theorem Tdaf.ConvexAnalysis.mem_dom₂ {U : Type u_1} {X : Type u_2} {K : U × X → EReal} {x : X} : x ∈ dom₂ K ↔ ∀ (u : U), K (u, x) < ⊤

theorem Tdaf.ConvexAnalysis.dom₁_eq_iInter {U : Type u_1} {X : Type u_2} (K : U × X → EReal) : dom₁ K = ⋂ (x : X), domConcave fun (u : U) => K (u, x)

theorem Tdaf.ConvexAnalysis.dom₂_eq_iInter {U : Type u_1} {X : Type u_2} (K : U × X → EReal) : dom₂ K = ⋂ (u : U), dom fun (x : X) => K (u, x)

Concave-convex functions

structure Tdaf.ConvexAnalysis.ConcaveConvexFn {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (K : U × X → EReal) : Prop

K is concave-convex: concave in the first argument, convex in the second.

• concave_fst (x : X) : ConcaveFn fun (u : U) => K (u, x)

  K (·, x) is concave for every x.

• convex_snd (u : U) : ConvexFn fun (x : X) => K (u, x)

  K (u, ·) is convex for every u.

structure Tdaf.ConvexAnalysis.ConvexConcaveFn {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (K : U × X → EReal) : Prop

K is convex-concave: convex in the first argument, concave in the second.

• convex_fst (x : X) : ConvexFn fun (u : U) => K (u, x)

  K (·, x) is convex for every x.

• concave_snd (u : U) : ConcaveFn fun (x : X) => K (u, x)

  K (u, ·) is concave for every u.

def Tdaf.ConvexAnalysis.SaddleFn {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (K : U × X → EReal) : Prop

A saddle-function is one of the two.

Equations

• Tdaf.ConvexAnalysis.SaddleFn K = (Tdaf.ConvexAnalysis.ConcaveConvexFn K ∨ Tdaf.ConvexAnalysis.ConvexConcaveFn K)

theorem Tdaf.ConvexAnalysis.ConcaveConvexFn.convexConcaveFn_neg {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {K : U × X → EReal} (h : ConcaveConvexFn K) : ConvexConcaveFn fun (p : U × X) => -K p

theorem Tdaf.ConvexAnalysis.ConvexConcaveFn.concaveConvexFn_neg {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {K : U × X → EReal} (h : ConvexConcaveFn K) : ConcaveConvexFn fun (p : U × X) => -K p

theorem Tdaf.ConvexAnalysis.ConcaveConvexFn.saddleFn {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {K : U × X → EReal} (h : ConcaveConvexFn K) : SaddleFn K

theorem Tdaf.ConvexAnalysis.ConvexConcaveFn.saddleFn {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {K : U × X → EReal} (h : ConvexConcaveFn K) : SaddleFn K

theorem Tdaf.ConvexAnalysis.ConcaveConvexFn.convex_dom₁ {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {K : U × X → EReal} (h : ConcaveConvexFn K) : Convex ℝ (dom₁ K)

dom₁ of a concave-convex function is convex: it is an intersection of concave domains.

theorem Tdaf.ConvexAnalysis.ConcaveConvexFn.convex_dom₂ {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {K : U × X → EReal} (h : ConcaveConvexFn K) : Convex ℝ (dom₂ K)

dom₂ of a concave-convex function is convex.

Partial conjugacy

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

The conjugate of f in the second variable only: the uncurried reading of bracket, which is what partialConj₂_graphFn makes precise. Downstream code uses the curried form.

Equations

• Tdaf.ConvexAnalysis.partialConj₂ Bx f p = Tdaf.ConvexAnalysis.conj Bx (fun (x : X) => f (p.1, x)) p.2

theorem Tdaf.ConvexAnalysis.partialConj₂_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 : U × X → EReal) (p : U × Y) : partialConj₂ Bx f p = conj Bx (fun (x : X) => f (p.1, x)) p.2

Partial closures

noncomputable def Tdaf.ConvexAnalysis.partialCl₂ {U : Type u_1} {X : Type u_2} [TopologicalSpace X] (K : U × X → EReal) : U × X → EReal

Rockafellar's cl₂: close in the second variable, convexly.

Equations

• Tdaf.ConvexAnalysis.partialCl₂ K p = Tdaf.ConvexAnalysis.clFn (fun (x : X) => K (p.1, x)) p.2

noncomputable def Tdaf.ConvexAnalysis.partialCl₁ {U : Type u_1} {X : Type u_2} [TopologicalSpace U] (K : U × X → EReal) : U × X → EReal

Rockafellar's cl₁: close in the first variable, concavely.

Equations

• Tdaf.ConvexAnalysis.partialCl₁ K p = Tdaf.ConvexAnalysis.clConcave (fun (u : U) => K (u, p.2)) p.1

theorem Tdaf.ConvexAnalysis.partialCl₂_apply {U : Type u_1} {X : Type u_2} [TopologicalSpace X] (K : U × X → EReal) (p : U × X) : partialCl₂ K p = clFn (fun (x : X) => K (p.1, x)) p.2

theorem Tdaf.ConvexAnalysis.partialCl₁_apply {U : Type u_1} {X : Type u_2} [TopologicalSpace U] (K : U × X → EReal) (p : U × X) : partialCl₁ K p = clConcave (fun (u : U) => K (u, p.2)) p.1

theorem Tdaf.ConvexAnalysis.partialCl₂_slice {U : Type u_1} {X : Type u_2} [TopologicalSpace X] (K : U × X → EReal) (u : U) : (fun (x : X) => partialCl₂ K (u, x)) = clFn fun (x : X) => K (u, x)

theorem Tdaf.ConvexAnalysis.partialCl₁_slice {U : Type u_1} {X : Type u_2} [TopologicalSpace U] (K : U × X → EReal) (x : X) : (fun (u : U) => partialCl₁ K (u, x)) = clConcave fun (u : U) => K (u, x)

theorem Tdaf.ConvexAnalysis.partialCl₂_le {U : Type u_1} {X : Type u_2} [TopologicalSpace X] (K : U × X → EReal) : partialCl₂ K ≤ K

theorem Tdaf.ConvexAnalysis.partialCl₂_mono {U : Type u_1} {X : Type u_2} [TopologicalSpace X] {K L : U × X → EReal} (h : K ≤ L) : partialCl₂ K ≤ partialCl₂ L

theorem Tdaf.ConvexAnalysis.le_partialCl₁ {U : Type u_1} {X : Type u_2} [TopologicalSpace U] (K : U × X → EReal) : K ≤ partialCl₁ K

theorem Tdaf.ConvexAnalysis.partialCl₁_mono {U : Type u_1} {X : Type u_2} [TopologicalSpace U] {K L : U × X → EReal} (h : K ≤ L) : partialCl₁ K ≤ partialCl₁ L

def Tdaf.ConvexAnalysis.ConvexClosedFn {U : Type u_1} {X : Type u_2} [TopologicalSpace X] (K : U × X → EReal) : Prop

K is convex-closed when it is unchanged by cl₂.

Equations

• Tdaf.ConvexAnalysis.ConvexClosedFn K = (Tdaf.ConvexAnalysis.partialCl₂ K = K)

def Tdaf.ConvexAnalysis.ConcaveClosedFn {U : Type u_1} {X : Type u_2} [TopologicalSpace U] (K : U × X → EReal) : Prop

K is concave-closed when it is unchanged by cl₁.

Equations

• Tdaf.ConvexAnalysis.ConcaveClosedFn K = (Tdaf.ConvexAnalysis.partialCl₁ K = K)

theorem Tdaf.ConvexAnalysis.convexClosedFn_iff {U : Type u_1} {X : Type u_2} [TopologicalSpace X] {K : U × X → EReal} : ConvexClosedFn K ↔ ∀ (u : U), ClosedFn fun (x : X) => K (u, x)

theorem Tdaf.ConvexAnalysis.concaveClosedFn_iff {U : Type u_1} {X : Type u_2} [TopologicalSpace U] {K : U × X → EReal} : ConcaveClosedFn K ↔ ∀ (x : X), ClosedConcaveFn fun (u : U) => K (u, x)

The bracket of a convex bifunction

noncomputable def Tdaf.ConvexAnalysis.bracket {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

Rockafellar's bracket ⟨Fu, y⟩ = (F u)*(y), read as a function of (u, y).

Equations

• Tdaf.ConvexAnalysis.bracket Bx F u y = Tdaf.ConvexAnalysis.conj Bx (F u) y

theorem Tdaf.ConvexAnalysis.bracket_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) (u : U) (y : Y) : bracket Bx F u y = ⨆ (x : X), ↑((Bx x) y) - F u x

theorem Tdaf.ConvexAnalysis.bracket_eq_conj {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 : U) : bracket Bx F u = conj Bx (F u)

theorem Tdaf.ConvexAnalysis.partialConj₂_graphFn {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) : partialConj₂ Bx (graphFn F) p = bracket Bx F p.1 p.2

The bracket is the partial conjugate of the graph function.

theorem Tdaf.ConvexAnalysis.convexFn_bracket {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 : U) : ConvexFn (bracket Bx F u)

⟨Fu, ·⟩ is convex, with no hypothesis on F.

theorem Tdaf.ConvexAnalysis.closedFn_bracket {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} (u : U) : ClosedFn (bracket Bx F u)

⟨Fu, ·⟩ is closed as well as convex.

The clauses that use convexity of the bifunction

theorem Tdaf.ConvexAnalysis.concaveFn_bracket {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] {F : Bifun U X} (hF : ConvexBifun F) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (y : Y) : ConcaveFn fun (u : U) => bracket Bx F u y

The clause with content: ⟨F·, y⟩ is concave in u whenever F is a convex bifunction. Its negative is the infimal projection of a jointly convex function along (u, x) ↦ u.

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

The bracket of a convex bifunction is concave-convex.

theorem Tdaf.ConvexAnalysis.clFn_eq_conj_bracket {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] {F : Bifun U X} (hF : ConvexBifun F) (u : U) : clFn (F u) = conj Bx.flip (bracket Bx F u)

The inversion formula: cl (F u) is recovered from the bracket by conjugating back. This is the Fenchel–Moreau theorem, uniformly in u.

The bifunction attached to a saddle-function

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

The convex bifunction attached to a saddle-function: F u = K (u, ·)*, the conjugate taken over the flipped pairing.

Equations

• Tdaf.ConvexAnalysis.bifunOfSaddle Bx K u x = Tdaf.ConvexAnalysis.conj Bx.flip (fun (y : Y) => K (u, y)) x

theorem Tdaf.ConvexAnalysis.bifunOfSaddle_apply {U : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (K : U × Y → EReal) (u : U) (x : X) : bifunOfSaddle Bx K u x = ⨆ (y : Y), ↑((Bx x) y) - K (u, y)

theorem Tdaf.ConvexAnalysis.convexBifun_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] {K : U × Y → EReal} (hK : ConcaveConvexFn K) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) : ConvexBifun (bifunOfSaddle Bx K)

The bifunction attached to a concave-convex K is convex: its graph function is a pointwise supremum of jointly convex functions.

theorem Tdaf.ConvexAnalysis.bracket_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) (p : U × Y) : bracket Bx (bifunOfSaddle Bx K) p.1 p.2 = partialCl₂ K p

The bracket of that bifunction is cl₂ K.

Closedness of the partial closures

theorem Tdaf.ConvexAnalysis.convexClosedFn_partialCl₂ {U : Type u_1} {X : Type u_2} [TopologicalSpace X] [AddCommGroup X] [IsTopologicalAddGroup X] (K : U × X → EReal) : ConvexClosedFn (partialCl₂ K)

cl₂ K is convex-closed.

theorem Tdaf.ConvexAnalysis.concaveClosedFn_partialCl₁ {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [AddCommGroup U] [IsTopologicalAddGroup U] (K : U × X → EReal) : ConcaveClosedFn (partialCl₁ K)

cl₁ K is concave-closed.

theorem Tdaf.ConvexAnalysis.convexFn_partialCl₂ {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {K : U × X → EReal} [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] (hK : ConcaveConvexFn K) (u : U) : ConvexFn fun (x : X) => partialCl₂ K (u, x)

cl₂ preserves convexity in the second variable.

theorem Tdaf.ConvexAnalysis.concaveFn_partialCl₁ {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {K : U × X → EReal} [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] (hK : ConcaveConvexFn K) (x : X) : ConcaveFn fun (u : U) => partialCl₁ K (u, x)

cl₁ preserves concavity in the first variable.

The concave bracket and the bridge to adjoint bifunctions

noncomputable def Tdaf.ConvexAnalysis.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 → Y → EReal

Rockafellar's bracket for a concave bifunction. Where bracket conjugates convexly in the second variable, this one conjugates concavely in the first.

Equations

• Tdaf.ConvexAnalysis.concaveBracket Bu G u y = Tdaf.ConvexAnalysis.concaveConj Bu.flip (G y) u

theorem Tdaf.ConvexAnalysis.concaveBracket_apply {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) (y : Y) : concaveBracket Bu G u y = ⨅ (v : V), ↑((Bu u) v) - G y v

theorem Tdaf.ConvexAnalysis.concaveBracket_eq_concaveConj {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) (y : Y) : (fun (u : U) => concaveBracket Bu G u y) = concaveConj Bu.flip (G y)

theorem Tdaf.ConvexAnalysis.concaveAdjointBifun_eq_conj_concaveBracket {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (G : Bifun Y V) (u : U) (x : X) : concaveAdjointBifun Bu Bx G u x = conj Bx.flip (fun (y : Y) => concaveBracket Bu G u y) x

The concave adjoint is the conjugate of the concave bracket — the mirror of adjointBifun_eq_concaveConj_bracket, with the two conjugations in the opposite order.

theorem Tdaf.ConvexAnalysis.concaveFn_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) (y : Y) : ConcaveFn fun (u : U) => concaveBracket Bu G u y

For a concave bifunction, ⟨·, G y⟩ is concave, being a concave conjugate.

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

For a concave bifunction, ⟨u, G ·⟩ is convex. The mirror of concaveFn_bracket, and again an infimal projection of a jointly convex function.

theorem Tdaf.ConvexAnalysis.concaveConvexFn_concaveBracket {U : Type u_1} {V : Type u_2} {Y : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup Y] [Module ℝ Y] {G : Bifun Y V} (hG : ConcaveBifun G) (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) : ConcaveConvexFn fun (p : U × Y) => concaveBracket Bu G p.1 p.2

The concave bracket of a concave bifunction is concave-convex.

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

The adjoint is the concave conjugate of the bracket. ⟨Fu, y⟩ and F* are the two halves of one conjugation of the graph function: first convexly in x, then concavely in u. This is what makes ⟨u, F* y⟩ = cl₁ ⟨Fu, y⟩ a case of concave Fenchel–Moreau.

The adjoint against the two partial closures

theorem Tdaf.ConvexAnalysis.concaveConj_adjointBifun_eq_partialCl₁ {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} {F : Bifun U X} (hF : ConvexBifun F) (y : Y) : (concaveConj Bu.flip fun (v : V) => adjointBifun Bu Bx F y v) = fun (u : U) => partialCl₁ (fun (p : U × Y) => bracket Bx F p.1 p.2) (u, y)

⟨u, F* y⟩ = cl₁ ⟨Fu, y⟩. Once adjointBifun_eq_concaveConj_bracket identifies F* y with concaveConj Bu ⟨F·, y⟩, this is concave Fenchel–Moreau applied to the concavity of ⟨F·, y⟩.

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

⟨u, F* y⟩ = cl₁ ⟨Fu, y⟩, in bracket notation.

theorem Tdaf.ConvexAnalysis.bracket_concaveAdjointBifun_eq_partialCl₂ {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx.flip] {G : Bifun Y V} (hG : ConcaveBifun G) (u : U) : bracket Bx (concaveAdjointBifun Bu Bx G) u = fun (y : Y) => partialCl₂ (fun (p : U × Y) => concaveBracket Bu G p.1 p.2) (u, y)

The general form in which the second equation is proved: for a concave bifunction G, the bracket of G* is the convex closure in y of the concave bracket of G. Fenchel–Moreau on Y, uniformly in u.

theorem Tdaf.ConvexAnalysis.partialCl₂_concaveBracket_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 U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] {F : Bifun U X} (hF : ConvexBifun F) (u : U) : (fun (y : Y) => partialCl₂ (fun (p : U × Y) => concaveBracket Bu (adjointBifun Bu Bx F) p.1 p.2) (u, y)) = bracket Bx (clBifun F) u

cl₂ ⟨u, F* y⟩ = ⟨(cl F) u, y⟩. The adjoint of F is concave with no hypothesis on F, so this is the concave form at F* followed by the biconjugation identity F** = cl F.

The clauses that need the correspondence

theorem Tdaf.ConvexAnalysis.concaveConvexFn_partialCl₂ {U : Type u_1} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] {K : U × Y → EReal} (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx.flip] (hK : ConcaveConvexFn K) : ConcaveConvexFn (partialCl₂ K)

The clause that is not pointwise: cl₂ K is again concave-convex. It is a bracket, and brackets are concave-convex.