Minimax problems and conjugate saddle-functions

A function K of two variables has two iterated extrema, maximin K = ⨆ u, ⨅ x, K (u, x) and minimax K = ⨅ x, ⨆ u, K (u, x), the first never above the second; when they agree their common value is the saddle-value of K. A saddle-point is a point p at which K (·, p.2) is maximised and K (p.1, ·) minimised, which is exactly a pair of optimal strategies together with the existence of the saddle-value. For a closed proper concave-convex K the whole space may be replaced by dom K without changing either extremum, and both depend only on the equivalence class of K.

The Lagrangian of a convex program is a saddle-function whose saddle-points are the pairs "optimal solution, Kuhn–Tucker vector", whence the general Kuhn–Tucker theorem; and the Lagrangians of closed convex programs are exactly the upper closed concave-convex functions.

The last part turns the iterated extrema into a conjugacy: -K̲*(0, 0) and -K̄*(0, 0) are minimax K and maximin K, and both conjugates of every member of a class Ω (F) are read off from F alone — the upper one is the Lagrangian of F, the lower one the bracket of F_*^*. So the saddle-value exists exactly when the two conjugates agree at the origin.

Main definitions

• IsSaddlePoint K p, IsSaddlePointOn K C D p — the saddle-point condition, over the whole space and relative to C × D.
• maximin K, minimax K, HasSaddleValue K — the two iterated extrema and their equality.
• saddleLagrangian Bu F — the Lagrangian of (P) read as a saddle-function on V × X; flipBifun F and inverseBifun F — arguments exchanged, and Rockafellar's F_*.
• lowerConjSaddle Bu Bx K, upperConjSaddle Bu Bx K — the conjugates K̲*, K̄*; bifunSaddleClass Bu Bx F — the class Ω (F), squeezed between the two brackets of F.

Main results

• maximin_le_minimax — sup inf ≤ inf sup; isSaddlePoint_iff_attained — a saddle-point is a pair of attained outer extrema that agree. Neither needs any structure at all, not even nonemptiness of the two spaces.
• isSaddlePoint_iff_iSup_eq_iInf — the one-equation form of the saddle-point condition, on which everything downstream is a computation of ⨆ u, K (u, x) and ⨅ x, K (u, x).
• maximin_eq_biSup_biInf, isSaddlePoint_iff_isSaddlePointOn_dom — for a closed proper K both extrema and all saddle-points already live on dom K; IsSaddlePoint.mem_domSaddle — a saddle-point of a proper K lies in dom K; SaddleEquiv.maximin_eq — the two extrema see only the equivalence class.
• isSaddlePoint_lagrangian_iff — the saddle-points of the Lagrangian are the pairs "Kuhn–Tucker vector, optimal solution"; isSaddlePoint_lagrangian_iff_normal_and_optimal — the same read through normality; mem_argmin_iff_exists_isSaddlePoint_lagrangian — the general Kuhn–Tucker theorem (Theorem 36.6 in [^1]); exists_unique_closedBifun_saddleLagrangian_eq — Lagrangians are exactly the upper closed concave-convex functions (Theorem 36.5 in [^1]).
• hasSaddleValue_iff_conjSaddle_zero_eq — the saddle-value read off at the origin.
• upperConjSaddle_eq_saddleLagrangian, lowerConjSaddle_eq_bracket_inverseBifun — the two conjugates of a member of Ω (F), in terms of F alone (Theorem 37.1 in [^1]); concaveConvexFn_upperConjSaddle and companions — they are again concave-convex, and closed.

Implementation notes

HasSaddleValue K is the bare equation maximin K = minimax K; as in the book, finiteness of the common value is a separate conclusion. The extrema are taken over the whole space, the ±∞ extension making a problem on C × D into one on the product; IsSaddlePointOn records that.

Rockafellar writes the Lagrangian as L (v, x) = ⟨v, F_* x⟩ and the bifunction behind the lower conjugate as F_*^*, both through the concave inverse. There is no concave adjoint of a concave bifunction here, so inverseBifun (adjointBifun Bu Bx F) is the definition of F_*^*; and the characterisation of Lagrangians goes through saddleSwap, which turns the Lagrangian into a bracket of flipBifun F for the negated pairing, where the convex theory applies verbatim.

References

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

Saddle-points and the two iterated extrema

def Tdaf.ConvexAnalysis.IsSaddlePoint {U : Type u_1} {X : Type u_2} (K : U × X → EReal) (p : U × X) : Prop

p is a saddle-point of K: the concave variable is maximised and the convex variable is minimised there.

Equations

• Tdaf.ConvexAnalysis.IsSaddlePoint K p = ((∀ (u : U), K (u, p.2) ≤ K p) ∧ ∀ (x : X), K p ≤ K (p.1, x))

def Tdaf.ConvexAnalysis.IsSaddlePointOn {U : Type u_1} {X : Type u_2} (K : U × X → EReal) (C : Set U) (D : Set X) (p : U × X) : Prop

