The two conjugates of a saddle-function form a closure pair

The lower and upper conjugates K̲*, K̄* of a saddle-function in the class Ω (F) of a closed convex bifunction F are the two brackets of one and the same convex bifunction, F_*^*. So they are a closure pair: equivalent, sharing an effective domain C* × D*, and agreeing wherever one coordinate is a relative interior point of it. In particular the origin in ri C* or ri D* forces the saddle-value of K to exist.

The one new algebraic fact needed is the biadjoint identity (F_*^*)^* = F_*. Since F ↦ F_* intertwines the convex and the concave adjoint, it is involutivity of the adjoint read through that intertwining.

The rest of the file computes the effective domains. D* is the projection of dom F on X, and its support function is a supremum of recession functions of the slices K (u, ·); that turns into criteria for 0 ∈ int D* and for the saddle-value to exist. The C* halves are in Saddle/Existence.lean, read at saddleSwap.

Main results

• adjointBifun_flip_inverseBifun, adjointBifun_flip_inverseBifun_adjointBifun — the intertwining (G_*)^* = (G^*)_* and the biadjoint identity (F_*^*)^* = F_*.
• saddleLagrangian_eq_concaveBracket — the Lagrangian is the concave bracket of F_*.
• partialCl₁_lowerConjSaddle, partialCl₂_upperConjSaddle, saddleClass_conjSaddle, domSaddle_conjSaddle_eq, lowerConjSaddle_eq_upperConjSaddle_of_mem_relint_dom₁ — the two conjugates are a closure pair (Corollary 37.1.2 in [^1]); properSaddleFn_saddleLagrangian — conjugates of closed proper saddle-functions are proper.
• hasSaddleValue_of_mem_relint_dom₁_lowerConjSaddle and exists_maximin_eq_coe_of_mem_relint_domSaddle — the origin in the relative interior of C* or of D* gives the saddle-value, and in both gives a finite one.
• dom₁_eq_domBifun_of_mem_bifunSaddleClass — C = dom F for every member of Ω (F).
• supportFn_dom₂_upperConjSaddle, zero_mem_interior_dom₂_upperConjSaddle_iff — the support function of D*, and the criterion for 0 ∈ int D* (Theorem 37.2 in [^1]).
• hasSaddleValue_of_no_common_direction_of_recession, hasSaddleValue_of_isBounded_dom₂ — no common direction of recession, or a bounded D, gives the saddle-value.

Implementation notes

K̲* and K̄* live on V × X and the bifunction behind them goes from V to Y, so every bracket lemma is used at the flipped pairings, whence the .flip compatibility instances throughout. Properness of the conjugate splits unevenly: dom₂ K̄* ≠ ∅ is one line from properness of the graph function, while dom₁ K̄* ≠ ∅ is the existence of an affine minorant of it — which is what makes closedness of F a genuine hypothesis rather than a convenience.

References

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

The inverse intertwines the convex and the concave adjoint

theorem Tdaf.ConvexAnalysis.adjointBifun_flip_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] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (G : Bifun Y V) : adjointBifun Bu.flip Bx.flip (inverseBifun G) = inverseBifun (concaveAdjointBifun Bu Bx G)

The inverse operation intertwines the two adjoints: for a concave bifunction G from Y to V, the convex adjoint of G_* at the flipped pairings is the inverse of the concave adjoint of G. No hypothesis on G is needed — both sides are the same iterated extremum, and the proof is one exchange of bound variables.

theorem Tdaf.ConvexAnalysis.adjointBifun_flip_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 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 Bu.flip Bx.flip (inverseBifun (adjointBifun Bu Bx F)) = inverseBifun F

The biadjoint identity (F_*^*)^* = F_* for a closed convex bifunction. This is Rockafellar's remark that the equivalence class conjugate to Ω (F) is Ω (F_*), and it is what makes the two conjugates a closure pair. It is adjointBifun_flip_inverseBifun followed by involutivity of the adjoint on closed convex bifunctions.

The Lagrangian is the concave bracket of the inverse

