The lower and upper closures of a saddle-function

Applying the two partial closures of a concave-convex function in the two possible orders gives the lower closure lowerCl K = cl₂ (cl₁ K) and the upper closure upperCl K = cl₁ (cl₂ K). These do not agree in general — the discrepancy is what forces saddle-functions to be grouped into equivalence classes — but each is idempotent.

Both halves run the correspondence between saddle-functions and convex bifunctions twice; the iteration stops because the adjoint does not see the closure, (cl F)* = F*.

Main definitions

• lowerCl, upperCl — the two closures; LowerClosedFn, UpperClosedFn, FullyClosedFn for the functions they fix.
• saddleSwap K = fun (x, u) => -K (u, x) — the involution exchanging the roles of cl₁ and cl₂, bundled as the order isomorphism saddleSwapOrderIso onto the order dual.

Main results

• fullyClosedFn_iff — fully closed means lower closed and upper closed.
• upperClosedFn_upperCl, lowerClosedFn_lowerCl — each closure is idempotent (Theorem 34.1 in [^1]). The pairings occur only in the hypotheses, never in the conclusion, so they must be given explicitly at each use site.

References

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

The two closures

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

The lower closure cl₂ cl₁ K of a concave-convex function.

Equations

• Tdaf.ConvexAnalysis.lowerCl K = Tdaf.ConvexAnalysis.partialCl₂ (Tdaf.ConvexAnalysis.partialCl₁ K)

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

The upper closure cl₁ cl₂ K of a concave-convex function.

Equations

• Tdaf.ConvexAnalysis.upperCl K = Tdaf.ConvexAnalysis.partialCl₁ (Tdaf.ConvexAnalysis.partialCl₂ K)

theorem Tdaf.ConvexAnalysis.lowerCl_def {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] (K : U × X → EReal) : lowerCl K = partialCl₂ (partialCl₁ K)

theorem Tdaf.ConvexAnalysis.upperCl_def {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] (K : U × X → EReal) : upperCl K = partialCl₁ (partialCl₂ K)

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

K is lower closed when it is its own lower closure.

Equations

• Tdaf.ConvexAnalysis.LowerClosedFn K = (Tdaf.ConvexAnalysis.lowerCl K = K)

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

K is upper closed when it is its own upper closure.

Equations

• Tdaf.ConvexAnalysis.UpperClosedFn K = (Tdaf.ConvexAnalysis.upperCl K = K)

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

K is fully closed when it is closed in each variable separately.

Equations

• Tdaf.ConvexAnalysis.FullyClosedFn K = (Tdaf.ConvexAnalysis.ConvexClosedFn K ∧ Tdaf.ConvexAnalysis.ConcaveClosedFn K)

theorem Tdaf.ConvexAnalysis.lowerClosedFn_iff {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] {K : U × X → EReal} : LowerClosedFn K ↔ lowerCl K = K

theorem Tdaf.ConvexAnalysis.upperClosedFn_iff {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] {K : U × X → EReal} : UpperClosedFn K ↔ upperCl K = K

theorem Tdaf.ConvexAnalysis.fullyClosedFn_iff' {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] {K : U × X → EReal} : FullyClosedFn K ↔ ConvexClosedFn K ∧ ConcaveClosedFn K

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

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