p is a saddle-point of K relative to C × D: Rockafellar's saddle-point with respect to maximising over C and minimising over D.

Equations

• Tdaf.ConvexAnalysis.IsSaddlePointOn K C D p = (p.1 ∈ C ∧ p.2 ∈ D ∧ (∀ u ∈ C, K (u, p.2) ≤ K p) ∧ ∀ x ∈ D, K p ≤ K (p.1, x))

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

Rockafellar's sup inf.

Equations

• Tdaf.ConvexAnalysis.maximin K = ⨆ (u : U), ⨅ (x : X), K (u, x)

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

Rockafellar's inf sup.

Equations

• Tdaf.ConvexAnalysis.minimax K = ⨅ (x : X), ⨆ (u : U), K (u, x)

theorem Tdaf.ConvexAnalysis.maximin_apply {U : Type u_1} {X : Type u_2} (K : U × X → EReal) : maximin K = ⨆ (u : U), ⨅ (x : X), K (u, x)

theorem Tdaf.ConvexAnalysis.minimax_apply {U : Type u_1} {X : Type u_2} (K : U × X → EReal) : minimax K = ⨅ (x : X), ⨆ (u : U), K (u, x)

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

The saddle-value of K exists when the two iterated extrema agree. Following Rockafellar, this says nothing about the common value being finite.

Equations

• Tdaf.ConvexAnalysis.HasSaddleValue K = (Tdaf.ConvexAnalysis.maximin K = Tdaf.ConvexAnalysis.minimax K)

theorem Tdaf.ConvexAnalysis.hasSaddleValue_iff {U : Type u_1} {X : Type u_2} {K : U × X → EReal} : HasSaddleValue K ↔ maximin K = minimax K

theorem Tdaf.ConvexAnalysis.maximin_le_minimax {U : Type u_1} {X : Type u_2} (K : U × X → EReal) : maximin K ≤ minimax K

sup inf ≤ inf sup. No hypothesis at all is needed — in particular neither U nor X need be nonempty.

theorem Tdaf.ConvexAnalysis.iInf_slice_le_maximin {U : Type u_1} {X : Type u_2} (K : U × X → EReal) (u : U) : ⨅ (x : X), K (u, x) ≤ maximin K

theorem Tdaf.ConvexAnalysis.minimax_le_iSup_slice {U : Type u_1} {X : Type u_2} (K : U × X → EReal) (x : X) : minimax K ≤ ⨆ (u : U), K (u, x)

theorem Tdaf.ConvexAnalysis.iInf_slice_le_self {U : Type u_1} {X : Type u_2} (K : U × X → EReal) (p : U × X) : ⨅ (x : X), K (p.1, x) ≤ K p

theorem Tdaf.ConvexAnalysis.le_iSup_slice {U : Type u_1} {X : Type u_2} (K : U × X → EReal) (p : U × X) : K p ≤ ⨆ (u : U), K (u, p.2)

theorem Tdaf.ConvexAnalysis.isSaddlePoint_iff_iSup_eq_iInf {U : Type u_1} {X : Type u_2} {K : U × X → EReal} {p : U × X} : IsSaddlePoint K p ↔ ⨆ (u : U), K (u, p.2) = ⨅ (x : X), K (p.1, x)

The saddle-point condition in one equation: p is a saddle-point exactly when the maximum of K (·, p.2) and the minimum of K (p.1, ·) agree, the common value being K p.

theorem Tdaf.ConvexAnalysis.IsSaddlePoint.iSup_eq {U : Type u_1} {X : Type u_2} {K : U × X → EReal} {p : U × X} (h : IsSaddlePoint K p) : ⨆ (u : U), K (u, p.2) = K p

theorem Tdaf.ConvexAnalysis.IsSaddlePoint.iInf_eq {U : Type u_1} {X : Type u_2} {K : U × X → EReal} {p : U × X} (h : IsSaddlePoint K p) : ⨅ (x : X), K (p.1, x) = K p

theorem Tdaf.ConvexAnalysis.isSaddlePoint_iff_attained {U : Type u_1} {X : Type u_2} {K : U × X → EReal} {p : U × X} : IsSaddlePoint K p ↔ ⨅ (x : X), K (p.1, x) = maximin K ∧ ⨆ (u : U), K (u, p.2) = minimax K ∧ HasSaddleValue K

p is a saddle-point exactly when the outer supremum in sup inf is attained at p.1, the outer infimum in inf sup is attained at p.2, and the two extrema are equal.

theorem Tdaf.ConvexAnalysis.IsSaddlePoint.maximin_eq {U : Type u_1} {X : Type u_2} {K : U × X → EReal} {p : U × X} (h : IsSaddlePoint K p) : maximin K = K p

At a saddle-point the saddle-value is K p.

theorem Tdaf.ConvexAnalysis.IsSaddlePoint.minimax_eq {U : Type u_1} {X : Type u_2} {K : U × X → EReal} {p : U × X} (h : IsSaddlePoint K p) : minimax K = K p

