Existence of saddle-values and saddle-points

Saddle/Conjugate.lean proves the D* halves of the criteria for a saddle-value; this module supplies the C* halves, turns the saddle-point criterion into a statement about K alone, and then specialises everything to a finite continuous concave-convex function on a product of closed convex sets — where the result is the classical minimax theorem.

The device is the involution saddleSwap K (y, u) = -K (u, y). Under it the class Ω (F) becomes the class Ω (F♯) for the negated flipped pairings -Bx.flip, -Bu.flip, where F♯ is the bifunction (F♯ y) v = -(F* y)(v), and the two conjugates are exchanged. So every C* statement is its D* companion read at the swapped data, and no new duality is needed. The pairings must be negated and not merely flipped: saddleSwap negates values, and only the negated pairings restore the sign of the linear terms in the two conjugates.

The file closes with the identification of ∂K with the subdifferential of the graph function of F, partially inverted along a linear homeomorphism.

Main results

• swapAdjointBifun, adjointBifun_swapAdjointBifun, saddleSwap_mem_bifunSaddleClass — the swap dictionary: saddleSwap carries Ω (F) onto Ω (F♯), and the adjoint of F♯ is -F; upperConjSaddle_saddleSwap, lowerConjSaddle_saddleSwap exchange the two conjugates.
• proper_graphFn_of_properSaddleFn — a proper member of Ω (F) forces Proper (graphFn F).
• zero_mem_interior_dom₁_lowerConjSaddle_iff — 0 ∈ int C* in terms of directions of recession; hasSaddleValue_of_no_common_direction_of_recession_neg — no common direction of recession in the first variable gives a saddle-value; hasSaddleValue_of_isBounded_dom₁ — likewise when C is bounded.
• exists_isSaddlePoint_of_no_common_direction_of_recession — a saddle-point exists when neither variable has a common direction of recession (Theorem 37.6 in [^1]); exists_isSaddlePoint_of_isBounded_domSaddle — likewise for a bounded effective domain.
• saddleStructure_lowerSimpleExt, maximin_lowerSimpleExt, exists_bifunSaddleClass_lowerSimpleExt — the transfer to a finite continuous concave-convex function on a closed C × D, through its lower simple extension.
• biSup_biInf_eq_biInf_biSup_of_isBounded_right — sup inf = inf sup with one factor bounded; exists_saddlePoint_of_isBounded — the minimax theorem (Corollary 37.6.2 in [^1]).
• isBifunSubgradientPair_iff_mem_subgradient_graphFn, setOf_mem_saddleSubgradient_eq_preimage — ∂K is ∂f partially inverted, pointwise and as an equality of graphs; isClosed_setOf_mem_saddleSubgradient — the graph of ∂K is closed.

Implementation notes

The sup inf = inf sup statements carry EReal-valued extrema. The customary display is inf_D sup_C K = sup_C inf_D K for a finite K, but with only one of C, D bounded the two iterated extrema can be ±∞. The minimax theorem, where both are bounded, is stated with real inequalities.

References

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

saddleSwap and the conjugate saddle-functions

theorem Tdaf.ConvexAnalysis.adjointBifun_neg_flipBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (F : Bifun U X) : adjointBifun (-Bx) (-Bu) (flipBifun F) = flipBifun (adjointBifun Bu Bx F)

The adjoint commutes with flipBifun once both pairings are negated and exchanged. This is the identity behind the whole swap dictionary: adjointBifun is an infimum over U × X of F u x + ⟨u, v⟩ - ⟨x, y⟩, and negating and exchanging the pairings restores that summand with the two bound variables exchanged.

theorem Tdaf.ConvexAnalysis.bracket_neg_flip_flipBifun_inverseBifun {U : Type u_1} {V : Type u_2} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (G : Bifun Y V) (y : Y) (u : U) : bracket (-Bu.flip) (flipBifun (inverseBifun G)) y u = -concaveBracket Bu G u y