theorem Tdaf.ConvexAnalysis.fullyClosedFn_iff {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [AddCommGroup U] [IsTopologicalAddGroup U] [TopologicalSpace X] [AddCommGroup X] [IsTopologicalAddGroup X] {K : U × X → EReal} : FullyClosedFn K ↔ LowerClosedFn K ∧ UpperClosedFn K

Fully closed is exactly lower closed and upper closed.

The swap involution

noncomputable def Tdaf.ConvexAnalysis.saddleSwap {U : Type u_1} {X : Type u_2} (K : U × X → EReal) : X × U → EReal

Negate a saddle-function and exchange its arguments: an involution of saddle-functions that exchanges cl₁ with cl₂.

Equations

• Tdaf.ConvexAnalysis.saddleSwap K q = -K (q.2, q.1)

theorem Tdaf.ConvexAnalysis.saddleSwap_apply {U : Type u_1} {X : Type u_2} (K : U × X → EReal) (q : X × U) : saddleSwap K q = -K (q.2, q.1)

@[simp]

theorem Tdaf.ConvexAnalysis.saddleSwap_saddleSwap {U : Type u_1} {X : Type u_2} (K : U × X → EReal) : saddleSwap (saddleSwap K) = K

theorem Tdaf.ConvexAnalysis.saddleSwap_le_saddleSwap {U : Type u_1} {X : Type u_2} {K L : U × X → EReal} (h : K ≤ L) : saddleSwap L ≤ saddleSwap K

noncomputable def Tdaf.ConvexAnalysis.saddleSwapOrderIso {U : Type u_1} {X : Type u_2} : (U × X → EReal) ≃o (X × U → EReal)ᵒᵈ

saddleSwap bundled as an order isomorphism onto the order dual. It is not an endomorphism — the two factors are exchanged — so its two-sided inverse has to be recorded as an Equiv.

Equations

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

@[simp]

theorem Tdaf.ConvexAnalysis.saddleSwapOrderIso_apply {U : Type u_1} {X : Type u_2} (K : U × X → EReal) : saddleSwapOrderIso K = saddleSwap K

theorem Tdaf.ConvexAnalysis.saddleSwap_injective {U : Type u_1} {X : Type u_2} : Function.Injective saddleSwap

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

theorem Tdaf.ConvexAnalysis.partialCl₁_saddleSwap {U : Type u_1} {X : Type u_2} [TopologicalSpace X] (K : U × X → EReal) : partialCl₁ (saddleSwap K) = saddleSwap (partialCl₂ K)

theorem Tdaf.ConvexAnalysis.partialCl₂_saddleSwap {U : Type u_1} {X : Type u_2} [TopologicalSpace U] (K : U × X → EReal) : partialCl₂ (saddleSwap K) = saddleSwap (partialCl₁ K)

theorem Tdaf.ConvexAnalysis.upperCl_saddleSwap {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] (K : U × X → EReal) : upperCl (saddleSwap K) = saddleSwap (lowerCl K)

theorem Tdaf.ConvexAnalysis.lowerCl_saddleSwap {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] (K : U × X → EReal) : lowerCl (saddleSwap K) = saddleSwap (upperCl K)

theorem Tdaf.ConvexAnalysis.lowerClosedFn_iff_upperClosedFn_saddleSwap {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] {K : U × X → EReal} : LowerClosedFn K ↔ UpperClosedFn (saddleSwap K)

Concave-convexity of the first partial closure

theorem Tdaf.ConvexAnalysis.concaveConvexFn_partialCl₁ {U : Type u_1} {V : Type u_2} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] {K : U × X → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] (hK : ConcaveConvexFn K) : ConcaveConvexFn (partialCl₁ K)

Mirroring concaveConvexFn_partialCl₂: cl₁ K is again concave-convex. The pairing needed is the one on the concave variable.

Idempotence of the two closures

theorem Tdaf.ConvexAnalysis.upperClosedFn_upperCl {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) : UpperClosedFn (upperCl K)

The upper closure is idempotent: cl₁ cl₂ cl₁ cl₂ K = cl₁ cl₂ K.

Bu pairs the concave variable and Bx the convex one; Bx must be compatible on both sides, because Fenchel–Moreau is applied once on Y and once on U × X.

theorem Tdaf.ConvexAnalysis.lowerClosedFn_lowerCl {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] {K : U × Y → EReal} [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] [LocallyConvexSpace ℝ V] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx.flip] (hK : ConcaveConvexFn K) : LowerClosedFn (lowerCl K)

The lower closure is idempotent: cl₂ cl₁ cl₂ cl₁ K = cl₂ cl₁ K. This is upperClosedFn_upperCl at saddleSwap K, which is why the pairings are needed on both sides.