theorem Tdaf.ConvexAnalysis.IsSaddlePoint.hasSaddleValue {U : Type u_1} {X : Type u_2} {K : U × X → EReal} {p : U × X} (h : IsSaddlePoint K p) : HasSaddleValue K

theorem Tdaf.ConvexAnalysis.isSaddlePointOn_iff_biSup_eq_biInf {U : Type u_1} {X : Type u_2} {K : U × X → EReal} {p : U × X} {C : Set U} {D : Set X} (h₁ : p.1 ∈ C) (h₂ : p.2 ∈ D) : IsSaddlePointOn K C D p ↔ ⨆ u ∈ C, K (u, p.2) = ⨅ x ∈ D, K (p.1, x)

A saddle-point relative to C × D is characterised by the same one equation, now with the two extrema restricted.

@[simp]

theorem Tdaf.ConvexAnalysis.isSaddlePointOn_univ_univ {U : Type u_1} {X : Type u_2} {K : U × X → EReal} {p : U × X} : IsSaddlePointOn K Set.univ Set.univ p ↔ IsSaddlePoint K p

Restricting the outer extrema to the effective domains

theorem Tdaf.ConvexAnalysis.iInf_slice_eq_bot_of_notMem_dom₁ {U : Type u_1} {X : Type u_2} {K : U × X → EReal} {u : U} (hu : u ∉ dom₁ K) : ⨅ (x : X), K (u, x) = ⊥

theorem Tdaf.ConvexAnalysis.iSup_slice_eq_top_of_notMem_dom₂ {U : Type u_1} {X : Type u_2} {K : U × X → EReal} {x : X} (hx : x ∉ dom₂ K) : ⨆ (u : U), K (u, x) = ⊤

theorem Tdaf.ConvexAnalysis.maximin_eq_biSup_dom₁ {U : Type u_1} {X : Type u_2} (K : U × X → EReal) : maximin K = ⨆ u ∈ dom₁ K, ⨅ (x : X), K (u, x)

The outer supremum in sup inf may always be restricted to dom₁ K: off it the inner infimum is −∞.

theorem Tdaf.ConvexAnalysis.minimax_eq_biInf_dom₂ {U : Type u_1} {X : Type u_2} (K : U × X → EReal) : minimax K = ⨅ x ∈ dom₂ K, ⨆ (u : U), K (u, x)

The outer infimum in inf sup may always be restricted to dom₂ K: off it the inner supremum is +∞.

The two extrema see only the equivalence class

theorem Tdaf.ConvexAnalysis.iSup_clConcave_eq_iSup {E : Type u_1} [TopologicalSpace E] [AddCommGroup E] (g : E → EReal) : ⨆ (x : E), clConcave g x = ⨆ (x : E), g x

The concave mirror of iInf_clFn_eq_iInf: a concave function and its concave closure have the same supremum. Like its convex original it needs no convexity.

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

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

theorem Tdaf.ConvexAnalysis.SaddleEquiv.iInf_slice_eq {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] [AddCommGroup X] {K L : U × X → EReal} (h : SaddleEquiv K L) (u : U) : ⨅ (x : X), K (u, x) = ⨅ (x : X), L (u, x)

Equivalent saddle-functions have the same inner infima — "two convex functions with the same closure have the same infimum".

theorem Tdaf.ConvexAnalysis.SaddleEquiv.iSup_slice_eq {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [AddCommGroup U] [TopologicalSpace X] {K L : U × X → EReal} (h : SaddleEquiv K L) (x : X) : ⨆ (u : U), K (u, x) = ⨆ (u : U), L (u, x)

Equivalent saddle-functions have the same inner suprema.

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

Equivalent saddle-functions have the same sup inf.

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

Equivalent saddle-functions have the same inf sup.

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

Equivalent saddle-functions have the same saddle-value.

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

Equivalent saddle-functions have the same saddle-points. The saddle-point condition is an equation between an inner supremum and an inner infimum (isSaddlePoint_iff_iSup_eq_iInf), and equivalence preserves both.

Saddle-points of a proper saddle-function

theorem Tdaf.ConvexAnalysis.IsSaddlePoint.mem_domSaddle {U : Type u_1} {X : Type u_2} {K : U × X → EReal} {p : U × X} (hp : ProperSaddleFn K) (h : IsSaddlePoint K p) : p ∈ domSaddle K

A saddle-point of a proper saddle-function lies in its effective domain. Only properness is used.

theorem Tdaf.ConvexAnalysis.IsSaddlePoint.exists_maximin_eq_coe {U : Type u_1} {X : Type u_2} {K : U × X → EReal} {p : U × X} (hp : ProperSaddleFn K) (h : IsSaddlePoint K p) : ∃ (r : ℝ), maximin K = ↑r

The saddle-value at a saddle-point of a proper saddle-function is finite.

Minimising a convex function over a set containing the relative interior

theorem Tdaf.ConvexAnalysis.ConvexFn.biInf_eq_iInf_of_relint_dom_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ConvexFn f) {S : Set E} (hS : intrinsicInterior ℝ (dom f) ⊆ S) : ⨅ x ∈ S, f x = ⨅ (x : E), f x