The bracket of y ↦ -(G y ·) at the negated flipped pairing is minus the concave bracket of G. This is one of the two halves of the swap dictionary for equivalence classes.

theorem Tdaf.ConvexAnalysis.concaveBracket_neg_flip_flipBifun_inverseBifun {U : Type u_1} {X : Type u_3} {Y : Type u_4} [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (H : Bifun U X) (y : Y) (u : U) : concaveBracket (-Bx.flip) (flipBifun (inverseBifun H)) y u = -bracket Bx H u y

The mirror half: the concave bracket of u ↦ -(H u ·) at the negated flipped pairing is minus the bracket of H.

The class conjugate to Ω (F) seen through saddleSwap

noncomputable def Tdaf.ConvexAnalysis.swapAdjointBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (F : Bifun U X) : Bifun Y V

The convex bifunction attached to the swapped saddle-function: (F♯ y) v = -(F* y)(v).

It is not F_*^*, which goes from V to Y and belongs to the conjugate class on V × X; F♯ goes from Y to V, and the two differ by flipBifun. Its two brackets at the negated flipped pairings are the negatives of the two brackets of F, exchanged — which is what saddleSwap does to the class Ω (F).

Equations

• Tdaf.ConvexAnalysis.swapAdjointBifun Bu Bx F = Tdaf.ConvexAnalysis.flipBifun (Tdaf.ConvexAnalysis.inverseBifun (Tdaf.ConvexAnalysis.adjointBifun Bu Bx F))

@[simp]

theorem Tdaf.ConvexAnalysis.swapAdjointBifun_apply {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (F : Bifun U X) (y : Y) (v : V) : swapAdjointBifun Bu Bx F y v = -adjointBifun Bu Bx F y v

theorem Tdaf.ConvexAnalysis.convexBifun_swapAdjointBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (F : Bifun U X) : ConvexBifun (swapAdjointBifun Bu Bx F)

F♯ is a convex bifunction: it is F_*^* with its two arguments exchanged.

theorem Tdaf.ConvexAnalysis.closedBifun_swapAdjointBifun {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 V] [IsTopologicalAddGroup V] [TopologicalSpace Y] [IsTopologicalAddGroup Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsContinuousPairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsContinuousPairing Bx.flip] (F : Bifun U X) : ClosedBifun (swapAdjointBifun Bu Bx F)

F♯ is a closed bifunction, because an adjoint bifunction is closed.

theorem Tdaf.ConvexAnalysis.adjointBifun_swapAdjointBifun {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] {F : Bifun U X} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] (hF : ConvexBifun F) (hcl : ClosedBifun F) : adjointBifun (-Bx.flip) (-Bu.flip) (swapAdjointBifun Bu Bx F) = flipBifun (inverseBifun F)

The adjoint of F♯ is -F, which is the biadjoint identity (F_*^*)^* = F_* read through adjointBifun_neg_flipBifun.

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

The swap dictionary for equivalence classes: saddleSwap carries Ω (F) onto Ω (F♯) at the negated flipped pairings. Every statement about the first variable is therefore the corresponding statement about the second variable, read here.

The two conjugates of saddleSwap K

theorem Tdaf.ConvexAnalysis.upperConjSaddle_saddleSwap {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (K : U × Y → EReal) : upperConjSaddle (-Bx.flip) (-Bu.flip) (saddleSwap K) = saddleSwap (lowerConjSaddle Bu Bx K)

The upper conjugate of saddleSwap K is the swap of the lower conjugate of K. Negating both pairings turns a supremum-of-infima into an infimum-of-suprema.

theorem Tdaf.ConvexAnalysis.lowerConjSaddle_saddleSwap {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (K : U × Y → EReal) : lowerConjSaddle (-Bx.flip) (-Bu.flip) (saddleSwap K) = saddleSwap (upperConjSaddle Bu Bx K)

The lower conjugate of saddleSwap K is the swap of the upper conjugate of K.

Properness of the bifunction behind a proper class

theorem Tdaf.ConvexAnalysis.proper_graphFn_of_properSaddleFn {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] {F : Bifun U X} {K : U × Y → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (hK : K ∈ bifunSaddleClass Bu Bx F) (hp : ProperSaddleFn K) : Proper (graphFn F)

A proper member forces a proper bifunction. The two propernesses are usually not separated, but the results here ask for Proper (graphFn F) while the structural theorems deliver ProperSaddleFn K, so the bridge is crossed explicitly.

F u x = ⊥ would make the bracket ⟨Fu, y⟩ identically +∞, contradicting dom₂ K ≠ ∅; and F ≡ +∞ would make the upper bracket -∞, contradicting dom₁ K ≠ ∅.

The C* half of the saddle-value criteria

theorem Tdaf.ConvexAnalysis.separatingRight_neg_flip {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} (hB : B.SeparatingLeft) : (-B.flip).SeparatingRight

Negating and flipping a pairing exchanges its two separation properties.

theorem Tdaf.ConvexAnalysis.zero_mem_interior_dom₁_lowerConjSaddle_iff {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] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] {F : Bifun U X} {K : U × Y → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hB : Bu.SeparatingLeft) (hF : ConvexBifun F) (hcl : ClosedBifun F) (hK : K ∈ bifunSaddleClass Bu Bx F) (hKcc : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SaddleStructure K) : 0 ∈ interior (dom₁ (lowerConjSaddle Bu Bx K)) ↔ ∀ (z : U), z ≠ 0 → ∃ y ∈ intrinsicInterior ℝ (dom₂ K), 0 < recessionFn (fun (u : U) => -K (u, y)) z

The origin is an interior point of C* if and only if the convex functions -K (·, v), for v ∈ ri D, have no common direction of recession. This is the D* half read at saddleSwap K, whose class is Ω (F♯) for the negated flipped pairings.

theorem Tdaf.ConvexAnalysis.hasSaddleValue_of_no_common_direction_of_recession_neg {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} {K : U × Y → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hB : Bu.SeparatingLeft) (hF : ConvexBifun F) (hcl : ClosedBifun F) (hK : K ∈ bifunSaddleClass Bu Bx F) (hKcc : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SaddleStructure K) (hrec : ∀ (z : U), z ≠ 0 → ∃ y ∈ intrinsicInterior ℝ (dom₂ K), 0 < recessionFn (fun (u : U) => -K (u, y)) z) : HasSaddleValue K

If the convex functions -K (·, v) for v ∈ ri D have no common direction of recession, then the saddle-value of K exists.

theorem Tdaf.ConvexAnalysis.hasSaddleValue_of_isBounded_dom₁ {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} {K : U × Y → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hB : Bu.SeparatingLeft) (hF : ConvexBifun F) (hcl : ClosedBifun F) (hK : K ∈ bifunSaddleClass Bu Bx F) (hKcc : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SaddleStructure K) (hbd : Bornology.IsBounded (dom₁ K)) : HasSaddleValue K

If the first effective domain of K is bounded, the saddle-value of K exists.

Existence of a saddle-point

theorem Tdaf.ConvexAnalysis.exists_isSaddlePoint_of_no_common_direction_of_recession {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} {K : U × Y → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hBu : Bu.SeparatingLeft) (hBx : Bx.SeparatingRight) (hF : ConvexBifun F) (hcl : ClosedBifun F) (hK : K ∈ bifunSaddleClass Bu Bx F) (hKcc : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SaddleStructure K) (hrec₂ : ∀ (w : Y), w ≠ 0 → ∃ u ∈ intrinsicInterior ℝ (dom₁ K), 0 < recessionFn (fun (y : Y) => K (u, y)) w) (hrec₁ : ∀ (z : U), z ≠ 0 → ∃ y ∈ intrinsicInterior ℝ (dom₂ K), 0 < recessionFn (fun (u : U) => -K (u, y)) z) : ∃ (q : U × Y), IsSaddlePoint K q

If neither variable has a common direction of recession, K has a saddle-point. The two recession conditions translate into 0 ∈ int C* and 0 ∈ int D*, and ∂K* (0, 0) is then a nonempty set of saddle-points.

theorem Tdaf.ConvexAnalysis.exists_isSaddlePoint_of_isBounded_domSaddle {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} {K : U × Y → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hBu : Bu.SeparatingLeft) (hBx : Bx.SeparatingRight) (hF : ConvexBifun F) (hcl : ClosedBifun F) (hK : K ∈ bifunSaddleClass Bu Bx F) (hKcc : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SaddleStructure K) (hbd₁ : Bornology.IsBounded (dom₁ K)) (hbd₂ : Bornology.IsBounded (dom₂ K)) : ∃ (q : U × Y), IsSaddlePoint K q

If both halves of the effective domain of K are bounded, K has a saddle-point.

theorem Tdaf.ConvexAnalysis.exists_maximin_eq_coe_of_isBounded_domSaddle {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} {K : U × Y → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hBu : Bu.SeparatingLeft) (hBx : Bx.SeparatingRight) (hF : ConvexBifun F) (hcl : ClosedBifun F) (hK : K ∈ bifunSaddleClass Bu Bx F) (hKcc : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hs : SaddleStructure K) (hbd₁ : Bornology.IsBounded (dom₁ K)) (hbd₂ : Bornology.IsBounded (dom₂ K)) : ∃ (r : ℝ), maximin K = ↑r

The saddle-value is then finite — it is a value of K at a saddle-point, and a proper saddle-function is finite on its effective domain.

A finite continuous saddle-function on C × D

theorem Tdaf.ConvexAnalysis.saddleStructure_lowerSimpleExt {U : Type u_1} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] {C : Set U} {D : Set Y} {K : U × Y → ℝ} (hC : Convex ℝ C) (hCcl : IsClosed C) (hDcl : IsClosed D) (hCne : C.Nonempty) (hDne : D.Nonempty) (hconv : ∀ u ∈ C, ConvexOn ℝ D fun (x : Y) => K (u, x)) (hconc : ∀ x ∈ D, ConcaveOn ℝ C fun (u : U) => K (u, x)) (hcontD : ∀ u ∈ C, ContinuousOn (fun (x : Y) => K (u, x)) D) (hcontC : ∀ x ∈ D, ContinuousOn (fun (u : U) => K (u, x)) C) : SaddleStructure (lowerSimpleExt C D K)

The lower simple extension is a closed proper concave-convex function, so it has the full structural description.

theorem Tdaf.ConvexAnalysis.maximin_lowerSimpleExt {U : Type u_1} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] {C : Set U} {D : Set Y} {K : U × Y → ℝ} (hC : Convex ℝ C) (hCcl : IsClosed C) (hDcl : IsClosed D) (hCne : C.Nonempty) (hDne : D.Nonempty) (hconv : ∀ u ∈ C, ConvexOn ℝ D fun (x : Y) => K (u, x)) (hconc : ∀ x ∈ D, ConcaveOn ℝ C fun (u : U) => K (u, x)) (hcontD : ∀ u ∈ C, ContinuousOn (fun (x : Y) => K (u, x)) D) (hcontC : ∀ x ∈ D, ContinuousOn (fun (u : U) => K (u, x)) C) : maximin (lowerSimpleExt C D K) = ⨆ u ∈ C, ⨅ x ∈ D, ↑(K (u, x))

The sup inf of the lower simple extension over the whole space is the sup inf of K over C × D.

theorem Tdaf.ConvexAnalysis.minimax_lowerSimpleExt {U : Type u_1} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] {C : Set U} {D : Set Y} {K : U × Y → ℝ} (hC : Convex ℝ C) (hCcl : IsClosed C) (hDcl : IsClosed D) (hCne : C.Nonempty) (hDne : D.Nonempty) (hconv : ∀ u ∈ C, ConvexOn ℝ D fun (x : Y) => K (u, x)) (hconc : ∀ x ∈ D, ConcaveOn ℝ C fun (u : U) => K (u, x)) (hcontD : ∀ u ∈ C, ContinuousOn (fun (x : Y) => K (u, x)) D) (hcontC : ∀ x ∈ D, ContinuousOn (fun (u : U) => K (u, x)) C) : minimax (lowerSimpleExt C D K) = ⨅ x ∈ D, ⨆ u ∈ C, ↑(K (u, x))