theorem Tdaf.ConvexAnalysis.concaveBracket_inverseBifun_eq_lagrangian {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) (x : X) : concaveBracket Bu.flip (inverseBifun F) v x = lagrangian Bu F v x

L (v, x) = ⟨v, F_* x⟩ — the Lagrangian of (P) is the concave bracket of the inverse bifunction F_*, for the flipped pairing. The identity itself is an unfolding.

theorem Tdaf.ConvexAnalysis.saddleLagrangian_eq_concaveBracket {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) : saddleLagrangian Bu F = fun (q : V × X) => concaveBracket Bu.flip (inverseBifun F) q.1 q.2

The saddle-function form of concaveBracket_inverseBifun_eq_lagrangian: the Lagrangian read on V × X is the upper bracket of F_*.

The two conjugates are the two brackets of F_*^*

theorem Tdaf.ConvexAnalysis.upperConjSaddle_eq_concaveBracket_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] [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 = fun (q : V × X) => concaveBracket Bu.flip (adjointBifun Bu.flip Bx.flip (inverseBifun (adjointBifun Bu Bx F))) q.1 q.2

The upper conjugate is the upper bracket of F_*^*, companion of lowerConjSaddle_eq_bracket_inverseBifun. The upper conjugate is the Lagrangian of F, that is the concave bracket of F_*, and the biadjoint identity rewrites F_* as the adjoint of F_*^*.

theorem Tdaf.ConvexAnalysis.partialCl₁_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) (hcl : ClosedBifun F) (hK : K ∈ bifunSaddleClass Bu Bx F) : partialCl₁ (lowerConjSaddle Bu Bx K) = upperConjSaddle Bu Bx K

cl₁ K̲* = K̄*. Both conjugates are brackets of the single closed convex bifunction F_*^*, so this is the first bracket-closure equation, at the flipped pairings.

theorem Tdaf.ConvexAnalysis.partialCl₂_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) : partialCl₂ (upperConjSaddle Bu Bx K) = lowerConjSaddle Bu Bx K

cl₂ K̄* = K̲*, the second bracket-closure equation; it is where closedness of F_*^* is used.

theorem Tdaf.ConvexAnalysis.saddleClass_conjSaddle {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) : bifunSaddleClass Bu.flip Bx.flip (inverseBifun (adjointBifun Bu Bx F)) = saddleClass (lowerConjSaddle Bu Bx K) (upperConjSaddle Bu Bx K)

The class conjugate to Ω (F) is Ω (F_*^*), its two ends being the lower and the upper conjugate of any member of Ω (F).

theorem Tdaf.ConvexAnalysis.saddleEquiv_lowerConjSaddle_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) : SaddleEquiv (lowerConjSaddle Bu Bx K) (upperConjSaddle Bu Bx K)

The two conjugates are equivalent saddle-functions, hence have the same iterated extrema and the same saddle-points.

Properness of the conjugate saddle-functions

theorem Tdaf.ConvexAnalysis.properSaddleFn_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] {F : Bifun U X} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] (hF : ConvexBifun F) (hcl : ClosedBifun F) (hpr : Proper (graphFn F)) : ProperSaddleFn (saddleLagrangian Bu F)

A saddle-function conjugate to a closed proper one is again proper.

The two halves are quite different. dom₂ L ≠ ∅ needs only a point where the graph function is finite. dom₁ L ≠ ∅ is the existence of an affine minorant of the graph function (proper_conj), which is where closedness enters.

A closure pair agrees on the relative interiors

