Kernels of saddle-functions

The kernel of a concave-convex function K is its restriction to the relative interior ri (dom₁ K) × ri (dom₂ K) of its effective domain, and it is a complete invariant: two closed proper concave-convex functions are equivalent exactly when their kernels agree. Every simple proper such function determines a single equivalence class of closed proper functions with that kernel, the order interval between its lower and upper closures; and closedness of a proper K is visible in the two effective domains C = dom₁ K and D = dom₂ K alone, with no closure operation involved.

Main definitions

• kernelSet K — the rectangle ri (dom₁ K) ×ˢ ri (dom₂ K), which is ri (dom K); kernel K is K on that rectangle and ⊤ off it.
• domSaddle K — dom K = dom₁ K × dom₂ K; ProperSaddleFn K — both halves nonempty.
• SaddleStructure K — the six structural clauses of a closed proper saddle-function, as ConvexSliceStructure for K and for saddleSwap K.
• SimpleSaddleFn K — Rockafellar's simple: over ri (dom₁ K) the convex slices stay inside cl (dom₂ K), and symmetrically.
• lowerSimpleExt C D K, upperSimpleExt C D K — the two simple extensions of a finite saddle-function on C × D.

Main results

• saddleEquiv_iff_kernel_eq — equivalence is detected by the kernel (Theorem 34.4 in [^1]); closedSaddleFn_iff_saddleStructure — closedness is detected by the six structural clauses.
• exists_unique_saddleEquiv_class_of_kernel — a simple proper saddle-function has exactly one class of closed proper functions with its kernel (Theorem 34.5 in [^1]); exists_unique_saddleEquiv_class_of_finite — the same starting from a finite saddle-function.
• kernel_partialCl₂, kernel_partialCl₁, SimpleSaddleFn.partialCl₂, SimpleSaddleFn.partialCl₁ — cl₁ and cl₂ preserve simplicity, properness and the kernel, which is the engine of that uniqueness.
• lowerCl_idem, upperCl_idem — the lower and upper closures are idempotent, with no duality.
• mem_saddleClass_simpleExt_iff_saddleEquiv — the extensions of a finite saddle-function with the prescribed infinite values off C × D are one full equivalence class; SaddleEquiv.eq_of_mem_relint_dom₁ — equivalent closed functions agree over ri (dom₁ K).
• clFn_eq_of_eqOn_relint_dom, clConcave_eq_of_eqOn_relint_domConcave — a closed convex function is determined by its values on ri (dom f).
• domConcave_bracket — the concave effective domain of u ↦ ⟨Fu, y⟩ is dom F; bracket_eq_concaveBracket_adjointBifun_of_polyhedral — for a proper polyhedral bifunction the relative interior may be dropped and the two brackets agree except at the pairs with u ∉ dom F and y ∉ dom F*; exists_unique_bifun_of_simpleExt — a finite continuous saddle-function on a closed C × D comes from a unique closed convex bifunction.

Implementation notes

kernel K is a total function rather than a Set.restrict: equations between restrictions to rectangles that move with the function are unusable, whereas kernel K = kernel L is one honest equation, which kernel_eq_iff unpacks into "same rectangle, same values there". Taking the kernel to be its rectangle alone would break the invariance, since K and K + 1 share a rectangle.

Finite dimension is used only where ri appears. No pairing appears in any statement here: concave-convexity of the partial closures is the only input from the duality layer, and over a normed space the continuous dual supplies the compatible pairing internally.

References

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

Closures agree when the functions agree on a common relative interior

theorem Tdaf.ConvexAnalysis.lscHull_eq_of_eqOn_relint_dom {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f g : E → EReal} (hf : ConvexFn f) (hg : ConvexFn g) (hdom : intrinsicInterior ℝ (dom f) = intrinsicInterior ℝ (dom g)) (heq : Set.EqOn f g (intrinsicInterior ℝ (dom f))) : lscHull f = lscHull g

Two convex functions that agree on the relative interior of a common effective domain have the same lower semicontinuous hull — the sharp form of "a closed convex function is determined by its values on the relative interior of its effective domain". From a relative interior point the half-open segment towards y stays in the relative interior, where the two agree; off cl (dom f) both hulls are ⊤.

theorem Tdaf.ConvexAnalysis.clFn_eq_of_eqOn_relint_dom {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f g : E → EReal} (hf : ConvexFn f) (hg : ConvexFn g) (hdom : intrinsicInterior ℝ (dom f) = intrinsicInterior ℝ (dom g)) (heq : Set.EqOn f g (intrinsicInterior ℝ (dom f))) : clFn f = clFn g

The clFn form of lscHull_eq_of_eqOn_relint_dom.

theorem Tdaf.ConvexAnalysis.clConcave_eq_of_eqOn_relint_domConcave {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f g : E → EReal} (hf : ConcaveFn f) (hg : ConcaveFn g) (hdom : intrinsicInterior ℝ (domConcave f) = intrinsicInterior ℝ (domConcave g)) (heq : Set.EqOn f g (intrinsicInterior ℝ (domConcave f))) : clConcave f = clConcave g

The concave counterpart of clFn_eq_of_eqOn_relint_dom: two concave functions that agree on the relative interior of a common effective domain have the same concave closure.

Two EReal rearrangements

theorem Tdaf.ConvexAnalysis.domConcave_neg {E : Type u_1} (h : E → EReal) : (domConcave fun (z : E) => -h z) = dom h

The concave effective domain of -h is the convex effective domain of h.

Auxiliary facts about closures and relative interiors

theorem Tdaf.ConvexAnalysis.clFn_eq_bot_of_eq_bot {E : Type u_1} [TopologicalSpace E] {f : E → EReal} {x₀ : E} (h : f x₀ = ⊥) : clFn f = fun (x : E) => ⊥

A convex closure that reaches -∞ anywhere is the constant -∞.

theorem Tdaf.ConvexAnalysis.clConcave_eq_top_of_eq_top {E : Type u_1} [TopologicalSpace E] {g : E → EReal} {x₀ : E} (h : g x₀ = ⊤) : clConcave g = fun (x : E) => ⊤

A concave closure that reaches +∞ anywhere is the constant +∞.

theorem Tdaf.ConvexAnalysis.Convex.relint_eq_of_subset_of_subset_closure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C S : Set E} (hC : Convex ℝ C) (hS : Convex ℝ S) (h₁ : C ⊆ S) (h₂ : S ⊆ closure C) : intrinsicInterior ℝ S = intrinsicInterior ℝ C

A convex set squeezed between C and cl C has the same relative interior as C.

theorem Tdaf.ConvexAnalysis.ConcaveFn.clConcave_eq_of_mem_relint_domConcave {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {g : E → EReal} (hg : ConcaveFn g) {x : E} (hx : x ∈ intrinsicInterior ℝ (domConcave g)) : clConcave g x = g x

The concave counterpart of ConvexFn.clFn_eq_of_mem_relint_dom: cl g agrees with g at every relative interior point of domConcave g.

theorem Tdaf.ConvexAnalysis.ConcaveFn.clConcave_eq_of_notMem_closure_domConcave {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {g : E → EReal} (hg : ConcaveFn g) (hp : ProperConcave g) {x : E} (hx : x ∉ closure (domConcave g)) : clConcave g x = g x

The concave counterpart of ConvexFn.clFn_eq_of_notMem_closure_dom: cl g agrees with g off the closure of domConcave g, where both are -∞.

Swapping the two variables

@[simp]

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

@[simp]

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

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

Rockafellar's closedness for saddle-functions is invariant under the swap involution: its two equations exchange places.

The effective domains of the partial closures

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

Every slice K (u, ·) has dom₂ K inside its effective domain.

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

Every slice K (·, x) has dom₁ K inside its concave effective domain.

theorem Tdaf.ConvexAnalysis.proper_slice_of_mem_dom₁ {U : Type u_1} {X : Type u_2} {K : U × X → EReal} {u : U} (hne : (dom₂ K).Nonempty) (hu : u ∈ dom₁ K) : Proper fun (x : X) => K (u, x)

On dom₁ K the slice K (u, ·) is a proper convex function, as soon as dom₂ K is nonempty.

theorem Tdaf.ConvexAnalysis.properConcave_slice_of_mem_dom₂ {U : Type u_1} {X : Type u_2} {K : U × X → EReal} {x : X} (hne : (dom₁ K).Nonempty) (hx : x ∈ dom₂ K) : ProperConcave fun (u : U) => K (u, x)

On dom₂ K the slice K (·, x) is a proper concave function, as soon as dom₁ K is nonempty.

theorem Tdaf.ConvexAnalysis.partialCl₂_slice_eq_bot_of_notMem_dom₁ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup X] {K : U × X → EReal} {u : U} (hu : u ∉ dom₁ K) : (fun (x : X) => partialCl₂ K (u, x)) = fun (x : X) => ⊥

Off dom₁ K the slice K (u, ·) takes the value -∞ somewhere, so its convex closure is the constant -∞.

theorem Tdaf.ConvexAnalysis.dom₂_subset_dom₂_partialCl₂ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup X] (K : U × X → EReal) : dom₂ K ⊆ dom₂ (partialCl₂ K)

cl₂ can only enlarge the second effective domain, since it lowers K.

theorem Tdaf.ConvexAnalysis.proper_partialCl₂_slice {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} {u : U} (hK : ConcaveConvexFn K) (hne : (dom₂ K).Nonempty) (hu : u ∈ dom₁ K) : Proper fun (x : X) => partialCl₂ K (u, x)

On dom₁ K the slice (cl₂ K) (u, ·) is again proper: closing a proper convex function leaves it proper, slice by slice.

theorem Tdaf.ConvexAnalysis.domConcave_partialCl₂_slice {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hne : (dom₂ K).Nonempty) (x : X) : (domConcave fun (u : U) => partialCl₂ K (u, x)) = dom₁ K

dom₁ K is the effective domain of every concave slice (cl₂ K) (·, x), not merely their intersection.

theorem Tdaf.ConvexAnalysis.dom₁_partialCl₂ {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hne : (dom₂ K).Nonempty) : dom₁ (partialCl₂ K) = dom₁ K

cl₂ does not change the first effective domain.