The inf sup of the lower simple extension over the whole space is the inf sup of K over C × D.

theorem Tdaf.ConvexAnalysis.exists_bifunSaddleClass_lowerSimpleExt {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] {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) (hDne : D.Nonempty) (hconv : ∀ u ∈ C, ConvexOn ℝ D fun (x : Y) => K (u, x)) (hconc : ∀ x ∈ D, ConcaveOn ℝ C fun (u : U) => K (u, x)) (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 ∧ lowerSimpleExt C D K ∈ bifunSaddleClass Bu Bx F

The unique closed convex bifunction whose lower bracket is the lower simple extension, packaged with the membership K₁ ∈ Ω (F) that the results above consume.

theorem Tdaf.ConvexAnalysis.biSup_biInf_eq_biInf_biSup_of_isBounded_right {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] {C : Set U} {D : Set Y} {K : U × Y → ℝ} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hB : Bx.SeparatingRight) (hC : Convex ℝ C) (hCcl : IsClosed C) (hDcl : IsClosed D) (hCne : C.Nonempty) (hDne : D.Nonempty) (hconv : ∀ u ∈ C, ConvexOn ℝ D fun (x : Y) => K (u, x)) (hconc : ∀ x ∈ D, ConcaveOn ℝ C fun (u : U) => K (u, x)) (hcontD : ∀ u ∈ C, ContinuousOn (fun (x : Y) => K (u, x)) D) (hcontC : ∀ x ∈ D, ContinuousOn (fun (u : U) => K (u, x)) C) (hbd : Bornology.IsBounded D) : ⨆ u ∈ C, ⨅ x ∈ D, ↑(K (u, x)) = ⨅ x ∈ D, ⨆ u ∈ C, ↑(K (u, x))