Minimising a convex function over any set that contains ri (dom f) already gives the global infimum.

The extrema and the saddle-points live on the effective domain

theorem Tdaf.ConvexAnalysis.biInf_dom₂_eq_iInf_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 : SaddleStructure K) (hp : ProperSaddleFn K) (u : U) : ⨅ x ∈ dom₂ K, K (u, x) = ⨅ (x : X), K (u, x)

The inner infimum: for a closed proper concave-convex K the infimum of a slice over all of X is already reached over D = dom₂ K.

theorem Tdaf.ConvexAnalysis.biSup_dom₁_eq_iSup_slice {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) (hs : SaddleStructure K) (hp : ProperSaddleFn K) (x : X) : ⨆ u ∈ dom₁ K, K (u, x) = ⨆ (u : U), K (u, x)

The inner supremum: the mirror of biInf_dom₂_eq_iInf_slice, obtained from it at the swapped saddle-function.

theorem Tdaf.ConvexAnalysis.maximin_eq_biSup_biInf {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 : SaddleStructure K) (hp : ProperSaddleFn K) : maximin K = ⨆ u ∈ dom₁ K, ⨅ x ∈ dom₂ K, K (u, x)

sup inf over the whole space is sup inf over C × D.

theorem Tdaf.ConvexAnalysis.minimax_eq_biInf_biSup {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) (hs : SaddleStructure K) (hp : ProperSaddleFn K) : minimax K = ⨅ x ∈ dom₂ K, ⨆ u ∈ dom₁ K, K (u, x)

inf sup over the whole space is inf sup over C × D.

theorem Tdaf.ConvexAnalysis.isSaddlePoint_iff_isSaddlePointOn_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} {p : U × X} (hK : ConcaveConvexFn K) (hs : SaddleStructure K) (hp : ProperSaddleFn K) : IsSaddlePoint K p ↔ IsSaddlePointOn K (dom₁ K) (dom₂ K) p

The saddle-points of K with respect to the whole space are exactly its saddle-points with respect to C × D = dom K.

Slices of a bifunction in its first variable