theorem Tdaf.ConvexAnalysis.eq_of_mem_relint_dom₁_of_closure_pair {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {Klow Kup : U × X → EReal} (hup : ConcaveConvexFn Kup) (hne : (dom₂ Kup).Nonempty) (h1 : partialCl₁ Klow = Kup) (h2 : partialCl₂ Kup = Klow) {u : U} (hu : u ∈ intrinsicInterior ℝ (dom₁ Klow)) (x : X) : Klow (u, x) = Kup (u, x)

A closure pair agrees over ri (dom₁ K̲): if cl₁ K̲ = K̄ and cl₂ K̄ = K̲ then the two coincide there. Because the closure relations hold on the nose the hypotheses are lighter than in the version for a closed saddle-function: K̲ (·, x) is cl₂ K̄ (·, x), whose concave effective domain is dom₁ K̄, and a concave function meets its closure on the relative interior of that domain. Only dom₂ K̄ ≠ ∅ is needed.

theorem Tdaf.ConvexAnalysis.eq_of_mem_relint_dom₂_of_closure_pair {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {Klow Kup : U × X → EReal} (hlow : ConcaveConvexFn Klow) (hne : (dom₁ Klow).Nonempty) (h1 : partialCl₁ Klow = Kup) (h2 : partialCl₂ Kup = Klow) {x : X} (hx : x ∈ intrinsicInterior ℝ (dom₂ Kup)) (u : U) : Klow (u, x) = Kup (u, x)

The mirror of eq_of_mem_relint_dom₁_of_closure_pair: a closure pair agrees over ri (dom₂ K̄). Not the same statement read at saddleSwap, because the two use different halves of properness — this one needs dom₁ K̲ ≠ ∅ — so it is proved directly.

The common effective domain, and existence of the saddle-value

theorem Tdaf.ConvexAnalysis.properSaddleFn_upperConjSaddle {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] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hF : ConvexBifun F) (hcl : ClosedBifun F) (hpr : Proper (graphFn F)) (hK : K ∈ bifunSaddleClass Bu Bx F) : ProperSaddleFn (upperConjSaddle Bu Bx K)

The upper conjugate of a member of Ω (F) is proper when F is a closed proper convex bifunction.

theorem Tdaf.ConvexAnalysis.properSaddleFn_lowerConjSaddle {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] [FiniteDimensional ℝ 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) (hpr : Proper (graphFn F)) (hK : K ∈ bifunSaddleClass Bu Bx F) : ProperSaddleFn (lowerConjSaddle Bu Bx K)

The lower conjugate is proper as well — it is cl₂ of the upper one, and cl₂ preserves properness.

theorem Tdaf.ConvexAnalysis.dom₁_conjSaddle_eq {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] [FiniteDimensional ℝ 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) (hpr : Proper (graphFn F)) (hK : K ∈ bifunSaddleClass Bu Bx F) : dom₁ (lowerConjSaddle Bu Bx K) = dom₁ (upperConjSaddle Bu Bx K)

C*, the first half of the common effective domain, does not depend on which of the two conjugates it is read from.

theorem Tdaf.ConvexAnalysis.dom₂_conjSaddle_eq {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ 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) (hpr : Proper (graphFn F)) (hK : K ∈ bifunSaddleClass Bu Bx F) : dom₂ (lowerConjSaddle Bu Bx K) = dom₂ (upperConjSaddle Bu Bx K)

The same for D*.

theorem Tdaf.ConvexAnalysis.domSaddle_conjSaddle_eq {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ 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) (hpr : Proper (graphFn F)) (hK : K ∈ bifunSaddleClass Bu Bx F) : domSaddle (lowerConjSaddle Bu Bx K) = domSaddle (upperConjSaddle Bu Bx K)

C* × D* is the effective domain of both conjugates.

theorem Tdaf.ConvexAnalysis.lowerConjSaddle_eq_upperConjSaddle_of_mem_relint_dom₁ {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ 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) (hpr : Proper (graphFn F)) (hK : K ∈ bifunSaddleClass Bu Bx F) {v : V} (hv : v ∈ intrinsicInterior ℝ (dom₁ (lowerConjSaddle Bu Bx K))) (x : X) : lowerConjSaddle Bu Bx K (v, x) = upperConjSaddle Bu Bx K (v, x)

The two conjugates agree wherever the first coordinate is a relative interior point of C*.

theorem Tdaf.ConvexAnalysis.lowerConjSaddle_eq_upperConjSaddle_of_mem_relint_dom₂ {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ 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) (hpr : Proper (graphFn F)) (hK : K ∈ bifunSaddleClass Bu Bx F) {x : X} (hx : x ∈ intrinsicInterior ℝ (dom₂ (lowerConjSaddle Bu Bx K))) (v : V) : lowerConjSaddle Bu Bx K (v, x) = upperConjSaddle Bu Bx K (v, x)

And wherever the second coordinate is a relative interior point of D*.

theorem Tdaf.ConvexAnalysis.hasSaddleValue_of_mem_relint_dom₁_lowerConjSaddle {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ 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) (hpr : Proper (graphFn F)) (hK : K ∈ bifunSaddleClass Bu Bx F) (h0 : 0 ∈ intrinsicInterior ℝ (dom₁ (lowerConjSaddle Bu Bx K))) : HasSaddleValue K

If the origin of the dual of the concave variable lies in ri C*, the saddle-value of K exists. The two iterated extrema of K are the two conjugates at the origin, and the closure pair makes them agree there.

theorem Tdaf.ConvexAnalysis.hasSaddleValue_of_mem_relint_dom₂_lowerConjSaddle {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ 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) (hpr : Proper (graphFn F)) (hK : K ∈ bifunSaddleClass Bu Bx F) (h0 : 0 ∈ intrinsicInterior ℝ (dom₂ (lowerConjSaddle Bu Bx K))) : HasSaddleValue K

The mirror half: the origin in ri D* suffices as well.

theorem Tdaf.ConvexAnalysis.exists_maximin_eq_coe_of_mem_relint_domSaddle {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ 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) (hpr : Proper (graphFn F)) (hK : K ∈ bifunSaddleClass Bu Bx F) (h1 : 0 ∈ intrinsicInterior ℝ (dom₁ (lowerConjSaddle Bu Bx K))) (h2 : 0 ∈ intrinsicInterior ℝ (dom₂ (lowerConjSaddle Bu Bx K))) : ∃ (r : ℝ), maximin K = ↑r

If the origin lies in the relative interior of both halves of C* × D*, the saddle-value is finite — it is a value of the conjugate on its own effective domain, where a saddle-function is finite by definition.

The effective domains of the conjugate saddle-functions

The support functions of C* = dom₁ K* and D* = dom₂ K*, for K ∈ Ω (F), can be computed in terms of K itself. The D* half is the one with content: D* is the projection on X of dom F, and the support function of that projection is assembled from the support functions of the individual slices dom (F u), each of which is a recession function. The lemmas before it are bookkeeping: support functions do not see relative interiors, and the relative interior of a projection is the union of those of the slices.

theorem Tdaf.ConvexAnalysis.dom₂_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) : dom₂ (saddleLagrangian Bu F) = Prod.snd '' dom (graphFn F)