theorem Tdaf.ConvexAnalysis.dom_partialCl₂_slice_subset_closure {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} {u : U} (hK : ConcaveConvexFn K) (hne : (dom₂ K).Nonempty) (hu : u ∈ dom₁ K) : (dom fun (x : X) => partialCl₂ K (u, x)) ⊆ closure (dom fun (x : X) => K (u, x))

Closing a convex function cannot push its effective domain past the closure: that of (cl₂ K) (u, ·) lies inside the closure of that of K (u, ·).

theorem Tdaf.ConvexAnalysis.partialCl₁_slice_eq_top_of_notMem_dom₂ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] {K : U × X → EReal} {x : X} (hx : x ∉ dom₂ K) : (fun (u : U) => partialCl₁ K (u, x)) = fun (x : U) => ⊤

Off dom₂ K the slice K (·, x) takes the value +∞ somewhere, so its concave closure is the constant +∞. The mirror of partialCl₂_slice_eq_bot_of_notMem_dom₁.

theorem Tdaf.ConvexAnalysis.dom₁_subset_dom₁_partialCl₁ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] (K : U × X → EReal) : dom₁ K ⊆ dom₁ (partialCl₁ K)

cl₁ can only enlarge the first effective domain, since it raises K.

theorem Tdaf.ConvexAnalysis.partialCl₂_saddleSwap_slice {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] (K : U × X → EReal) (x : X) : (fun (u : U) => partialCl₂ (saddleSwap K) (x, u)) = fun (u : U) => -partialCl₁ K (u, x)

The slice of cl₂ of the swap, written back in terms of cl₁. This is the workhorse of the transport: every cl₁ statement below is a cl₂ statement at saddleSwap K.

theorem Tdaf.ConvexAnalysis.properConcave_partialCl₁_slice {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [AddCommGroup X] [Module ℝ X] {K : U × X → EReal} {x : X} [FiniteDimensional ℝ U] (hK : ConcaveConvexFn K) (hne : (dom₁ K).Nonempty) (hx : x ∈ dom₂ K) : ProperConcave fun (u : U) => partialCl₁ K (u, x)

The mirror of proper_partialCl₂_slice: on dom₂ K the slice (cl₁ K) (·, x) is again a proper concave function.

theorem Tdaf.ConvexAnalysis.dom_partialCl₁_slice {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [AddCommGroup X] [Module ℝ X] {K : U × X → EReal} [FiniteDimensional ℝ U] (hK : ConcaveConvexFn K) (hne : (dom₁ K).Nonempty) (u : U) : (dom fun (x : X) => partialCl₁ K (u, x)) = dom₂ K

The mirror of domConcave_partialCl₂_slice: dom₂ K is the effective domain of every convex slice (cl₁ K) (u, ·).

theorem Tdaf.ConvexAnalysis.dom₂_partialCl₁ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [AddCommGroup X] [Module ℝ X] {K : U × X → EReal} [FiniteDimensional ℝ U] (hK : ConcaveConvexFn K) (hne : (dom₁ K).Nonempty) : dom₂ (partialCl₁ K) = dom₂ K

cl₁ does not change the second effective domain.

theorem Tdaf.ConvexAnalysis.domConcave_partialCl₁_slice_subset_closure {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [AddCommGroup X] [Module ℝ X] {K : U × X → EReal} {x : X} [FiniteDimensional ℝ U] (hK : ConcaveConvexFn K) (hne : (dom₁ K).Nonempty) (hx : x ∈ dom₂ K) : (domConcave fun (u : U) => partialCl₁ K (u, x)) ⊆ closure (domConcave fun (u : U) => K (u, x))

The mirror of dom_partialCl₂_slice_subset_closure.

Proper saddle-functions and their effective domain

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

The effective domain of a saddle-function: the product dom₁ K × dom₂ K, on which K is finite.

Equations

• Tdaf.ConvexAnalysis.domSaddle K = Tdaf.ConvexAnalysis.dom₁ K ×ˢ Tdaf.ConvexAnalysis.dom₂ K

@[simp]

theorem Tdaf.ConvexAnalysis.mem_domSaddle {U : Type u_1} {X : Type u_2} {K : U × X → EReal} {p : U × X} : p ∈ domSaddle K ↔ p.1 ∈ dom₁ K ∧ p.2 ∈ dom₂ K

structure Tdaf.ConvexAnalysis.ProperSaddleFn {U : Type u_1} {X : Type u_2} (K : U × X → EReal) : Prop

A saddle-function is proper when its effective domain is nonempty.

• dom₁_nonempty : (dom₁ K).Nonempty

  K is somewhere finite in the first variable.

• dom₂_nonempty : (dom₂ K).Nonempty

  K is somewhere finite in the second variable.

theorem Tdaf.ConvexAnalysis.ProperSaddleFn.domSaddle_nonempty {U : Type u_1} {X : Type u_2} {K : U × X → EReal} (hp : ProperSaddleFn K) : (domSaddle K).Nonempty

theorem Tdaf.ConvexAnalysis.properSaddleFn_iff_domSaddle_nonempty {U : Type u_1} {X : Type u_2} {K : U × X → EReal} : ProperSaddleFn K ↔ (domSaddle K).Nonempty

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

theorem Tdaf.ConvexAnalysis.lt_top_of_mem_domSaddle {U : Type u_1} {X : Type u_2} {K : U × X → EReal} {p : U × X} (hp : p ∈ domSaddle K) : K p < ⊤

On its effective domain a saddle-function is finite.

theorem Tdaf.ConvexAnalysis.bot_lt_of_mem_domSaddle {U : Type u_1} {X : Type u_2} {K : U × X → EReal} {p : U × X} (hp : p ∈ domSaddle K) : ⊥ < K p

theorem Tdaf.ConvexAnalysis.relint_domSaddle {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] (K : U × X → EReal) : intrinsicInterior ℝ (domSaddle K) = intrinsicInterior ℝ (dom₁ K) ×ˢ intrinsicInterior ℝ (dom₂ K)

The relative interior of the effective domain of a saddle-function is the product of the two relative interiors: ri (dom K) = ri (dom₁ K) × ri (dom₂ K).

theorem Tdaf.ConvexAnalysis.ProperSaddleFn.relint_dom₁_nonempty {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) : (intrinsicInterior ℝ (dom₁ K)).Nonempty

The first effective domain of a proper concave-convex K has nonempty relative interior.

theorem Tdaf.ConvexAnalysis.ProperSaddleFn.relint_dom₂_nonempty {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) : (intrinsicInterior ℝ (dom₂ K)).Nonempty

The partial closures are again concave-convex, with no pairing to choose

theorem Tdaf.ConvexAnalysis.ConcaveConvexFn.partialCl₂ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) : ConcaveConvexFn (ConvexAnalysis.partialCl₂ K)

The partial closure cl₂ K of a concave-convex function is again concave-convex: over a normed space the continuous dual is a compatible partner, so no pairing has to be chosen.

theorem Tdaf.ConvexAnalysis.ConcaveConvexFn.partialCl₁ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) : ConcaveConvexFn (ConvexAnalysis.partialCl₁ K)

The mirror clause: cl₁ K of a concave-convex function is again concave-convex.

Effective domains and the relative-interior clauses

theorem Tdaf.ConvexAnalysis.ClosedSaddleFn.dom₂_partialCl₂ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hcl : ClosedSaddleFn K) (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) : dom₂ (partialCl₂ K) = dom₂ K

cl₂ leaves the second effective domain of a closed proper saddle-function unchanged. (That it leaves the first unchanged is dom₁_partialCl₂ and needs no closedness.)

theorem Tdaf.ConvexAnalysis.ClosedSaddleFn.dom₁_partialCl₁ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hcl : ClosedSaddleFn K) (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) : dom₁ (partialCl₁ K) = dom₁ K

cl₁ leaves the first effective domain of a closed proper saddle-function unchanged.

theorem Tdaf.ConvexAnalysis.eq_partialCl₂_of_partialCl₁_eq {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedAddCommGroup X] {K : U × X → EReal} {p : U × X} (h : partialCl₁ K p = partialCl₂ K p) : K p = partialCl₂ K p

Where the two closures agree, K agrees with them: they sandwich it.

theorem Tdaf.ConvexAnalysis.ClosedSaddleFn.partialCl₁_eq_partialCl₂_of_mem_relint_dom₁ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hcl : ClosedSaddleFn K) (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) {u : U} (hu : u ∈ intrinsicInterior ℝ (dom₁ K)) (x : X) : partialCl₁ K (u, x) = partialCl₂ K (u, x)

At a relative interior point of dom₁ K the two partial closures of a closed saddle-function already agree.

Closedness gives cl₁ K = cl₁ (cl₂ K), which closes the concave function (cl₂ K) (·, x), whose effective domain is exactly dom₁ K, and a concave function agrees with its closure on the relative interior of that domain.

theorem Tdaf.ConvexAnalysis.ClosedSaddleFn.partialCl₁_eq_partialCl₂_of_mem_relint_dom₂ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hcl : ClosedSaddleFn K) (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) {x : X} (hx : x ∈ intrinsicInterior ℝ (dom₂ K)) (u : U) : partialCl₁ K (u, x) = partialCl₂ K (u, x)

The mirror clause on U × ri (dom₂ K), obtained from the swap involution.

theorem Tdaf.ConvexAnalysis.ClosedSaddleFn.eq_partialCl₂_of_mem_relint_dom₁ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hcl : ClosedSaddleFn K) (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) {u : U} (hu : u ∈ intrinsicInterior ℝ (dom₁ K)) (x : X) : K (u, x) = partialCl₂ K (u, x)

A closed saddle-function coincides with cl₂ K — hence with every member of its equivalence class — on ri (dom₁ K) × X.

theorem Tdaf.ConvexAnalysis.ClosedSaddleFn.eq_partialCl₂_of_mem_relint_dom₂ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hcl : ClosedSaddleFn K) (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) {x : X} (hx : x ∈ intrinsicInterior ℝ (dom₂ K)) (u : U) : K (u, x) = partialCl₂ K (u, x)

The same on U × ri (dom₂ K): there too a closed saddle-function coincides with cl₂ K.

Equivalent saddle-functions: shared domains, agreement on relative interiors