theorem Tdaf.ConvexAnalysis.ConvexBifun.convexFn_flip {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {F : Bifun U X} (hF : ConvexBifun F) (x : X) : ConvexFn fun (u : U) => F u x

Each first-variable slice F (·) x of a convex bifunction is convex. Not an instance of convexFn_compLin, because u ↦ (u, x) is affine and not linear.

theorem Tdaf.ConvexAnalysis.ClosedBifun.closedFn_flip {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [AddCommGroup U] [IsTopologicalAddGroup U] [TopologicalSpace X] [AddCommGroup X] [IsTopologicalAddGroup X] {F : Bifun U X} (hF : ClosedBifun F) (x : X) : ClosedFn fun (u : U) => F u x

Each first-variable slice of a closed bifunction is closed — the mirror of ClosedBifun.imageClosedBifun.

The Lagrangian as a saddle-function

noncomputable def Tdaf.ConvexAnalysis.saddleLagrangian {U : Type u_1} {V : Type u_2} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (F : Bifun U X) : V × X → EReal

The Lagrangian of (P) read as a function on the product V × X, i.e. as a saddle-function. The minimax problem studied below is the one for exactly this function.

Equations

• Tdaf.ConvexAnalysis.saddleLagrangian Bu F q = Tdaf.ConvexAnalysis.lagrangian Bu F q.1 q.2

theorem Tdaf.ConvexAnalysis.saddleLagrangian_apply {U : Type u_1} {V : Type u_2} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (F : Bifun U X) (q : V × X) : saddleLagrangian Bu F q = lagrangian Bu F q.1 q.2

Saddle-points of the Lagrangian

theorem Tdaf.ConvexAnalysis.iSup_lagrangian {U : Type u_1} {V : Type u_2} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {F : Bifun U X} {x : X} (hf : ConvexFn fun (u : U) => F u x) : ⨆ (w : V), lagrangian Bu F w x = clFn (fun (u : U) => F u x) 0

The companion of iInf_lagrangian: maximising the Lagrangian over the price variable gives the closure of the objective slice at the origin. This is the computation behind the criterion.

theorem Tdaf.ConvexAnalysis.iSup_lagrangian_eq {U : Type u_1} {V : Type u_2} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {F : Bifun U X} {x : X} (hF : ConvexBifun F) (hcl : ClosedBifun F) : ⨆ (w : V), lagrangian Bu F w x = F 0 x

For a closed convex bifunction the supremum of the Lagrangian over the price variable is the objective (F 0)(x) itself.

theorem Tdaf.ConvexAnalysis.iInf_lagrangian_ne_top {U : Type u_1} {V : Type u_2} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {F : Bifun U X} {v : V} (hpr : Proper (graphFn F)) : ⨅ (y : X), lagrangian Bu F v y ≠ ⊤

Properness bounds the Lagrangian's infimum away from +∞.

theorem Tdaf.ConvexAnalysis.isSaddlePoint_lagrangian_iff {U : Type u_1} {V : Type u_2} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {F : Bifun U X} {v : V} {x : X} (hF : ConvexBifun F) (hcl : ClosedBifun F) (hpr : Proper (graphFn F)) : IsSaddlePoint (saddleLagrangian Bu F) (v, x) ↔ v ∈ KuhnTucker Bu F ∧ x ∈ argmin (F 0)

(v, x) is a saddle-point of the Lagrangian of (P) exactly when v is a Kuhn–Tucker vector for (P) and x is an optimal solution to (P).

The proof is the book's: ⨅ y, L (v, y) ≤ inf F 0 ≤ (F 0) x = ⨆ w, L (w, x), whose outer terms are respectively ≠ ⊤ and ≠ ⊥ by properness, so the saddle-point condition collapses the chain.

The general Kuhn–Tucker theorem

theorem Tdaf.ConvexAnalysis.iInf_lagrangian_eq_adjointBifun_zero {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 →ₗ[ℝ] ℝ} {F : Bifun U X} {v : V} (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) : ⨅ (y : X), lagrangian Bu F v y = adjointBifun Bu Bx F 0 v

Minimising the Lagrangian over the convex variable is evaluating the dual objective F* 0: both are ⨅ u (⟨u, v⟩ + inf F u).

theorem Tdaf.ConvexAnalysis.isSaddlePoint_lagrangian_iff_le_adjointBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {F : Bifun U X} {v : V} {x : X} (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (hF : ConvexBifun F) (hcl : ClosedBifun F) : IsSaddlePoint (saddleLagrangian Bu F) (v, x) ↔ F 0 x ≤ adjointBifun Bu Bx F 0 v

(v, x) is a saddle-point of the Lagrangian exactly when the primal objective at x is no larger than the dual objective at v — in which case weak duality forces equality.

theorem Tdaf.ConvexAnalysis.isSaddlePoint_lagrangian_iff_normal_and_optimal {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] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {F : Bifun U X} {v : V} {x : X} (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (hF : ConvexBifun F) (hcl : ClosedBifun F) (hpr : Proper (graphFn F)) : IsSaddlePoint (saddleLagrangian Bu F) (v, x) ↔ Normal F ∧ x ∈ argmin (F 0) ∧ adjointBifun Bu Bx F 0 v = ⨆ (w : V), adjointBifun Bu Bx F 0 w

(v, x) is a saddle-point of the Lagrangian exactly when normality holds and x, v are optimal for (P) and (P*).

theorem Tdaf.ConvexAnalysis.mem_argmin_iff_exists_isSaddlePoint_lagrangian {U : Type u_1} {V : Type u_2} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {F : Bifun U X} {x : X} (hF : ConvexBifun F) (hcl : ClosedBifun F) (hpr : Proper (graphFn F)) (hkt : (KuhnTucker Bu F).Nonempty) : x ∈ argmin (F 0) ↔ ∃ (v : V), IsSaddlePoint (saddleLagrangian Bu F) (v, x)

The general Kuhn–Tucker theorem: once one Kuhn–Tucker vector is known to exist, x solves (P) exactly when some v makes (v, x) a saddle-point of the Lagrangian, and the v that do are precisely the Kuhn–Tucker vectors.

theorem Tdaf.ConvexAnalysis.isSaddlePoint_lagrangian_iff_mem_kuhnTucker {U : Type u_1} {V : Type u_2} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {F : Bifun U X} {v : V} {x : X} (hF : ConvexBifun F) (hcl : ClosedBifun F) (hpr : Proper (graphFn F)) (hx : x ∈ argmin (F 0)) : IsSaddlePoint (saddleLagrangian Bu F) (v, x) ↔ v ∈ KuhnTucker Bu F

The "which v" clause: for an optimal x, the prices v completing it to a saddle-point of the Lagrangian are exactly the Kuhn–Tucker vectors.

theorem Tdaf.ConvexAnalysis.mem_argmin_iff_exists_isSaddlePoint_lagrangian_of_stronglyConsistent {U : Type u_1} {V : Type u_2} {X : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] {F : Bifun U X} {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {x : X} (hF : ConvexBifun F) (hcl : ClosedBifun F) (hpr : Proper (graphFn F)) (hip : Proper (infBifun F)) (hs : StronglyConsistent F) (ht : infBifun F 0 ≠ ⊤) : x ∈ argmin (F 0) ↔ ∃ (v : V), IsSaddlePoint (saddleLagrangian Bu F) (v, x)

The Kuhn–Tucker theorem under the strong-consistency qualification: for a strongly consistent closed proper convex program, x is an optimal solution exactly when it is the convex half of a saddle-point of the Lagrangian.

Lagrangians are exactly the upper closed concave-convex functions

def Tdaf.ConvexAnalysis.flipBifun {U : Type u_1} {X : Type u_2} (F : Bifun U X) : Bifun X U

The bifunction with its two arguments exchanged. Unlike Rockafellar's inverse operation F_* this does not negate, so it stays convex; it is what lets the convex bracket theory be applied to the swapped saddle-function.

Equations

• Tdaf.ConvexAnalysis.flipBifun F x u = F u x

@[simp]

theorem Tdaf.ConvexAnalysis.flipBifun_apply {U : Type u_1} {X : Type u_2} (F : Bifun U X) (x : X) (u : U) : flipBifun F x u = F u x

@[simp]

theorem Tdaf.ConvexAnalysis.flipBifun_flipBifun {U : Type u_1} {X : Type u_2} (F : Bifun U X) : flipBifun (flipBifun F) = F

theorem Tdaf.ConvexAnalysis.graphFn_flipBifun {U : Type u_1} {X : Type u_2} (F : Bifun U X) (q : X × U) : graphFn (flipBifun F) q = graphFn F (q.2, q.1)

theorem Tdaf.ConvexAnalysis.convexBifun_flipBifun {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {F : Bifun U X} (hF : ConvexBifun F) : ConvexBifun (flipBifun F)

Exchanging the two arguments preserves convexity.

theorem Tdaf.ConvexAnalysis.closedBifun_flipBifun {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [AddCommGroup U] [IsTopologicalAddGroup U] [TopologicalSpace X] [AddCommGroup X] [IsTopologicalAddGroup X] {F : Bifun U X} (hF : ClosedBifun F) : ClosedBifun (flipBifun F)

Exchanging the two arguments preserves closedness.

theorem Tdaf.ConvexAnalysis.saddleSwap_saddleLagrangian {U : Type u_1} {V : Type u_2} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (F : Bifun U X) : saddleSwap (saddleLagrangian Bu F) = fun (q : X × V) => bracket (-Bu) (flipBifun F) q.1 q.2

The Lagrangian is a bracket, after swapping. Rockafellar writes it L (v, x) = ⟨v, F_* x⟩, through the inverse bifunction; the same identity, negated and with the variables exchanged, is the bracket of flipBifun F for the negated pairing, where the convex theory applies verbatim.

theorem Tdaf.ConvexAnalysis.concaveConvexFn_saddleLagrangian {U : Type u_1} {V : Type u_2} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] {F : Bifun U X} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (hF : ConvexBifun F) : ConcaveConvexFn (saddleLagrangian Bu F)

The Lagrangian of a convex program is a concave-convex function: the brackets of a convex bifunction are, and the Lagrangian is one of them after swapping.

theorem Tdaf.ConvexAnalysis.upperClosedFn_saddleLagrangian {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 V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] [LocallyConvexSpace ℝ V] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] {F : Bifun U X} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] (hF : ConvexBifun F) (hcl : ClosedBifun F) : UpperClosedFn (saddleLagrangian Bu F)

The Lagrangian of a closed convex bifunction is an upper closed concave-convex function.

theorem Tdaf.ConvexAnalysis.exists_unique_closedBifun_saddleLagrangian_eq {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 V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] [LocallyConvexSpace ℝ V] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] {L : V × X → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] (hL : ConcaveConvexFn L) (huc : UpperClosedFn L) : ∃! G : Bifun U X, ConvexBifun G ∧ ClosedBifun G ∧ saddleLagrangian Bu G = L

Every upper closed concave-convex function on V × X is the Lagrangian of one and only one closed convex bifunction from U to X.

Conjugate saddle-functions

The inverse of a bifunction

theorem Tdaf.ConvexAnalysis.inverseBifun_eq_flipBifun_neg {U : Type u_1} {X : Type u_2} (F : Bifun U X) : inverseBifun F = flipBifun fun (u : U) (x : X) => -F u x

The inverse is flipBifun composed with a change of sign.

theorem Tdaf.ConvexAnalysis.convexBifun_inverseBifun {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {G : Bifun U X} (hG : ConcaveBifun G) : ConvexBifun (inverseBifun G)

The inverse of a concave bifunction is convex.

theorem Tdaf.ConvexAnalysis.closedBifun_inverseBifun {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [AddCommGroup U] [IsTopologicalAddGroup U] [TopologicalSpace X] [AddCommGroup X] [IsTopologicalAddGroup X] {G : Bifun U X} (hG : ClosedConcaveFn (graphFn G)) : ClosedBifun (inverseBifun G)

The inverse of a concave-closed bifunction is closed.

The concave conjugate sees only the concave closure

theorem Tdaf.ConvexAnalysis.concaveConj_clConcave {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] [IsTopologicalAddGroup E] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsContinuousPairing B] (g : E → EReal) : concaveConj B (clConcave g) = concaveConj B g

The concave conjugate sees only the concave closure: (cl g)* = g*. This is conj_clFn read through the sign dictionary, and it is what makes the lower conjugate independent of the representative of the equivalence class.

The lower and upper conjugates of a saddle-function

noncomputable def Tdaf.ConvexAnalysis.lowerConjSaddle {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) : V × X → EReal

The lower conjugate K̲* of a saddle-function: K̲* (u*, x) = ⨆ y, ⨅ u, {⟨u, u*⟩ + ⟨x, y⟩ - K (u, y)}.

Equations

• Tdaf.ConvexAnalysis.lowerConjSaddle Bu Bx K q = ⨆ (y : Y), ⨅ (u : U), ↑((Bu u) q.1 + (Bx q.2) y) - K (u, y)

noncomputable def Tdaf.ConvexAnalysis.upperConjSaddle {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) : V × X → EReal

The upper conjugate K̄* of a saddle-function: K̄* (u*, x) = ⨅ u, ⨆ y, {⟨u, u*⟩ + ⟨x, y⟩ - K (u, y)}.

Equations

• Tdaf.ConvexAnalysis.upperConjSaddle Bu Bx K q = ⨅ (u : U), ⨆ (y : Y), ↑((Bu u) q.1 + (Bx q.2) y) - K (u, y)

theorem Tdaf.ConvexAnalysis.lowerConjSaddle_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 →ₗ[ℝ] ℝ) (K : U × Y → EReal) (q : V × X) : lowerConjSaddle Bu Bx K q = ⨆ (y : Y), ⨅ (u : U), ↑((Bu u) q.1 + (Bx q.2) y) - K (u, y)

theorem Tdaf.ConvexAnalysis.upperConjSaddle_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 →ₗ[ℝ] ℝ) (K : U × Y → EReal) (q : V × X) : upperConjSaddle Bu Bx K q = ⨅ (u : U), ⨆ (y : Y), ↑((Bu u) q.1 + (Bx q.2) y) - K (u, y)

theorem Tdaf.ConvexAnalysis.lowerConjSaddle_le_upperConjSaddle {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 Bu Bx K ≤ upperConjSaddle Bu Bx K

The lower conjugate never exceeds the upper one, K̲* ≤ K̄*, by sup inf ≤ inf sup.

noncomputable def Tdaf.ConvexAnalysis.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] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (F : Bifun U X) : Set (U × Y → EReal)

The equivalence class Ω (F) of saddle-functions attached to a convex bifunction: the concave-convex functions squeezed between the two brackets of F.

Equations

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

theorem Tdaf.ConvexAnalysis.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] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} {F : Bifun U X} {K : U × Y → EReal} : K ∈ bifunSaddleClass Bu Bx F ↔ (fun (p : U × Y) => bracket Bx F p.1 p.2) ≤ K ∧ K ≤ fun (p : U × Y) => concaveBracket Bu (adjointBifun Bu Bx F) p.1 p.2