The half where D is bounded: a finite continuous concave-convex function on a product of nonempty closed convex sets, one of them bounded, has sup inf = inf sup over C × D. The lower simple extension is a closed proper concave-convex function with effective domain C × D, so it has a saddle-value, and its extrema over the whole space are the restricted ones.

theorem Tdaf.ConvexAnalysis.biSup_biInf_eq_biInf_biSup_of_isBounded_left {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] {C : Set U} {D : Set Y} {K : U × Y → ℝ} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hB : Bu.SeparatingLeft) (hC : Convex ℝ C) (hCcl : IsClosed C) (hDcl : IsClosed D) (hCne : C.Nonempty) (hDne : D.Nonempty) (hconv : ∀ u ∈ C, ConvexOn ℝ D fun (x : Y) => K (u, x)) (hconc : ∀ x ∈ D, ConcaveOn ℝ C fun (u : U) => K (u, x)) (hcontD : ∀ u ∈ C, ContinuousOn (fun (x : Y) => K (u, x)) D) (hcontC : ∀ x ∈ D, ContinuousOn (fun (u : U) => K (u, x)) C) (hbd : Bornology.IsBounded C) : ⨆ u ∈ C, ⨅ x ∈ D, ↑(K (u, x)) = ⨅ x ∈ D, ⨆ u ∈ C, ↑(K (u, x))