theorem Tdaf.ConvexAnalysis.SaddleEquiv.dom₁_eq {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K L : U × X → EReal} (h : SaddleEquiv K L) (hK : ConcaveConvexFn K) (hpK : ProperSaddleFn K) (hL : ConcaveConvexFn L) (hpL : ProperSaddleFn L) : dom₁ K = dom₁ L

Equivalent saddle-functions have the same first effective domain. No closedness is needed: dom₁ K is already dom₁ (cl₂ K).

theorem Tdaf.ConvexAnalysis.SaddleEquiv.dom₂_eq {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {K L : U × X → EReal} (h : SaddleEquiv K L) (hK : ConcaveConvexFn K) (hpK : ProperSaddleFn K) (hL : ConcaveConvexFn L) (hpL : ProperSaddleFn L) : dom₂ K = dom₂ L

Equivalent saddle-functions have the same second effective domain.

theorem Tdaf.ConvexAnalysis.SaddleEquiv.domSaddle_eq {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K L : U × X → EReal} (h : SaddleEquiv K L) (hK : ConcaveConvexFn K) (hpK : ProperSaddleFn K) (hL : ConcaveConvexFn L) (hpL : ProperSaddleFn L) : domSaddle K = domSaddle L

Equivalent saddle-functions have the same effective domain.

theorem Tdaf.ConvexAnalysis.SaddleEquiv.eq_of_mem_relint_dom₁ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K L : U × X → EReal} (h : SaddleEquiv K L) (hclK : ClosedSaddleFn K) (hK : ConcaveConvexFn K) (hpK : ProperSaddleFn K) (hclL : ClosedSaddleFn L) (hL : ConcaveConvexFn L) (hpL : ProperSaddleFn L) {u : U} (hu : u ∈ intrinsicInterior ℝ (dom₁ K)) (x : X) : K (u, x) = L (u, x)

Equivalent closed saddle-functions agree wherever the first coordinate is a relative interior point of dom₁ K.

theorem Tdaf.ConvexAnalysis.SaddleEquiv.eq_of_mem_relint_dom₂ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K L : U × X → EReal} (h : SaddleEquiv K L) (hclK : ClosedSaddleFn K) (hK : ConcaveConvexFn K) (hpK : ProperSaddleFn K) (hclL : ClosedSaddleFn L) (hL : ConcaveConvexFn L) (hpL : ProperSaddleFn L) {x : X} (hx : x ∈ intrinsicInterior ℝ (dom₂ K)) (u : U) : K (u, x) = L (u, x)

The mirror half: equivalent closed saddle-functions agree over ri (dom₂ K).

Lower and upper closed representatives

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

A lower closed saddle-function is closed.

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

An upper closed saddle-function is closed.

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

The least member cl₂ K of the class of a closed saddle-function is lower closed.

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

The greatest member cl₁ K of the class of a closed saddle-function is upper closed.

theorem Tdaf.ConvexAnalysis.SaddleEquiv.eq_partialCl₂_of_lowerClosedFn {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] [AddCommGroup X] [IsTopologicalAddGroup X] {K L : U × X → EReal} (h : SaddleEquiv K L) (hL : LowerClosedFn L) : L = partialCl₂ K

The lower closed member of an equivalence class is unique.