The set D*: the second effective domain of the Lagrangian L (v, x) = inf_u {⟨u, v⟩ + F (u, x)} is the projection of dom F on X, with no hypotheses on F whatsoever. L (v, x) ≤ ⟨u, v⟩ + F (u, x) gives ⊇; for ⊆ it is enough to test v = 0.

theorem Tdaf.ConvexAnalysis.domBifun_eq_image_fst {U : Type u_1} {X : Type u_2} (F : Bifun U X) : domBifun F = Prod.fst '' dom (graphFn F)

dom F ⊆ U is the projection on U of the effective domain of the graph function: both say that some value F (u, x) is < ⊤.

theorem Tdaf.ConvexAnalysis.dom₁_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) : (dom₁ fun (p : U × Y) => bracket Bx F p.1 p.2) = domBifun F

The first effective domain of the lower bracket ⟨Fu, y⟩ is dom F: the bracket is -∞ exactly where the slice F u is identically +∞, uniformly in y (domConcave_bracket).

theorem Tdaf.ConvexAnalysis.supportFn_relint {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [IsContinuousPairing B] {C : Set E} (hC : Convex ℝ C) : supportFn B (intrinsicInterior ℝ C) = supportFn B C

The support function does not see the relative interior: δ*(· | ri C) = δ*(· | C) for convex C, since it does not see closures and cl (ri C) = cl C.

theorem Tdaf.ConvexAnalysis.relint_image_snd_eq_iUnion {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {S : Set (U × X)} (hS : Convex ℝ S) : intrinsicInterior ℝ (Prod.snd '' S) = ⋃ u ∈ intrinsicInterior ℝ (Prod.fst '' S), intrinsicInterior ℝ {x : X | (u, x) ∈ S}

The relative interior of a projection: for a convex S ⊆ U × X that of the projection on X is the union, over u in the relative interior of the projection on U, of the relative interiors of the slices of S.

theorem Tdaf.ConvexAnalysis.supportFn_biUnion {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {ι : Type u_3} (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (s : Set ι) (t : ι → Set E) (y : F) : supportFn B (⋃ i ∈ s, t i) y = ⨆ i ∈ s, supportFn B (t i) y

theorem Tdaf.ConvexAnalysis.dom₁_eq_domBifun_of_mem_bifunSaddleClass {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] [FiniteDimensional ℝ 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) (hKcc : ConcaveConvexFn K) (hne : (dom₂ K).Nonempty) : dom₁ K = domBifun F

The first effective domain of any K ∈ Ω (F) is dom F, an identification the book makes silently. cl₂ does not move dom₁, and on Ω (F) it is constant at the lower bracket, whose dom₁ is dom F because ⟨Fu, y⟩ = -∞ exactly where F u ≡ +∞.

theorem Tdaf.ConvexAnalysis.recessionFn_slice_eq_supportFn_dom {U : Type u_1} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {K : U × Y → EReal} (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx.flip] (hK : ConcaveConvexFn K) (hs : ConvexSliceStructure K) {u : U} (hu : u ∈ intrinsicInterior ℝ (dom₁ K)) : (recessionFn fun (y : Y) => K (u, y)) = supportFn Bx (dom (bifunOfSaddle Bx K u))

The support function of dom (F u) is the recession function of K (u, ·), for u in ri (dom₁ K) and F = bifunOfSaddle Bx K. Over ri (dom₁ K) the slice is closed proper convex and F u is its conjugate, and the support function of the domain of a conjugate is the recession function of the original.

theorem Tdaf.ConvexAnalysis.supportFn_dom_bifunOfSaddle_eq_iSup_sub {U : Type u_1} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {K : U × Y → EReal} (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx.flip] (hK : ConcaveConvexFn K) (hs : ConvexSliceStructure K) {u : U} (hu : u ∈ intrinsicInterior ℝ (dom₁ K)) (w : Y) : supportFn Bx (dom (bifunOfSaddle Bx K u)) w = ⨆ y ∈ dom₂ K, K (u, y + w) - K (u, y)

The inner half: for u in ri (dom₁ K) the support function of the slice dom (F u) — where F = bifunOfSaddle Bx K — is the difference-quotient supremum sup_{y ∈ D} {K (u, y + w) - K (u, y)}. The support function of dom (K (u, ·)*) is the recession function of K (u, ·), which is in turn the supremum of the difference quotients over the effective domain.

theorem Tdaf.ConvexAnalysis.dom₂_upperConjSaddle {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] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hF : ConvexBifun F) (hcl : ClosedBifun F) (hK : K ∈ bifunSaddleClass Bu Bx F) : dom₂ (upperConjSaddle Bu Bx K) = Prod.snd '' dom (graphFn F)

The second effective domain of the upper conjugate is the projection of dom F on X: the upper conjugate is the Lagrangian of F, and dom₂_saddleLagrangian applies.

theorem Tdaf.ConvexAnalysis.supportFn_dom₂_upperConjSaddle {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] [FiniteDimensional ℝ 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) (hKcc : ConcaveConvexFn K) (hne : (dom₂ K).Nonempty) (hs : ConvexSliceStructure K) (w : Y) : supportFn Bx (dom₂ (upperConjSaddle Bu Bx K)) w = ⨆ u ∈ intrinsicInterior ℝ (dom₁ K), ⨆ y ∈ dom₂ K, K (u, y + w) - K (u, y)

The support function of D*: that of the second effective domain of the conjugate saddle-function is

δ*(w | D*) = sup_{u ∈ ri C} sup_{y ∈ D} {K (u, y + w) - K (u, y)},

where C = dom₁ K and D = dom₂ K. D* is the projection of dom F on X; a support function does not see the relative interior, so it is the supremum over u ∈ ri C of the support functions of the slices dom (F u).

theorem Tdaf.ConvexAnalysis.supportFn_dom₂_upperConjSaddle_eq_iSup_recessionFn {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] [FiniteDimensional ℝ 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) (hKcc : ConcaveConvexFn K) (hne : (dom₂ K).Nonempty) (hs : ConvexSliceStructure K) (w : Y) : supportFn Bx (dom₂ (upperConjSaddle Bu Bx K)) w = ⨆ u ∈ intrinsicInterior ℝ (dom₁ K), recessionFn (fun (y : Y) => K (u, y)) w

The same in recession-function form: the support function of D* is the pointwise supremum, over u ∈ ri C, of the recession functions of the slices K (u, ·).

theorem Tdaf.ConvexAnalysis.zero_mem_interior_dom₂_upperConjSaddle_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] [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] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hB : Bx.SeparatingRight) (hF : ConvexBifun F) (hcl : ClosedBifun F) (hpr : Proper (graphFn F)) (hK : K ∈ bifunSaddleClass Bu Bx F) (hKcc : ConcaveConvexFn K) (hne : (dom₂ K).Nonempty) (hs : ConvexSliceStructure K) : 0 ∈ interior (dom₂ (upperConjSaddle Bu Bx K)) ↔ ∀ (w : Y), w ≠ 0 → ∃ u ∈ intrinsicInterior ℝ (dom₁ K), 0 < recessionFn (fun (y : Y) => K (u, y)) w

The origin is an interior point of D* if and only if the convex functions K (u, ·), for u ∈ ri C, have no common direction of recession.

0 ∈ int D* iff δ*(w | D*) > 0 for every w ≠ 0, and the computation above evaluates δ*(w | D*) as the supremum of the (K (u, ·))∞ (w). Bx.SeparatingRight is what makes w ≠ 0 and ⟨·, w⟩ ≠ 0 the same condition; where a space is paired with itself it is automatic.

Existence of the saddle-value

theorem Tdaf.ConvexAnalysis.hasSaddleValue_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] (hB : Bx.SeparatingRight) (hF : ConvexBifun F) (hcl : ClosedBifun F) (hpr : Proper (graphFn F)) (hK : K ∈ bifunSaddleClass Bu Bx F) (hKcc : ConcaveConvexFn K) (hne : (dom₂ K).Nonempty) (hs : ConvexSliceStructure K) (hrec : ∀ (w : Y), w ≠ 0 → ∃ u ∈ intrinsicInterior ℝ (dom₁ K), 0 < recessionFn (fun (y : Y) => K (u, y)) w) : HasSaddleValue K