The half where C is bounded.

theorem Tdaf.ConvexAnalysis.exists_saddlePoint_of_isBounded {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] {C : Set U} {D : Set Y} {K : U × Y → ℝ} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hBu : Bu.SeparatingLeft) (hBx : Bx.SeparatingRight) (hC : Convex ℝ C) (hCcl : IsClosed C) (hDcl : IsClosed D) (hCne : C.Nonempty) (hDne : D.Nonempty) (hconv : ∀ u ∈ C, ConvexOn ℝ D fun (x : Y) => K (u, x)) (hconc : ∀ x ∈ D, ConcaveOn ℝ C fun (u : U) => K (u, x)) (hcontD : ∀ u ∈ C, ContinuousOn (fun (x : Y) => K (u, x)) D) (hcontC : ∀ x ∈ D, ContinuousOn (fun (u : U) => K (u, x)) C) (hbdC : Bornology.IsBounded C) (hbdD : Bornology.IsBounded D) : ∃ (q : U × Y), q.1 ∈ C ∧ q.2 ∈ D ∧ (∀ u ∈ C, K (u, q.2) ≤ K q) ∧ ∀ x ∈ D, K q ≤ K (q.1, x)

The minimax theorem: a finite continuous concave-convex function on a product of nonempty compact convex sets has a saddle-point relative to that product. The bounded-domain criterion gives the lower simple extension a saddle-point, that saddle-point lies in C × D, and there the extension agrees with K.