The saddle-value is a value of the conjugate at the origin

theorem Tdaf.ConvexAnalysis.minimax_eq_neg_lowerConjSaddle_zero {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) : minimax K = -lowerConjSaddle Bu Bx K 0

inf sup K = -K̲* (0, 0): the inf sup is a value of the lower conjugate at the origin.

theorem Tdaf.ConvexAnalysis.maximin_eq_neg_upperConjSaddle_zero {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) : maximin K = -upperConjSaddle Bu Bx K 0

sup inf K = -K̄* (0, 0): the sup inf is a value of the upper conjugate at the origin.

theorem Tdaf.ConvexAnalysis.hasSaddleValue_iff_conjSaddle_zero_eq {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) : HasSaddleValue K ↔ upperConjSaddle Bu Bx K 0 = lowerConjSaddle Bu Bx K 0

The saddle-value of K exists exactly when the two conjugates agree at the origin. This is the reduction of minimax theory to the position of the origin relative to the effective domain of the conjugate class.

The structure of the inverse adjoint

theorem Tdaf.ConvexAnalysis.concaveFn_adjointBifun_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) : ConcaveFn (adjointBifun Bu Bx F y)

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

The inverse of the adjoint is a convex bifunction. Rockafellar writes it F_*^*, using the commutation (F_*)^* = (F^*)_*; taking (F^*)_* as the definition makes that commutation a triviality, and this is the bifunction the lower conjugate turns out to be the bracket of.