theorem Tdaf.ConvexAnalysis.SaddleEquiv.eq_partialCl₁_of_upperClosedFn {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [AddCommGroup U] [IsTopologicalAddGroup U] [TopologicalSpace X] {K L : U × X → EReal} (h : SaddleEquiv K L) (hL : UpperClosedFn L) : L = partialCl₁ K

The upper closed member of an equivalence class is unique.

The improper closed saddle-functions

@[simp]

theorem Tdaf.ConvexAnalysis.clFn_const_top {E : Type u_1} [NormedAddCommGroup E] : (clFn fun (x : E) => ⊤) = fun (x : E) => ⊤

The constant +∞ is its own closure.

@[simp]

theorem Tdaf.ConvexAnalysis.clConcave_const_bot {E : Type u_1} [NormedAddCommGroup E] : (clConcave fun (x : E) => ⊥) = fun (x : E) => ⊥

The constant -∞ is its own concave closure.

theorem Tdaf.ConvexAnalysis.ClosedSaddleFn.eq_const_bot_of_dom₁_eq_empty {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedAddCommGroup X] {K : U × X → EReal} (hcl : ClosedSaddleFn K) (h : dom₁ K = ∅) : K = fun (x : U × X) => ⊥

A closed saddle-function with empty first effective domain is the constant -∞.

theorem Tdaf.ConvexAnalysis.ClosedSaddleFn.eq_const_top_of_dom₂_eq_empty {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedAddCommGroup X] {K : U × X → EReal} (hcl : ClosedSaddleFn K) (h : dom₂ K = ∅) : K = fun (x : U × X) => ⊤

A closed saddle-function with empty second effective domain is the constant +∞.

theorem Tdaf.ConvexAnalysis.ClosedSaddleFn.eq_const_of_not_properSaddleFn {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedAddCommGroup X] {K : U × X → EReal} (hcl : ClosedSaddleFn K) (hp : ¬ProperSaddleFn K) : (K = fun (x : U × X) => ⊥) ∨ K = fun (x : U × X) => ⊤

The only improper closed saddle-functions are the two constants.

theorem Tdaf.ConvexAnalysis.not_saddleEquiv_const_bot_const_top {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedAddCommGroup X] [Nonempty U] [Nonempty X] : ¬SaddleEquiv (fun (x : U × X) => ⊥) fun (x : U × X) => ⊤

The two improper closed saddle-functions are not equivalent.

The structure of a closed proper saddle-function

structure Tdaf.ConvexAnalysis.ConvexSliceStructure {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] (K : U × X → EReal) : Prop

The convex slice structure: the description of the convex slices K (u, ·) of a closed proper concave-convex function, according to whether u lies in ri C, in C ∖ ri C, or outside C = dom₁ K.

Over C the lower bound dom₂ K ⊆ dom (K (u, ·)) is unconditional (dom₂_subset_dom_slice) and is therefore not a field, and improperness off C is recorded through the two -∞ clauses rather than as a separate assertion.

• proper_slice (u : U) : u ∈ dom₁ K → Proper fun (x : X) => K (u, x)

  Every slice over dom₁ K is a proper convex function.

• closedFn_slice (u : U) : u ∈ intrinsicInterior ℝ (dom₁ K) → ClosedFn fun (x : X) => K (u, x)

  Over ri (dom₁ K) the slice is moreover closed …

• dom_slice (u : U) : u ∈ intrinsicInterior ℝ (dom₁ K) → (dom fun (x : X) => K (u, x)) = dom₂ K

  … with effective domain exactly dom₂ K.

• dom_slice_subset_closure (u : U) : u ∈ dom₁ K → (dom fun (x : X) => K (u, x)) ⊆ closure (dom₂ K)

  Over dom₁ K the effective domain of the slice stays inside cl (dom₂ K).

• eq_bot_of_notMem_dom₁ (u : U) : u ∉ dom₁ K → ∀ x ∈ intrinsicInterior ℝ (dom₂ K), K (u, x) = ⊥

  Off dom₁ K the slice is -∞ throughout ri (dom₂ K).

• eq_bot_of_notMem_closure_dom₁ (u : U) : u ∉ closure (dom₁ K) → ∀ x ∈ dom₂ K, K (u, x) = ⊥

  Off cl (dom₁ K) the slice is -∞ throughout dom₂ K.

def Tdaf.ConvexAnalysis.SaddleStructure {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] (K : U × X → EReal) : Prop

The full structural description of a closed proper saddle-function: the convex slice structure for K, together with the same for the swapped saddle-function.

Equations

• Tdaf.ConvexAnalysis.SaddleStructure K = (Tdaf.ConvexAnalysis.ConvexSliceStructure K ∧ Tdaf.ConvexAnalysis.ConvexSliceStructure (Tdaf.ConvexAnalysis.saddleSwap K))

theorem Tdaf.ConvexAnalysis.SaddleStructure.saddleSwap {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {K : U × X → EReal} (hs : SaddleStructure K) : SaddleStructure (ConvexAnalysis.saddleSwap K)

The swapped clauses, read in concave language

theorem Tdaf.ConvexAnalysis.SaddleStructure.properConcave_slice {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {K : U × X → EReal} (hs : SaddleStructure K) {x : X} (hx : x ∈ dom₂ K) : ProperConcave fun (u : U) => K (u, x)

Every slice K (·, x) over dom₂ K is a proper concave function.

theorem Tdaf.ConvexAnalysis.SaddleStructure.closedConcaveFn_slice {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {K : U × X → EReal} (hs : SaddleStructure K) {x : X} (hx : x ∈ intrinsicInterior ℝ (dom₂ K)) : ClosedConcaveFn fun (u : U) => K (u, x)

Over ri (dom₂ K) the slice K (·, x) is a closed concave function.

theorem Tdaf.ConvexAnalysis.SaddleStructure.domConcave_slice {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {K : U × X → EReal} (hs : SaddleStructure K) {x : X} (hx : x ∈ intrinsicInterior ℝ (dom₂ K)) : (domConcave fun (u : U) => K (u, x)) = dom₁ K

Over ri (dom₂ K) the slice K (·, x) has dom₁ K as its effective domain.

theorem Tdaf.ConvexAnalysis.SaddleStructure.domConcave_slice_subset_closure {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {K : U × X → EReal} (hs : SaddleStructure K) {x : X} (hx : x ∈ dom₂ K) : (domConcave fun (u : U) => K (u, x)) ⊆ closure (dom₁ K)

Over dom₂ K the effective domain of K (·, x) stays inside cl (dom₁ K).

theorem Tdaf.ConvexAnalysis.SaddleStructure.eq_top_of_notMem_dom₂ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {K : U × X → EReal} (hs : SaddleStructure K) {x : X} (hx : x ∉ dom₂ K) {u : U} (hu : u ∈ intrinsicInterior ℝ (dom₁ K)) : K (u, x) = ⊤

Off dom₂ K the slice K (·, x) is +∞ throughout ri (dom₁ K).

theorem Tdaf.ConvexAnalysis.SaddleStructure.eq_top_of_notMem_closure_dom₂ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {K : U × X → EReal} (hs : SaddleStructure K) {x : X} (hx : x ∉ closure (dom₂ K)) {u : U} (hu : u ∈ dom₁ K) : K (u, x) = ⊤

Off cl (dom₂ K) the slice K (·, x) is +∞ throughout dom₁ K.

Necessity: a closed proper saddle-function is structured

theorem Tdaf.ConvexAnalysis.ClosedSaddleFn.convexSliceStructure {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hcl : ClosedSaddleFn K) (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) : ConvexSliceStructure K

A closed proper concave-convex function has the convex slice structure.

theorem Tdaf.ConvexAnalysis.ClosedSaddleFn.saddleStructure {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hcl : ClosedSaddleFn K) (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) : SaddleStructure K

A closed proper concave-convex function has all six structural properties.

Sufficiency: a structured saddle-function is closed

theorem Tdaf.ConvexAnalysis.SaddleStructure.clConcave_partialCl₂_slice {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hs : SaddleStructure K) (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (x : X) : (clConcave fun (u : U) => partialCl₂ K (u, x)) = clConcave fun (u : U) => K (u, x)

The key step of the sufficiency half: for a structured K, the concave slices of cl₂ K and of K have the same concave closure.

theorem Tdaf.ConvexAnalysis.SaddleStructure.partialCl₁_partialCl₂ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hs : SaddleStructure K) (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) : partialCl₁ (partialCl₂ K) = partialCl₁ K

A structured saddle-function satisfies the first closedness equation, cl₁ (cl₂ K) = cl₁ K.

theorem Tdaf.ConvexAnalysis.SaddleStructure.closedSaddleFn {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hs : SaddleStructure K) (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) : ClosedSaddleFn K

The six structural properties make K closed.

theorem Tdaf.ConvexAnalysis.closedSaddleFn_iff_saddleStructure {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) : ClosedSaddleFn K ↔ SaddleStructure K

A proper concave-convex function is closed if and only if it has the six structural properties.

The kernel

def Tdaf.ConvexAnalysis.kernelSet {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] (K : U × X → EReal) : Set (U × X)

The rectangle ri (dom K) = ri (dom₁ K) × ri (dom₂ K) on which the kernel lives.

Equations

• Tdaf.ConvexAnalysis.kernelSet K = intrinsicInterior ℝ (Tdaf.ConvexAnalysis.dom₁ K) ×ˢ intrinsicInterior ℝ (Tdaf.ConvexAnalysis.dom₂ K)

theorem Tdaf.ConvexAnalysis.kernelSet_eq_relint_domSaddle {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] (K : U × X → EReal) : kernelSet K = intrinsicInterior ℝ (domSaddle K)

@[simp]

theorem Tdaf.ConvexAnalysis.mem_kernelSet {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {K : U × X → EReal} {p : U × X} : p ∈ kernelSet K ↔ p.1 ∈ intrinsicInterior ℝ (dom₁ K) ∧ p.2 ∈ intrinsicInterior ℝ (dom₂ K)

theorem Tdaf.ConvexAnalysis.kernelSet_subset_domSaddle {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] (K : U × X → EReal) : kernelSet K ⊆ domSaddle K

noncomputable def Tdaf.ConvexAnalysis.kernel {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] (K : U × X → EReal) : U × X → EReal

The kernel of a saddle-function: the restriction of K to ri (dom K), extended by ⊤ off that rectangle.

Rockafellar's kernel is literally a partial function, which makes equations between the kernels of two saddle-functions awkward to state. The extension loses nothing — K is finite on ri (dom K), so kernel K is ⊤ exactly off the rectangle — and kernel K = kernel L recovers both "the same rectangle" and "the same values there" (kernel_eq_iff).

Equations

• Tdaf.ConvexAnalysis.kernel K = Tdaf.ConvexAnalysis.restrict (Tdaf.ConvexAnalysis.kernelSet K) K

@[simp]

theorem Tdaf.ConvexAnalysis.kernel_of_mem {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {K : U × X → EReal} {p : U × X} (hp : p ∈ kernelSet K) : kernel K p = K p

@[simp]

theorem Tdaf.ConvexAnalysis.kernel_of_notMem {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {K : U × X → EReal} {p : U × X} (hp : p ∉ kernelSet K) : kernel K p = ⊤

theorem Tdaf.ConvexAnalysis.lt_top_of_mem_kernelSet {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {K : U × X → EReal} {p : U × X} (hp : p ∈ kernelSet K) : K p < ⊤

A saddle-function is finite on its kernel rectangle, which is what makes kernel K detect that rectangle.

theorem Tdaf.ConvexAnalysis.kernel_eq_iff {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {K L : U × X → EReal} : kernel K = kernel L ↔ kernelSet K = kernelSet L ∧ Set.EqOn K L (kernelSet K)

Equality of kernels unpacks into equality of the two rectangles and agreement on them.

theorem Tdaf.ConvexAnalysis.relint_dom₁_eq_of_kernelSet_eq {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K L : U × X → EReal} (hK : ConcaveConvexFn K) (hpK : ProperSaddleFn K) (h : kernelSet K = kernelSet L) : intrinsicInterior ℝ (dom₁ K) = intrinsicInterior ℝ (dom₁ L)

The two factors of the kernel rectangle are determined by it, since both are nonempty for a proper concave-convex function.

theorem Tdaf.ConvexAnalysis.relint_dom₂_eq_of_kernelSet_eq {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K L : U × X → EReal} (hK : ConcaveConvexFn K) (hpK : ProperSaddleFn K) (h : kernelSet K = kernelSet L) : intrinsicInterior ℝ (dom₂ K) = intrinsicInterior ℝ (dom₂ L)

theorem Tdaf.ConvexAnalysis.kernelSet_saddleSwap {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] (K : U × X → EReal) : kernelSet (saddleSwap K) = intrinsicInterior ℝ (dom₂ K) ×ˢ intrinsicInterior ℝ (dom₁ K)

The kernel rectangle of the swapped saddle-function.

theorem Tdaf.ConvexAnalysis.kernel_saddleSwap_eq_of_kernel_eq {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K L : U × X → EReal} (hK : ConcaveConvexFn K) (hpK : ProperSaddleFn K) (h : kernel K = kernel L) : kernel (saddleSwap K) = kernel (saddleSwap L)

Having the same kernel is invariant under the swap involution.

Equivalence is equality of kernels

theorem Tdaf.ConvexAnalysis.SaddleEquiv.kernel_eq {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K L : U × X → EReal} (h : SaddleEquiv K L) (hclK : ClosedSaddleFn K) (hK : ConcaveConvexFn K) (hpK : ProperSaddleFn K) (hclL : ClosedSaddleFn L) (hL : ConcaveConvexFn L) (hpL : ProperSaddleFn L) : kernel K = kernel L

Equivalent closed proper saddle-functions have the same kernel: they share both effective domains and agree over the relative interiors.

theorem Tdaf.ConvexAnalysis.slice_eq_of_kernel_eq {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K L : U × X → EReal} (hclK : ClosedSaddleFn K) (hK : ConcaveConvexFn K) (hpK : ProperSaddleFn K) (hclL : ClosedSaddleFn L) (hL : ConcaveConvexFn L) (hpL : ProperSaddleFn L) (h : kernel K = kernel L) {u : U} (hu : u ∈ intrinsicInterior ℝ (dom₁ K)) : (fun (x : X) => K (u, x)) = fun (x : X) => L (u, x)

Over ri (dom₁ K) two closed proper saddle-functions with the same kernel have literally the same convex slice. A closed convex function is determined by its values on the relative interior of its effective domain.

theorem Tdaf.ConvexAnalysis.dom₂_eq_of_kernel_eq {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K L : U × X → EReal} (hclK : ClosedSaddleFn K) (hK : ConcaveConvexFn K) (hpK : ProperSaddleFn K) (hclL : ClosedSaddleFn L) (hL : ConcaveConvexFn L) (hpL : ProperSaddleFn L) (h : kernel K = kernel L) : dom₂ K = dom₂ L

Two closed proper saddle-functions with the same kernel have the same second effective domain.

theorem Tdaf.ConvexAnalysis.partialCl₁_eq_of_kernel_eq {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K L : U × X → EReal} (hclK : ClosedSaddleFn K) (hK : ConcaveConvexFn K) (hpK : ProperSaddleFn K) (hclL : ClosedSaddleFn L) (hL : ConcaveConvexFn L) (hpL : ProperSaddleFn L) (h : kernel K = kernel L) : partialCl₁ K = partialCl₁ L

Two closed proper saddle-functions with the same kernel have the same concave closure cl₁.

theorem Tdaf.ConvexAnalysis.saddleEquiv_iff_kernel_eq {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K L : U × X → EReal} (hclK : ClosedSaddleFn K) (hK : ConcaveConvexFn K) (hpK : ProperSaddleFn K) (hclL : ClosedSaddleFn L) (hL : ConcaveConvexFn L) (hpL : ProperSaddleFn L) : SaddleEquiv K L ↔ kernel K = kernel L

Two closed proper concave-convex functions are equivalent if and only if they have the same kernel.

Idempotence of the lower and upper closures, without any duality

theorem Tdaf.ConvexAnalysis.lowerCl_idem {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [AddCommGroup U] [IsTopologicalAddGroup U] [TopologicalSpace X] [AddCommGroup X] [IsTopologicalAddGroup X] (K : U × X → EReal) : lowerCl (lowerCl K) = lowerCl K

The lower closure is lower closed: lowerCl is idempotent.

No duality is needed: cl₁ and cl₂ are a closure and a co-closure operator — monotone, idempotent, one raising and one lowering — and with M = cl₁ K, N = cl₂ M the chain cl₂ (cl₁ N) ≤ cl₂ (cl₁ M) = cl₂ M = N = cl₂ N ≤ cl₂ (cl₁ N) closes.

theorem Tdaf.ConvexAnalysis.upperCl_idem {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [AddCommGroup U] [IsTopologicalAddGroup U] [TopologicalSpace X] [AddCommGroup X] [IsTopologicalAddGroup X] (K : U × X → EReal) : upperCl (upperCl K) = upperCl K

The upper closure is upper closed, by the swap involution.

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

The lower closure is convex-closed: it is a cl₂.

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

The upper closure is concave-closed: it is a cl₁.

theorem Tdaf.ConvexAnalysis.closedSaddleFn_lowerCl {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [AddCommGroup U] [IsTopologicalAddGroup U] [TopologicalSpace X] [AddCommGroup X] [IsTopologicalAddGroup X] (K : U × X → EReal) : ClosedSaddleFn (lowerCl K)

The lower closure of any saddle-function is a closed saddle-function.

theorem Tdaf.ConvexAnalysis.closedSaddleFn_upperCl {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [AddCommGroup U] [IsTopologicalAddGroup U] [TopologicalSpace X] [AddCommGroup X] [IsTopologicalAddGroup X] (K : U × X → EReal) : ClosedSaddleFn (upperCl K)

The upper closure of any saddle-function is a closed saddle-function.

Simple saddle-functions

structure Tdaf.ConvexAnalysis.SimpleSaddleFn {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] (K : U × X → EReal) : Prop

A concave-convex function is simple — Rockafellar's word — when over ri (dom₁ K) the convex slices have their effective domains inside cl (dom₂ K), and symmetrically. Every closed proper saddle-function is simple, and so is every simple extension of a finite saddle-function on a product of convex sets.

• dom_slice_subset_closure (u : U) : u ∈ intrinsicInterior ℝ (dom₁ K) → (dom fun (x : X) => K (u, x)) ⊆ closure (dom₂ K)

  Over ri (dom₁ K) the convex slice does not reach beyond cl (dom₂ K).

• domConcave_slice_subset_closure (x : X) : x ∈ intrinsicInterior ℝ (dom₂ K) → (domConcave fun (u : U) => K (u, x)) ⊆ closure (dom₁ K)

  Over ri (dom₂ K) the concave slice does not reach beyond cl (dom₁ K).

theorem Tdaf.ConvexAnalysis.simpleSaddleFn_saddleSwap_iff {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {K : U × X → EReal} : SimpleSaddleFn (saddleSwap K) ↔ SimpleSaddleFn K

Simplicity is invariant under the swap involution: the two clauses trade places.

theorem Tdaf.ConvexAnalysis.SaddleStructure.simpleSaddleFn {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {K : U × X → EReal} (hs : SaddleStructure K) : SimpleSaddleFn K

The two slice-domain clauses say precisely that a structured saddle-function is simple.

theorem Tdaf.ConvexAnalysis.ClosedSaddleFn.simpleSaddleFn {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hcl : ClosedSaddleFn K) (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) : SimpleSaddleFn K

Every closed proper concave-convex function is simple.

The partial closures preserve simplicity, properness and the kernel

theorem Tdaf.ConvexAnalysis.relint_dom_slice {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hs : SimpleSaddleFn K) {u : U} (hu : u ∈ intrinsicInterior ℝ (dom₁ K)) : intrinsicInterior ℝ (dom fun (x : X) => K (u, x)) = intrinsicInterior ℝ (dom₂ K)

For a simple K, a convex slice taken over ri (dom₁ K) has effective domain with the same relative interior as dom₂ K.

theorem Tdaf.ConvexAnalysis.partialCl₂_eq_of_mem_kernelSet {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hs : SimpleSaddleFn K) {p : U × X} (hmem : p ∈ kernelSet K) : partialCl₂ K p = K p

cl₂ does not move a simple K on the kernel rectangle.

theorem Tdaf.ConvexAnalysis.dom₂_partialCl₂_subset_closure {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SimpleSaddleFn K) : dom₂ (partialCl₂ K) ⊆ closure (dom₂ K)

cl₂ cannot enlarge dom₂ K beyond its closure.

theorem Tdaf.ConvexAnalysis.relint_dom₂_partialCl₂ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SimpleSaddleFn K) : intrinsicInterior ℝ (dom₂ (partialCl₂ K)) = intrinsicInterior ℝ (dom₂ K)

cl₂ leaves the relative interior of dom₂ alone when K is simple.

theorem Tdaf.ConvexAnalysis.closure_dom₂_partialCl₂ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SimpleSaddleFn K) : closure (dom₂ (partialCl₂ K)) = closure (dom₂ K)

cl₂ leaves the closure of dom₂ alone when K is simple.

theorem Tdaf.ConvexAnalysis.ProperSaddleFn.partialCl₂ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) : ProperSaddleFn (ConvexAnalysis.partialCl₂ K)

cl₂ preserves properness.

theorem Tdaf.ConvexAnalysis.SimpleSaddleFn.partialCl₂ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SimpleSaddleFn K) : SimpleSaddleFn (ConvexAnalysis.partialCl₂ K)

cl₂ preserves simplicity.

theorem Tdaf.ConvexAnalysis.kernel_partialCl₂ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SimpleSaddleFn K) : kernel (partialCl₂ K) = kernel K

cl₂ preserves the kernel.

theorem Tdaf.ConvexAnalysis.ProperSaddleFn.partialCl₁ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) : ProperSaddleFn (ConvexAnalysis.partialCl₁ K)

cl₁ preserves properness.

theorem Tdaf.ConvexAnalysis.SimpleSaddleFn.partialCl₁ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SimpleSaddleFn K) : SimpleSaddleFn (ConvexAnalysis.partialCl₁ K)

The mirror: cl₁ preserves simplicity.

theorem Tdaf.ConvexAnalysis.kernel_partialCl₁ {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SimpleSaddleFn K) : kernel (partialCl₁ K) = kernel K

The mirror: cl₁ preserves the kernel.

The equivalence class attached to a simple saddle-function

theorem Tdaf.ConvexAnalysis.dom₁_mono {U : Type u_1} {X : Type u_2} {K L : U × X → EReal} (h : K ≤ L) : dom₁ K ⊆ dom₁ L

The first effective domain is monotone in the saddle-function.

theorem Tdaf.ConvexAnalysis.dom₂_anti {U : Type u_1} {X : Type u_2} {K L : U × X → EReal} (h : K ≤ L) : dom₂ L ⊆ dom₂ K

The second effective domain is antitone in the saddle-function.

theorem Tdaf.ConvexAnalysis.ConcaveConvexFn.lowerCl {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) : ConcaveConvexFn (ConvexAnalysis.lowerCl K)

The lower closure of a simple proper concave-convex function is concave-convex.

theorem Tdaf.ConvexAnalysis.ConcaveConvexFn.upperCl {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) : ConcaveConvexFn (ConvexAnalysis.upperCl K)

The upper closure of a concave-convex function is concave-convex.

theorem Tdaf.ConvexAnalysis.ProperSaddleFn.lowerCl {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) : ProperSaddleFn (ConvexAnalysis.lowerCl K)

The lower closure of a simple proper saddle-function is proper.

theorem Tdaf.ConvexAnalysis.ProperSaddleFn.upperCl {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) : ProperSaddleFn (ConvexAnalysis.upperCl K)

The upper closure of a simple proper saddle-function is proper.

theorem Tdaf.ConvexAnalysis.SimpleSaddleFn.lowerCl {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SimpleSaddleFn K) : SimpleSaddleFn (ConvexAnalysis.lowerCl K)

The lower closure of a simple saddle-function is simple.

theorem Tdaf.ConvexAnalysis.SimpleSaddleFn.upperCl {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SimpleSaddleFn K) : SimpleSaddleFn (ConvexAnalysis.upperCl K)

The upper closure of a simple saddle-function is simple.

theorem Tdaf.ConvexAnalysis.kernel_lowerCl {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SimpleSaddleFn K) : kernel (lowerCl K) = kernel K

The lower closure of a simple saddle-function has the same kernel.

theorem Tdaf.ConvexAnalysis.kernel_upperCl {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SimpleSaddleFn K) : kernel (upperCl K) = kernel K

The upper closure of a simple saddle-function has the same kernel.

theorem Tdaf.ConvexAnalysis.saddleEquiv_lowerCl_upperCl {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SimpleSaddleFn K) : SaddleEquiv (lowerCl K) (upperCl K)

For a simple proper concave-convex K, the lower closure cl₂ cl₁ K and the upper closure cl₁ cl₂ K are equivalent. Both are closed, and both have the same kernel as K, which for closed proper saddle-functions already forces equivalence.

theorem Tdaf.ConvexAnalysis.partialCl₁_lowerCl {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SimpleSaddleFn K) : partialCl₁ (lowerCl K) = upperCl K

cl₁ carries the lower closure to the upper one: the two are a closure pair.

theorem Tdaf.ConvexAnalysis.partialCl₂_upperCl {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SimpleSaddleFn K) : partialCl₂ (upperCl K) = lowerCl K

cl₂ carries the upper closure back to the lower one.

theorem Tdaf.ConvexAnalysis.lowerCl_le_upperCl {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SimpleSaddleFn K) : lowerCl K ≤ upperCl K

The lower closure lies below the upper one: cl₂ cl₁ K ≤ cl₁ cl₂ K.

theorem Tdaf.ConvexAnalysis.closedSaddleFn_of_mem_saddleClass_lowerCl {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K L : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SimpleSaddleFn K) (hL : L ∈ saddleClass (lowerCl K) (upperCl K)) : ClosedSaddleFn L

Every saddle-function between the two closures is closed.

theorem Tdaf.ConvexAnalysis.properSaddleFn_of_mem_saddleClass_lowerCl {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K L : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hL : L ∈ saddleClass (lowerCl K) (upperCl K)) : ProperSaddleFn L

Every saddle-function between the two closures is proper.

theorem Tdaf.ConvexAnalysis.saddleEquiv_of_mem_saddleClass_lowerCl {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K L : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SimpleSaddleFn K) (hL : L ∈ saddleClass (lowerCl K) (upperCl K)) : SaddleEquiv (lowerCl K) L

Every saddle-function between the two closures is equivalent to them.

theorem Tdaf.ConvexAnalysis.kernel_of_mem_saddleClass_lowerCl {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K L : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SimpleSaddleFn K) (hCC : ConcaveConvexFn L) (hL : L ∈ saddleClass (lowerCl K) (upperCl K)) : kernel L = kernel K

Every concave-convex saddle-function between the two closures has the same kernel as K.

theorem Tdaf.ConvexAnalysis.mem_saddleClass_lowerCl_of_kernel_eq {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K L : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SimpleSaddleFn K) (hclL : ClosedSaddleFn L) (hCC : ConcaveConvexFn L) (hpL : ProperSaddleFn L) (hker : kernel L = kernel K) : L ∈ saddleClass (lowerCl K) (upperCl K)

Conversely, a closed proper concave-convex function with the same kernel as K lies between the two closures.

theorem Tdaf.ConvexAnalysis.exists_unique_saddleEquiv_class_of_kernel {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → EReal} (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SimpleSaddleFn K) : ∃ (M : U × X → EReal), (ClosedSaddleFn M ∧ ConcaveConvexFn M ∧ ProperSaddleFn M ∧ kernel M = kernel K) ∧ ∀ (L : U × X → EReal), ClosedSaddleFn L → ConcaveConvexFn L → ProperSaddleFn L → (kernel L = kernel K ↔ SaddleEquiv M L)

The kernel of a simple proper concave-convex function is the kernel of exactly one equivalence class of closed proper concave-convex functions, represented by the lower closure cl₂ cl₁ K.

The simple extensions of a finite saddle-function on C × D

theorem Tdaf.ConvexAnalysis.dom_restrict_coe {E : Type u_1} (s : Set E) (g : E → ℝ) : dom (restrict s fun (x : E) => ↑(g x)) = s

The effective domain of a finite function extended by ⊤ is the set it was given on.

theorem Tdaf.ConvexAnalysis.domConcave_restrictConcave_coe {E : Type u_1} (s : Set E) (g : E → ℝ) : domConcave (restrictConcave s fun (x : E) => ↑(g x)) = s

The concave effective domain of a finite function extended by ⊥ is the set it was given on.

theorem Tdaf.ConvexAnalysis.concaveFn_const {E : Type u_1} [AddCommGroup E] [Module ℝ E] (c : EReal) : ConcaveFn fun (x : E) => c

Constant functions are concave; the mirror of convexFn_const.

theorem Tdaf.ConvexAnalysis.ConcaveFn.restrictConcave {E : Type u_1} [AddCommGroup E] [Module ℝ E] {g : E → EReal} {s : Set E} (hg : ConcaveFn g) (hs : Convex ℝ s) : ConcaveFn (ConvexAnalysis.restrictConcave s g)

Restricting a concave function to a convex set — extending by ⊥ off it — gives a concave function; the mirror of ConvexFn.restrict.

noncomputable def Tdaf.ConvexAnalysis.lowerSimpleExt {U : Type u_1} {X : Type u_2} (C : Set U) (D : Set X) (K : U × X → ℝ) : U × X → EReal

Rockafellar's lower simple extension K₁ of a finite saddle-function K on C × D: K on C × D, +∞ on C × Dᶜ, and -∞ off C.

Equations

• Tdaf.ConvexAnalysis.lowerSimpleExt C D K p = Tdaf.ConvexAnalysis.restrictConcave C (fun (u : U) => Tdaf.ConvexAnalysis.restrict D (fun (x : X) => ↑(K (u, x))) p.2) p.1

@[simp]

theorem Tdaf.ConvexAnalysis.lowerSimpleExt_of_mem {U : Type u_1} {X : Type u_2} {C : Set U} {D : Set X} {K : U × X → ℝ} {p : U × X} (hu : p.1 ∈ C) (hx : p.2 ∈ D) : lowerSimpleExt C D K p = ↑(K p)

@[simp]

theorem Tdaf.ConvexAnalysis.lowerSimpleExt_of_notMem_left {U : Type u_1} {X : Type u_2} {C : Set U} {D : Set X} {K : U × X → ℝ} {p : U × X} (hu : p.1 ∉ C) : lowerSimpleExt C D K p = ⊥

@[simp]

theorem Tdaf.ConvexAnalysis.lowerSimpleExt_of_notMem_right {U : Type u_1} {X : Type u_2} {C : Set U} {D : Set X} {K : U × X → ℝ} {p : U × X} (hu : p.1 ∈ C) (hx : p.2 ∉ D) : lowerSimpleExt C D K p = ⊤

theorem Tdaf.ConvexAnalysis.lowerSimpleExt_slice₂_of_mem {U : Type u_1} {X : Type u_2} {C : Set U} {D : Set X} {K : U × X → ℝ} {u : U} (hu : u ∈ C) : (fun (x : X) => lowerSimpleExt C D K (u, x)) = restrict D fun (x : X) => ↑(K (u, x))

Over C the convex slice of K₁ is K (u, ·) extended by ⊤ off D.

theorem Tdaf.ConvexAnalysis.lowerSimpleExt_slice₂_of_notMem {U : Type u_1} {X : Type u_2} {C : Set U} {D : Set X} {K : U × X → ℝ} {u : U} (hu : u ∉ C) : (fun (x : X) => lowerSimpleExt C D K (u, x)) = fun (x : X) => ⊥

Off C the convex slice of K₁ is the constant -∞.

theorem Tdaf.ConvexAnalysis.lowerSimpleExt_slice₁_of_mem {U : Type u_1} {X : Type u_2} {C : Set U} {D : Set X} {K : U × X → ℝ} {x : X} (hx : x ∈ D) : (fun (u : U) => lowerSimpleExt C D K (u, x)) = restrictConcave C fun (u : U) => ↑(K (u, x))

Over D the concave slice of K₁ is K (·, x) extended by -∞ off C.

theorem Tdaf.ConvexAnalysis.lowerSimpleExt_slice₁_of_notMem {U : Type u_1} {X : Type u_2} {C : Set U} {D : Set X} {K : U × X → ℝ} {x : X} (hx : x ∉ D) : (fun (u : U) => lowerSimpleExt C D K (u, x)) = restrictConcave C fun (x : U) => ⊤

Off D the concave slice of K₁ is the indicator-like function that is +∞ on C and -∞ off it.

theorem Tdaf.ConvexAnalysis.dom₁_lowerSimpleExt {U : Type u_1} {X : Type u_2} {C : Set U} {D : Set X} {K : U × X → ℝ} (hD : D.Nonempty) : dom₁ (lowerSimpleExt C D K) = C

The lower simple extension has dom₁ K₁ = C.

theorem Tdaf.ConvexAnalysis.dom₂_lowerSimpleExt {U : Type u_1} {X : Type u_2} {C : Set U} {D : Set X} {K : U × X → ℝ} (hC : C.Nonempty) : dom₂ (lowerSimpleExt C D K) = D

The lower simple extension has dom₂ K₁ = D.

theorem Tdaf.ConvexAnalysis.concaveConvexFn_lowerSimpleExt {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {C : Set U} {D : Set X} {K : U × X → ℝ} (hC : Convex ℝ C) (hconv : ∀ u ∈ C, ConvexOn ℝ D fun (x : X) => K (u, x)) (hconc : ∀ x ∈ D, ConcaveOn ℝ C fun (u : U) => K (u, x)) : ConcaveConvexFn (lowerSimpleExt C D K)

The lower simple extension of a finite concave-convex function on C × D is concave-convex on all of U × X.

theorem Tdaf.ConvexAnalysis.properSaddleFn_lowerSimpleExt {U : Type u_1} {X : Type u_2} {C : Set U} {D : Set X} {K : U × X → ℝ} (hCne : C.Nonempty) (hDne : D.Nonempty) : ProperSaddleFn (lowerSimpleExt C D K)

The lower simple extension of a finite saddle-function on a nonempty C × D is proper.

theorem Tdaf.ConvexAnalysis.simpleSaddleFn_lowerSimpleExt {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {C : Set U} {D : Set X} {K : U × X → ℝ} (hCne : C.Nonempty) (hDne : D.Nonempty) : SimpleSaddleFn (lowerSimpleExt C D K)

The lower simple extension of a finite saddle-function is simple. Its slices have effective domains exactly D and C, so they do not even reach the boundary.

theorem Tdaf.ConvexAnalysis.kernel_lowerSimpleExt {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {C : Set U} {D : Set X} {K : U × X → ℝ} (hCne : C.Nonempty) (hDne : D.Nonempty) : kernel (lowerSimpleExt C D K) = restrict (intrinsicInterior ℝ (C ×ˢ D)) fun (p : U × X) => ↑(K p)

The kernel of the lower simple extension is the restriction of K to ri (C × D).

theorem Tdaf.ConvexAnalysis.exists_unique_saddleEquiv_class_of_finite {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {C : Set U} {D : Set X} {K : U × X → ℝ} (hC : Convex ℝ C) (hCne : C.Nonempty) (hDne : D.Nonempty) (hconv : ∀ u ∈ C, ConvexOn ℝ D fun (x : X) => K (u, x)) (hconc : ∀ x ∈ D, ConcaveOn ℝ C fun (u : U) => K (u, x)) : ∃ (M : U × X → EReal), (ClosedSaddleFn M ∧ ConcaveConvexFn M ∧ ProperSaddleFn M ∧ kernel M = restrict (intrinsicInterior ℝ (C ×ˢ D)) fun (p : U × X) => ↑(K p)) ∧ ∀ (L : U × X → EReal), ClosedSaddleFn L → ConcaveConvexFn L → ProperSaddleFn L → ((kernel L = restrict (intrinsicInterior ℝ (C ×ˢ D)) fun (p : U × X) => ↑(K p)) ↔ SaddleEquiv M L)

A finite concave-convex function K on a nonempty product C × D of convex sets is the kernel of exactly one equivalence class of closed proper concave-convex functions on U × X. The class is the one attached to the lower simple extension of K.

Closedness of a finite continuous function on a closed set

theorem Tdaf.ConvexAnalysis.isClosed_epi_restrict_coe {E : Type u_1} [TopologicalSpace E] {s : Set E} {g : E → ℝ} (hs : IsClosed s) (hg : ContinuousOn g s) : IsClosed (epi (restrict s fun (x : E) => ↑(g x)))

The epigraph of a finite continuous function on a closed set, extended by ⊤, is closed.

theorem Tdaf.ConvexAnalysis.closedFn_restrict_coe {E : Type u_1} [TopologicalSpace E] [AddCommGroup E] [IsTopologicalAddGroup E] {s : Set E} {g : E → ℝ} (hs : IsClosed s) (hg : ContinuousOn g s) : ClosedFn (restrict s fun (x : E) => ↑(g x))

A finite continuous function on a closed set, extended by ⊤, is a closed function.

theorem Tdaf.ConvexAnalysis.closedConcaveFn_restrictConcave_coe {E : Type u_1} [TopologicalSpace E] [AddCommGroup E] [IsTopologicalAddGroup E] {s : Set E} {g : E → ℝ} (hs : IsClosed s) (hg : ContinuousOn g s) : ClosedConcaveFn (restrictConcave s fun (x : E) => ↑(g x))

The concave mirror: a finite continuous function on a closed set, extended by -∞, is a closed concave function.

The upper simple extension

noncomputable def Tdaf.ConvexAnalysis.upperSimpleExt {U : Type u_1} {X : Type u_2} (C : Set U) (D : Set X) (K : U × X → ℝ) : U × X → EReal

Rockafellar's upper simple extension K₂ of a finite saddle-function K on C × D: K on C × D, -∞ on Cᶜ × D, and +∞ off D.

Equations

• Tdaf.ConvexAnalysis.upperSimpleExt C D K p = Tdaf.ConvexAnalysis.restrict D (fun (x : X) => Tdaf.ConvexAnalysis.restrictConcave C (fun (u : U) => ↑(K (u, x))) p.1) p.2

def Tdaf.ConvexAnalysis.swapReal {U : Type u_1} {X : Type u_2} (K : U × X → ℝ) : X × U → ℝ

The real-valued companion of saddleSwap: negate and exchange the two arguments. Note that swapReal (swapReal K) = K is not rfl, because the negation is on ℝ values.

Equations

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

@[simp]

theorem Tdaf.ConvexAnalysis.swapReal_swapReal {U : Type u_1} {X : Type u_2} (K : U × X → ℝ) : swapReal (swapReal K) = K

theorem Tdaf.ConvexAnalysis.upperSimpleExt_eq_saddleSwap {U : Type u_1} {X : Type u_2} (C : Set U) (D : Set X) (K : U × X → ℝ) : upperSimpleExt C D K = saddleSwap (lowerSimpleExt D C (swapReal K))

The upper simple extension is the lower one, swapped.

This identity is the whole of the upper theory: exchanging the two arguments turns C into D, the concave restriction into the convex one and -∞ into +∞, which is what saddleSwap does on the value side and swapReal on the real side. Every upper lemma below is a rewrite along it.

@[simp]

theorem Tdaf.ConvexAnalysis.upperSimpleExt_of_mem {U : Type u_1} {X : Type u_2} {C : Set U} {D : Set X} {K : U × X → ℝ} {p : U × X} (hu : p.1 ∈ C) (hx : p.2 ∈ D) : upperSimpleExt C D K p = ↑(K p)

@[simp]

theorem Tdaf.ConvexAnalysis.upperSimpleExt_of_notMem_right {U : Type u_1} {X : Type u_2} {C : Set U} {D : Set X} {K : U × X → ℝ} {p : U × X} (hx : p.2 ∉ D) : upperSimpleExt C D K p = ⊤

@[simp]

theorem Tdaf.ConvexAnalysis.upperSimpleExt_of_notMem_left {U : Type u_1} {X : Type u_2} {C : Set U} {D : Set X} {K : U × X → ℝ} {p : U × X} (hu : p.1 ∉ C) (hx : p.2 ∈ D) : upperSimpleExt C D K p = ⊥

theorem Tdaf.ConvexAnalysis.upperSimpleExt_slice₂_of_mem {U : Type u_1} {X : Type u_2} {C : Set U} {D : Set X} {K : U × X → ℝ} {u : U} (hu : u ∈ C) : (fun (x : X) => upperSimpleExt C D K (u, x)) = restrict D fun (x : X) => ↑(K (u, x))

Over C the convex slice of K₂ agrees with that of K₁.

theorem Tdaf.ConvexAnalysis.upperSimpleExt_slice₂_of_notMem {U : Type u_1} {X : Type u_2} {C : Set U} {D : Set X} {K : U × X → ℝ} {u : U} (hu : u ∉ C) : (fun (x : X) => upperSimpleExt C D K (u, x)) = restrict D fun (x : X) => ⊥

Off C the convex slice of K₂ is -∞ on D and +∞ elsewhere.

theorem Tdaf.ConvexAnalysis.upperSimpleExt_slice₁_of_mem {U : Type u_1} {X : Type u_2} {C : Set U} {D : Set X} {K : U × X → ℝ} {x : X} (hx : x ∈ D) : (fun (u : U) => upperSimpleExt C D K (u, x)) = restrictConcave C fun (u : U) => ↑(K (u, x))

Over D the concave slice of K₂ agrees with that of K₁.

theorem Tdaf.ConvexAnalysis.upperSimpleExt_slice₁_of_notMem {U : Type u_1} {X : Type u_2} {C : Set U} {D : Set X} {K : U × X → ℝ} {x : X} (hx : x ∉ D) : (fun (u : U) => upperSimpleExt C D K (u, x)) = fun (x : U) => ⊤

Off D the concave slice of K₂ is the constant +∞.

theorem Tdaf.ConvexAnalysis.dom₁_upperSimpleExt {U : Type u_1} {X : Type u_2} {C : Set U} {D : Set X} {K : U × X → ℝ} (hD : D.Nonempty) : dom₁ (upperSimpleExt C D K) = C

The upper simple extension has dom₁ K₂ = C.

theorem Tdaf.ConvexAnalysis.dom₂_upperSimpleExt {U : Type u_1} {X : Type u_2} {C : Set U} {D : Set X} {K : U × X → ℝ} (hC : C.Nonempty) : dom₂ (upperSimpleExt C D K) = D

The upper simple extension has dom₂ K₂ = D.

theorem Tdaf.ConvexAnalysis.mem_saddleClass_simpleExt_iff {U : Type u_1} {X : Type u_2} {C : Set U} {D : Set X} {K : U × X → ℝ} {L : U × X → EReal} : L ∈ saddleClass (lowerSimpleExt C D K) (upperSimpleExt C D K) ↔ (∀ u ∈ C, ∀ x ∈ D, L (u, x) = ↑(K (u, x))) ∧ (∀ u ∈ C, ∀ x ∉ D, L (u, x) = ⊤) ∧ ∀ u ∉ C, ∀ x ∈ D, L (u, x) = ⊥

The interval between the two simple extensions is exactly the set of extensions of K with Rockafellar's prescribed infinite values off C × D — the class Ω. The values on Cᶜ × Dᶜ are unconstrained.

theorem Tdaf.ConvexAnalysis.concaveConvexFn_upperSimpleExt {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {C : Set U} {D : Set X} {K : U × X → ℝ} (hD : Convex ℝ D) (hconv : ∀ u ∈ C, ConvexOn ℝ D fun (x : X) => K (u, x)) (hconc : ∀ x ∈ D, ConcaveOn ℝ C fun (u : U) => K (u, x)) : ConcaveConvexFn (upperSimpleExt C D K)

The upper simple extension of a finite concave-convex function on C × D is concave-convex on all of U × X.

Transported from concaveConvexFn_lowerSimpleExt: the swap exchanges the convexity and concavity hypotheses and negates each, which is exactly ConvexOn.neg and ConcaveOn.neg.

The class Ω is a full equivalence class

theorem Tdaf.ConvexAnalysis.partialCl₂_lowerSimpleExt {U : Type u_1} {X : Type u_2} [TopologicalSpace X] [AddCommGroup X] [IsTopologicalAddGroup X] {C : Set U} {D : Set X} {K : U × X → ℝ} (hDcl : IsClosed D) (hcont : ∀ u ∈ C, ContinuousOn (fun (x : X) => K (u, x)) D) : partialCl₂ (lowerSimpleExt C D K) = lowerSimpleExt C D K

The convex slices of the two simple extensions of a finite continuous saddle-function on a closed C × D are closed, so cl₂ fixes the lower simple extension.

theorem Tdaf.ConvexAnalysis.partialCl₁_lowerSimpleExt {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [AddCommGroup U] [IsTopologicalAddGroup U] {C : Set U} {D : Set X} {K : U × X → ℝ} (hCcl : IsClosed C) (hCne : C.Nonempty) (hcont : ∀ x ∈ D, ContinuousOn (fun (u : U) => K (u, x)) C) : partialCl₁ (lowerSimpleExt C D K) = upperSimpleExt C D K

cl₁ carries the lower simple extension to the upper one.

theorem Tdaf.ConvexAnalysis.partialCl₂_upperSimpleExt {U : Type u_1} {X : Type u_2} [TopologicalSpace X] [AddCommGroup X] [IsTopologicalAddGroup X] {C : Set U} {D : Set X} {K : U × X → ℝ} (hDcl : IsClosed D) (hDne : D.Nonempty) (hcont : ∀ u ∈ C, ContinuousOn (fun (x : X) => K (u, x)) D) : partialCl₂ (upperSimpleExt C D K) = lowerSimpleExt C D K

cl₂ carries the upper simple extension back to the lower one.

The mirror of partialCl₁_lowerSimpleExt, transported rather than re-proved: partialCl₂_saddleSwap exchanges the two closures, upperSimpleExt_eq_saddleSwap exchanges the two extensions, and the continuity hypothesis passes through as ContinuousOn.neg.

theorem Tdaf.ConvexAnalysis.closedSaddleFn_of_mem_saddleClass_simpleExt {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [AddCommGroup U] [IsTopologicalAddGroup U] [TopologicalSpace X] [AddCommGroup X] [IsTopologicalAddGroup X] {C : Set U} {D : Set X} {K : U × X → ℝ} {L : U × X → EReal} (hCcl : IsClosed C) (hDcl : IsClosed D) (hCne : C.Nonempty) (hDne : D.Nonempty) (hcontD : ∀ u ∈ C, ContinuousOn (fun (x : X) => K (u, x)) D) (hcontC : ∀ x ∈ D, ContinuousOn (fun (u : U) => K (u, x)) C) (hL : L ∈ saddleClass (lowerSimpleExt C D K) (upperSimpleExt C D K)) : ClosedSaddleFn L

Every member of Ω is a closed saddle-function.

theorem Tdaf.ConvexAnalysis.saddleEquiv_of_mem_saddleClass_simpleExt {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [AddCommGroup U] [IsTopologicalAddGroup U] [TopologicalSpace X] [AddCommGroup X] [IsTopologicalAddGroup X] {C : Set U} {D : Set X} {K : U × X → ℝ} {L : U × X → EReal} (hCcl : IsClosed C) (hDcl : IsClosed D) (hCne : C.Nonempty) (hDne : D.Nonempty) (hcontD : ∀ u ∈ C, ContinuousOn (fun (x : X) => K (u, x)) D) (hcontC : ∀ x ∈ D, ContinuousOn (fun (u : U) => K (u, x)) C) (hL : L ∈ saddleClass (lowerSimpleExt C D K) (upperSimpleExt C D K)) : SaddleEquiv (lowerSimpleExt C D K) L

Ω is contained in a single equivalence class.

theorem Tdaf.ConvexAnalysis.mem_saddleClass_simpleExt_iff_saddleEquiv {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [AddCommGroup U] [IsTopologicalAddGroup U] [TopologicalSpace X] [AddCommGroup X] [IsTopologicalAddGroup X] {C : Set U} {D : Set X} {K : U × X → ℝ} {L : U × X → EReal} (hCcl : IsClosed C) (hDcl : IsClosed D) (hCne : C.Nonempty) (hDne : D.Nonempty) (hcontD : ∀ u ∈ C, ContinuousOn (fun (x : X) => K (u, x)) D) (hcontC : ∀ x ∈ D, ContinuousOn (fun (u : U) => K (u, x)) C) : L ∈ saddleClass (lowerSimpleExt C D K) (upperSimpleExt C D K) ↔ SaddleEquiv (lowerSimpleExt C D K) L

Ω is exactly the equivalence class of the lower simple extension, so the extensions of K with the prescribed infinite values form one full equivalence class of closed saddle-functions. Proved from closedness of the slices of the two simple extensions rather than from the bifunction representation, so the hypotheses are separate continuity in each variable rather than joint continuity.

theorem Tdaf.ConvexAnalysis.properSaddleFn_of_mem_saddleClass_simpleExt {U : Type u_1} {X : Type u_2} {C : Set U} {D : Set X} {K : U × X → ℝ} {L : U × X → EReal} (hCne : C.Nonempty) (hDne : D.Nonempty) (hL : L ∈ saddleClass (lowerSimpleExt C D K) (upperSimpleExt C D K)) : ProperSaddleFn L

Every member of Ω is proper.

The two brackets of a bifunction on a relative interior

The two brackets of a convex bifunction differ by a concave closure in the first variable. A concave function agrees with its closure on the relative interior of its effective domain, and the effective domain of u ↦ ⟨Fu, y⟩ is dom F on the nose — so on ri (dom F) the two brackets are simply equal.

theorem Tdaf.ConvexAnalysis.domConcave_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) (y : Y) : (domConcave fun (u : U) => bracket Bx F u y) = domBifun F

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

theorem Tdaf.ConvexAnalysis.bracket_eq_concaveBracket_adjointBifun_of_mem_relint {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] {F : Bifun U X} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (hF : ConvexBifun F) {u : U} (hu : u ∈ intrinsicInterior ℝ (domBifun F)) (y : Y) : bracket Bx F u y = concaveBracket Bu (adjointBifun Bu Bx F) u y

At a relative interior point of dom F the two brackets already agree — ⟨Fu, y⟩ = ⟨u, F* y⟩, with no closure in sight.

The two brackets of a polyhedral bifunction

The previous section puts the two brackets together on the relative interior of an effective domain, because that is where a convex or concave function must agree with its closure. A polyhedral function agrees with its closure on all of its effective domain, so for a polyhedral bifunction the equality extends to the domain itself, leaving uncovered only the pairs with u ∉ dom F and y ∉ dom F*, where the two brackets are -∞ and +∞. The u-side half needs no properness; the y-side half does, because it runs through F** = cl F = F.

theorem Tdaf.ConvexAnalysis.bracket_eq_bot_of_notMem_domBifun {U : Type u_1} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {F : Bifun U X} (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) {u : U} (hu : u ∉ domBifun F) (y : Y) : bracket Bx F u y = ⊥

Off dom F the bracket is -∞: there F u is identically +∞, and the conjugate of +∞ is -∞.

theorem Tdaf.ConvexAnalysis.concaveBracket_eq_top_of_notMem_domConcaveBifun {U : Type u_1} {V : Type u_2} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (G : Bifun Y V) (u : U) {y : Y} (hy : y ∉ domConcaveBifun G) : concaveBracket Bu G u y = ⊤

Off dom G the concave bracket is +∞, the mirror of bracket_eq_bot_of_notMem_domBifun.

theorem Tdaf.ConvexAnalysis.bracket_eq_concaveBracket_adjointBifun_of_mem_domBifun {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 →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (hF : PolyhedralBifun F) {u : U} (hu : u ∈ domBifun F) (y : Y) : bracket Bx F u y = concaveBracket Bu (adjointBifun Bu Bx F) u y

The u-side half: for a polyhedral convex bifunction the two brackets agree at every u of dom F, not merely at the relative-interior points that bracket_eq_concaveBracket_adjointBifun_of_mem_relint asks for.

The two differ by the concave closure in u; ⟨F·, y⟩ is polyhedral concave with effective domain dom F, and a polyhedral function agrees with its closure on all of its effective domain. Properness of F plays no part here.

theorem Tdaf.ConvexAnalysis.bracket_eq_concaveBracket_adjointBifun_of_mem_domConcaveBifun {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] [FiniteDimensional ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] {F : Bifun U X} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hF : PolyhedralBifun F) (hp : Proper (graphFn F)) (u : U) {y : Y} (hy : y ∈ domConcaveBifun (adjointBifun Bu Bx F)) : bracket Bx F u y = concaveBracket Bu (adjointBifun Bu Bx F) u y

The y-side half: for a proper polyhedral convex bifunction the two brackets agree at every y of dom F*, for every u.

This is the first half read on the dual side: the brackets differ by the convex closure in y once cl F = F, which properness plus polyhedrality supply; ⟨u, F*·⟩ is polyhedral convex with effective domain dom F*, so the closure changes nothing there.

theorem Tdaf.ConvexAnalysis.bracket_eq_concaveBracket_adjointBifun_of_polyhedral {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] [FiniteDimensional ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] {F : Bifun U X} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hF : PolyhedralBifun F) (hp : Proper (graphFn F)) (u : U) (y : Y) (h : u ∈ domBifun F ∨ y ∈ domConcaveBifun (adjointBifun Bu Bx F)) : bracket Bx F u y = concaveBracket Bu (adjointBifun Bu Bx F) u y

For a proper polyhedral convex bifunction the two brackets agree, ⟨Fu, y⟩ = ⟨u, F* y⟩, at every pair (u, y) except those with u ∉ dom F and y ∉ dom F*.

theorem Tdaf.ConvexAnalysis.bracket_eq_bot_and_concaveBracket_eq_top {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {F : Bifun U X} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) {u : U} (hu : u ∉ domBifun F) {y : Y} (hy : y ∉ domConcaveBifun (adjointBifun Bu Bx F)) : bracket Bx F u y = ⊥ ∧ concaveBracket Bu (adjointBifun Bu Bx F) u y = ⊤

The exceptional pairs: when u ∉ dom F and y ∉ dom F* one bracket is -∞ and the other +∞. Neither polyhedrality nor properness is used.

The bifunction behind a finite continuous saddle-function

The two simple extensions of a finite continuous saddle-function on a closed C × D are a closure pair, which is exactly what the representation by a closed convex bifunction asks for. Both closure computations are already done — they are what the class Ω runs on — so the result is their composition.

theorem Tdaf.ConvexAnalysis.lowerClosedFn_lowerSimpleExt {U : Type u_1} {Y : Type u_2} [TopologicalSpace U] [AddCommGroup U] [IsTopologicalAddGroup U] [TopologicalSpace Y] [AddCommGroup Y] [IsTopologicalAddGroup Y] {C : Set U} {D : Set Y} {K : U × Y → ℝ} (hCcl : IsClosed C) (hDcl : IsClosed D) (hCne : C.Nonempty) (hDne : D.Nonempty) (hcontD : ∀ u ∈ C, ContinuousOn (fun (x : Y) => K (u, x)) D) (hcontC : ∀ x ∈ D, ContinuousOn (fun (u : U) => K (u, x)) C) : LowerClosedFn (lowerSimpleExt C D K)

The lower simple extension is lower closed.

theorem Tdaf.ConvexAnalysis.upperClosedFn_upperSimpleExt {U : Type u_1} {Y : Type u_2} [TopologicalSpace U] [AddCommGroup U] [IsTopologicalAddGroup U] [TopologicalSpace Y] [AddCommGroup Y] [IsTopologicalAddGroup Y] {C : Set U} {D : Set Y} {K : U × Y → ℝ} (hCcl : IsClosed C) (hDcl : IsClosed D) (hCne : C.Nonempty) (hDne : D.Nonempty) (hcontD : ∀ u ∈ C, ContinuousOn (fun (x : Y) => K (u, x)) D) (hcontC : ∀ x ∈ D, ContinuousOn (fun (u : U) => K (u, x)) C) : UpperClosedFn (upperSimpleExt C D K)

The upper simple extension is upper closed.

theorem Tdaf.ConvexAnalysis.exists_unique_bifun_of_simpleExt {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] {C : Set U} {D : Set Y} {K : U × Y → ℝ} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hC : Convex ℝ C) (hCcl : IsClosed C) (hDcl : IsClosed D) (hCne : C.Nonempty) (hconv : ∀ u ∈ C, ConvexOn ℝ D fun (x : Y) => K (u, x)) (hconc : ∀ x ∈ D, ConcaveOn ℝ C fun (u : U) => K (u, x)) (hDne : D.Nonempty) (hcontD : ∀ u ∈ C, ContinuousOn (fun (x : Y) => K (u, x)) D) (hcontC : ∀ x ∈ D, ContinuousOn (fun (u : U) => K (u, x)) C) : ∃! F : Bifun U X, ConvexBifun F ∧ ClosedBifun F ∧ (fun (p : U × Y) => bracket Bx F p.1 p.2) = lowerSimpleExt C D K ∧ (fun (p : U × Y) => concaveBracket Bu (adjointBifun Bu Bx F) p.1 p.2) = upperSimpleExt C D K

A finite continuous concave-convex function on a nonempty closed C × D has a unique closed convex bifunction F whose two brackets are its lower and upper simple extensions. The explicit formulas for F and F* are the definitions of the conjugate and the concave conjugate of the slices.