∂K as the subdifferential of the graph function, partially inverted

theorem Tdaf.ConvexAnalysis.isBifunSubgradientPair_iff_mem_subgradient_graphFn {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (F : Bifun U X) (p : U × Y) (q : V × X) : IsBifunSubgradientPair Bu Bx F p q ↔ (-q.1, p.2) ∈ subgradient (prodPairing Bu Bx) (graphFn F) (p.1, q.2)

Membership in the subdifferential of the class Ω (F) is membership in the subdifferential of the graph function f of F, with the pair (u*, v) partially inverted to (-u*, v). No hypothesis on F is needed: it is the conjugate criterion for a subgradient together with the unconditional identity (F* v)(u*) = -f*(-u*, v).

theorem Tdaf.ConvexAnalysis.setOf_mem_saddleSubgradient_eq_preimage {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} {K : U × Y → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hF : ConvexBifun F) (hcl : ClosedBifun F) (hK : K ∈ bifunSaddleClass Bu Bx F) : {r : (U × Y) × V × X | r.2 ∈ saddleSubgradient Bu Bx.flip K r.1} = (fun (r : (U × Y) × V × X) => ((r.1.1, r.2.2), -r.2.1, r.1.2)) ⁻¹' subgradientRel (prodPairing Bu Bx) (graphFn F)

The graph of ∂K is the graph of ∂f partially inverted, f the graph function of F, as an equality of sets. The inversion (u, y, v, x) ↦ ((u, x), (-v, y)) is a linear homeomorphism, which is what makes closedness and maximal monotonicity transfer from ∂f.

theorem Tdaf.ConvexAnalysis.isClosed_setOf_mem_saddleSubgradient {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} {K : U × Y → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hcu : Continuous fun (r : U × V) => (Bu r.1) r.2) (hcx : Continuous fun (r : X × Y) => (Bx r.1) r.2) (hF : ConvexBifun F) (hcl : ClosedBifun F) (hpr : Proper (graphFn F)) (hK : K ∈ bifunSaddleClass Bu Bx F) : IsClosed {r : (U × Y) × V × X | r.2 ∈ saddleSubgradient Bu Bx.flip K r.1}

The graph of ∂K is closed: it is the preimage of the graph of ∂f under a linear homeomorphism, and the graph of the subdifferential of a closed proper convex function is closed. The homeomorphism clause is saddleSubgradientHomeomorph.