theorem Tdaf.ConvexAnalysis.closedFn_neg_adjointBifun_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] [TopologicalSpace V] [IsTopologicalAddGroup V] [TopologicalSpace Y] [IsTopologicalAddGroup Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsContinuousPairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsContinuousPairing Bx.flip] (F : Bifun U X) (y : Y) : ClosedFn fun (v : V) => -adjointBifun Bu Bx F y v

Each slice of the negated adjoint is a closed convex function: the adjoint of a bifunction is closed, read slice by slice.

theorem Tdaf.ConvexAnalysis.closedBifun_inverseBifun_adjointBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace V] [IsTopologicalAddGroup V] [TopologicalSpace Y] [IsTopologicalAddGroup Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsContinuousPairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsContinuousPairing Bx.flip] (F : Bifun U X) : ClosedBifun (inverseBifun (adjointBifun Bu Bx F))

The inverse of the adjoint is a closed bifunction.

The two conjugates of a member of Ω (F)

theorem Tdaf.ConvexAnalysis.bifunOfSaddle_antitone {U : Type u_1} {X : Type u_3} {Y : Type u_4} [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) {K L : U × Y → EReal} (h : K ≤ L) : bifunOfSaddle Bx L ≤ bifunOfSaddle Bx K

bifunOfSaddle is antitone: it is a conjugate in disguise.

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