If the convex functions K (u, ·) for u ∈ ri C have no common direction of recession, then the saddle-value of K exists. The hypothesis turns into 0 ∈ int D*, hence 0 ∈ ri D*, and the origin in ri D* gives the saddle-value.

theorem Tdaf.ConvexAnalysis.lt_recessionFn_of_isBounded_dom {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} (hne : (dom f).Nonempty) (hb : Bornology.IsBounded (dom f)) {w : E} (hw : w ≠ 0) : 0 < recessionFn f w

A function with a nonempty bounded effective domain has no nonzero direction of recession: f0⁺ (w) > 0 for every w ≠ 0. If f0⁺ (w) ≤ 0 then f is nonincreasing along w, so the whole ray stays in dom f, and a ray in a direction w ≠ 0 leaves every ball.

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 : Bx.SeparatingRight) (hF : ConvexBifun F) (hcl : ClosedBifun F) (hpr : Proper (graphFn F)) (hK : K ∈ bifunSaddleClass Bu Bx F) (hKcc : ConcaveConvexFn K) (hne : (dom₂ K).Nonempty) (hne₁ : (dom₁ K).Nonempty) (hs : ConvexSliceStructure K) (hbd : Bornology.IsBounded (dom₂ K)) : HasSaddleValue K

If the second effective domain of K is bounded, the saddle-value of K exists. Over a compact D this is the classical minimax theorem.

For u ∈ ri C the slice K (u, ·) has effective domain exactly D, which is bounded, so it has no nonzero direction of recession and the previous criterion applies.