Equivalence classes of saddle-functions

Two saddle-functions are equivalent when their partial closures agree, and K is closed when cl₁ K and cl₂ K are both equivalent to K. This is weaker than lower or upper closedness: a whole order interval can be closed while only its two ends are lower and upper closed.

The equivalence classes of closed saddle-functions are exactly the order intervals Ω(F) = {K | ⟨Fu, y⟩ ≤ K ≤ ⟨u, F* y⟩} between the two brackets of a closed convex bifunction F; on such an interval both partial closures are constant, equal to the two ends, and F is determined by the class. The interval lemmas below are stated for a closure pair (K̲, K̄) with cl₁ K̲ = K̄ and cl₂ K̄ = K̲ rather than for a bifunction, so they need no pairing; the closure pairs are exactly the bracket pairs.

Main definitions

• SaddleEquiv K L — cl₁ K = cl₁ L and cl₂ K = cl₂ L.
• ClosedSaddleFn K — cl₁ cl₂ K = cl₁ K and cl₂ cl₁ K = cl₂ K.
• saddleClass Klow Kup — the order interval Ω, as a set of functions.

Main results

• partialCl₂_eq_of_mem_saddleClass, closedSaddleFn_of_mem_saddleClass — the closures are constant on the interval and every member of it is closed (Theorem 34.2 in [^1]).
• exists_unique_bifun_of_closedSaddleFn — conversely, a closed concave-convex function determines a unique closed convex bifunction, with brackets cl₂ K and cl₁ K.

References

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

Equivalence, closedness, and the order interval

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

Two saddle-functions are equivalent when their partial closures agree. Rockafellar uses the single closures here, not the doubled ones.

Equations

• Tdaf.ConvexAnalysis.SaddleEquiv K L = (Tdaf.ConvexAnalysis.partialCl₁ K = Tdaf.ConvexAnalysis.partialCl₁ L ∧ Tdaf.ConvexAnalysis.partialCl₂ K = Tdaf.ConvexAnalysis.partialCl₂ L)

theorem Tdaf.ConvexAnalysis.saddleEquiv_refl {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] (K : U × X → EReal) : SaddleEquiv K K

theorem Tdaf.ConvexAnalysis.SaddleEquiv.symm {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] {K L : U × X → EReal} (h : SaddleEquiv K L) : SaddleEquiv L K

theorem Tdaf.ConvexAnalysis.SaddleEquiv.trans {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] {K L M : U × X → EReal} (h : SaddleEquiv K L) (h' : SaddleEquiv L M) : SaddleEquiv K M

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

A saddle-function is closed when cl₁ K and cl₂ K are both equivalent to it; by idempotence of the closures that amounts to these two equations.

Equations

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

def Tdaf.ConvexAnalysis.saddleClass {U : Type u_1} {X : Type u_2} (Klow Kup : U × X → EReal) : Set (U × X → EReal)

Rockafellar's Ω: the saddle-functions between the two members of a closure pair.

Equations

• Tdaf.ConvexAnalysis.saddleClass Klow Kup = {K : U × X → EReal | Klow ≤ K ∧ K ≤ Kup}

theorem Tdaf.ConvexAnalysis.mem_saddleClass {U : Type u_1} {X : Type u_2} {K Klow Kup : U × X → EReal} : K ∈ saddleClass Klow Kup ↔ Klow ≤ K ∧ K ≤ Kup

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

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

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

The closures are constant on the interval

theorem Tdaf.ConvexAnalysis.partialCl₂_eq_of_mem_saddleClass {U : Type u_1} {X : Type u_2} [TopologicalSpace X] [AddCommGroup X] [IsTopologicalAddGroup X] {Klow Kup K : U × X → EReal} (h2 : partialCl₂ Kup = Klow) (hK : K ∈ saddleClass Klow Kup) : partialCl₂ K = Klow

On the interval of a closure pair, cl₂ is constant at the lower end. Monotonicity squeezes cl₂ K between cl₂ K̲ = K̲ and cl₂ K̄ = K̲.

theorem Tdaf.ConvexAnalysis.partialCl₁_eq_of_mem_saddleClass {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [AddCommGroup U] [IsTopologicalAddGroup U] {Klow Kup K : U × X → EReal} (h1 : partialCl₁ Klow = Kup) (hK : K ∈ saddleClass Klow Kup) : partialCl₁ K = Kup

theorem Tdaf.ConvexAnalysis.saddleEquiv_of_mem_saddleClass {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [AddCommGroup U] [IsTopologicalAddGroup U] [TopologicalSpace X] [AddCommGroup X] [IsTopologicalAddGroup X] {Klow Kup K L : U × X → EReal} (h1 : partialCl₁ Klow = Kup) (h2 : partialCl₂ Kup = Klow) (hK : K ∈ saddleClass Klow Kup) (hL : L ∈ saddleClass Klow Kup) : SaddleEquiv K L

theorem Tdaf.ConvexAnalysis.closedSaddleFn_of_mem_saddleClass {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [AddCommGroup U] [IsTopologicalAddGroup U] [TopologicalSpace X] [AddCommGroup X] [IsTopologicalAddGroup X] {Klow Kup K : U × X → EReal} (h1 : partialCl₁ Klow = Kup) (h2 : partialCl₂ Kup = Klow) (hK : K ∈ saddleClass Klow Kup) : ClosedSaddleFn K

Every member of the interval of a closure pair is a closed saddle-function.

theorem Tdaf.ConvexAnalysis.mem_saddleClass_left {U : Type u_1} {X : Type u_2} [TopologicalSpace X] {Klow Kup : U × X → EReal} (h2 : partialCl₂ Kup = Klow) : Klow ∈ saddleClass Klow Kup

theorem Tdaf.ConvexAnalysis.mem_saddleClass_right {U : Type u_1} {X : Type u_2} [TopologicalSpace X] {Klow Kup : U × X → EReal} (h2 : partialCl₂ Kup = Klow) : Kup ∈ saddleClass Klow Kup

The interval of a closed convex bifunction

theorem Tdaf.ConvexAnalysis.partialCl₂_eq_bracket_of_mem_saddleClass {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} {K : U × Y → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hF : ConvexBifun F) (hcl : ClosedBifun F) (hK : K ∈ saddleClass (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) : partialCl₂ K = fun (p : U × Y) => bracket Bx F p.1 p.2

Between the two brackets of a closed convex bifunction, cl₂ is the lower bracket and cl₁ the upper.

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

theorem Tdaf.ConvexAnalysis.closedSaddleFn_of_mem_saddleClass_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} {K : U × Y → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hF : ConvexBifun F) (hcl : ClosedBifun F) (hK : K ∈ saddleClass (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) : ClosedSaddleFn K

theorem Tdaf.ConvexAnalysis.exists_unique_bifun_of_closedSaddleFn {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) (hcl : ClosedSaddleFn K) : ∃! F : Bifun U X, ConvexBifun F ∧ ClosedBifun F ∧ (fun (p : U × Y) => bracket Bx F p.1 p.2) = partialCl₂ K ∧ (fun (p : U × Y) => concaveBracket Bu (adjointBifun Bu Bx F) p.1 p.2) = partialCl₁ K

Conversely, a closed concave-convex function determines a unique closed convex bifunction, with brackets cl₂ K and cl₁ K. With mem_saddleClass_self, every class of closed saddle-functions is an Ω(F).