The convex bifunction attached to a saddle-function sees only its cl₂ closure. This is conj_clFn on each slice.

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

Every member of the class Ω (F) has the same associated bifunction, namely F. The two brackets have equal bifunOfSaddle — one is the cl₂ of the other, and bifunOfSaddle sees only cl₂ — so the sandwich collapses. This is the step that gives the upper conjugate.

theorem Tdaf.ConvexAnalysis.concaveConj_slice_eq_adjointBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] [LocallyConvexSpace ℝ V] [TopologicalSpace Y] [IsTopologicalAddGroup Y] {F : Bifun U X} {K : U × Y → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx.flip] (hF : ConvexBifun F) (hK : K ∈ bifunSaddleClass Bu Bx F) (y : Y) : (concaveConj Bu fun (u : U) => K (u, y)) = adjointBifun Bu Bx F y

The concave conjugate of a slice of K is a slice of the adjoint F*, for every K in the class Ω (F): the concave conjugate sees only cl₁, and cl₁ of the lower bracket is the upper bracket. This is the step that gives the lower conjugate.

theorem Tdaf.ConvexAnalysis.upperConjSaddle_eq_saddleLagrangian {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] {F : Bifun U X} {K : U × Y → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hF : ConvexBifun F) (hcl : ClosedBifun F) (hK : K ∈ bifunSaddleClass Bu Bx F) : upperConjSaddle Bu Bx K = saddleLagrangian Bu F

The upper conjugate of any K in the class Ω (F) of a closed convex bifunction F is the Lagrangian of F, K̄* (u*, x) = ⟨u*, F_* x⟩ = ⨅ u, {⟨u, u*⟩ + (Fu)(x)}. In particular it does not depend on the representative.

theorem Tdaf.ConvexAnalysis.lowerConjSaddle_eq_bracket_inverseBifun {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 V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] [LocallyConvexSpace ℝ V] [TopologicalSpace Y] [IsTopologicalAddGroup Y] {F : Bifun U X} {K : U × Y → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx.flip] (hF : ConvexBifun F) (hK : K ∈ bifunSaddleClass Bu Bx F) : lowerConjSaddle Bu Bx K = fun (q : V × X) => bracket Bx.flip (inverseBifun (adjointBifun Bu Bx F)) q.1 q.2

The lower conjugate of any K in the class Ω (F) is the bracket of the inverse adjoint, K̲* (u*, x) = ⟨F_*^* u*, x⟩; like the upper conjugate it depends only on the class.

The conjugates are again concave-convex, and closed

theorem Tdaf.ConvexAnalysis.concaveConvexFn_upperConjSaddle {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] {F : Bifun U X} {K : U × Y → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hF : ConvexBifun F) (hcl : ClosedBifun F) (hK : K ∈ bifunSaddleClass Bu Bx F) : ConcaveConvexFn (upperConjSaddle Bu Bx K)

The upper conjugate of a member of Ω (F) is a concave-convex function.

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

The upper conjugate of a member of Ω (F) is upper closed: it is a Lagrangian, and the Lagrangians are exactly the upper closed concave-convex functions.

theorem Tdaf.ConvexAnalysis.concaveConvexFn_lowerConjSaddle {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 V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] [LocallyConvexSpace ℝ V] [TopologicalSpace Y] [IsTopologicalAddGroup Y] {F : Bifun U X} {K : U × Y → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx.flip] (hF : ConvexBifun F) (hK : K ∈ bifunSaddleClass Bu Bx F) : ConcaveConvexFn (lowerConjSaddle Bu Bx K)

The lower conjugate of a member of Ω (F) is a concave-convex function.

theorem Tdaf.ConvexAnalysis.lowerClosedFn_lowerConjSaddle {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 V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] [LocallyConvexSpace ℝ V] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] {F : Bifun U X} {K : U × Y → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hF : ConvexBifun F) (hK : K ∈ bifunSaddleClass Bu Bx F) : LowerClosedFn (lowerConjSaddle Bu Bx K)

The lower conjugate of a member of Ω (F) is lower closed: it is the bracket of the closed convex bifunction F_*^*.