Subdifferentials of saddle-functions

A saddle-function is concave in one variable and convex in the other, so it has two one-sided subdifferentials: a superdifferential in the concave variable and a subdifferential in the convex one. Their product is ∂K. Two facts make it useful: (u*, x*) ∈ ∂K (u, x) says exactly that (u, x) is a saddle-point of K tilted by ⟨·, u*⟩ + ⟨·, x*⟩, and for a closed proper K one has ri (dom K) ⊆ dom ∂K ⊆ dom K.

Moreover ∂K depends only on the equivalence class of K: on Ω (F) it is one relation attached to F, and the relations of conjugate classes are inverse. In particular ∂K*(0, 0) is the set of saddle-points of K, so one exists whenever the origin lies in ri (dom K*).

Main definitions

• concaveSubgradient B g x — the superdifferential of a concave g: the y with g z ≤ g x + ⟨z - x, y⟩ for all z. The sign dictionary to subgradient is mem_concaveSubgradient_iff_neg_mem_subgradient_neg.
• saddleSubgradient Bu Bx K p — ∂K (u, x) = ∂₁K (u, x) × ∂₂K (u, x) ⊆ V × Y, the concave variable being paired against V and the convex one against Y; domSaddleSubgradient is where it is nonempty, and saddleTilt Bu Bx K q is K - ⟨·, u*⟩ - ⟨·, x*⟩.
• IsBifunSubgradientPair Bu Bx F p q — the relation (F u) x - ⟨x, y⟩ = (F* y) v - ⟨u, v⟩: the subdifferential of a class, without a representative.

Main results

• mem_concaveSubgradient_iff_concaveConj_eq, concaveSubgradient_nonempty_of_mem_relint_domConcave — the conjugate criterion for a supergradient, and existence of one at a relative interior point.
• mem_saddleSubgradient_iff_isSaddlePoint — subgradients are saddle-points of the tilt, with no hypotheses at all (Theorem 37.4 in [^1]); kernelSet_subset_domSaddleSubgradient_subset_domSaddle — ri (dom K) ⊆ dom ∂K ⊆ dom K.
• mem_saddleSubgradient_iff_isBifunSubgradientPair, mem_saddleSubgradient_upperConjSaddle_iff — ∂K is one relation attached to the class, read from either side (Theorem 37.5 in [^1]).
• mem_saddleSubgradient_upperConjSaddle_zero_iff — ∂K* (0, 0) is the set of saddle-points; exists_isSaddlePoint_of_zero_mem_kernelSet_upperConjSaddle — one exists if 0 ∈ ri (dom K*).

Implementation notes

In Rᵐ × Rⁿ the four spaces coincide; keeping them apart is what makes ∂K* land back in U × Y.

The variant (-v, y) ∈ ∂f (u, x) for the graph function f of F is not equivalent to IsBifunSubgradientPair without properness: where F u x = (F* y) v = ⊤, the latter reads ⊤ - r = ⊤ - s and holds while the former fails. The customary statements do not record the restriction; the form used in Saddle/Monotone.lean assumes Proper (graphFn F).

References

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

Cancelling real coercions across an EReal inequality

theorem Tdaf.ConvexAnalysis.sub_coe_le_sub_coe_iff_le_add {z w : EReal} {c d e : ℝ} (he : c - d = e) : z - ↑c ≤ w - ↑d ↔ z ≤ w + ↑e

Moving a real subtrahend across an EReal inequality: z - c ≤ w - d ↔ z ≤ w + e whenever c - d = e. There is no side condition, because c and d are finite. The difference is passed as a parameter with its defining equation, so that the caller supplies whatever form it has.

theorem Tdaf.ConvexAnalysis.sub_coe_le_sub_coe_iff_add_le {z w : EReal} {c d e : ℝ} (he : d - c = e) : z - ↑c ≤ w - ↑d ↔ z + ↑e ≤ w

The companion of sub_coe_le_sub_coe_iff_le_add with the real moved to the left: z - c ≤ w - d ↔ z + e ≤ w whenever d - c = e.

theorem Tdaf.ConvexAnalysis.sub_coe_lt_top_iff {z : EReal} {c : ℝ} : z - ↑c < ⊤ ↔ z < ⊤

Subtracting a real number does not move the effective domain: z - c < ⊤ ↔ z < ⊤.

theorem Tdaf.ConvexAnalysis.bot_lt_sub_coe_iff {z : EReal} {c : ℝ} : ⊥ < z - ↑c ↔ ⊥ < z

Subtracting a real number does not move the concave effective domain: ⊥ < z - c ↔ ⊥ < z.

theorem Tdaf.ConvexAnalysis.coe_sub_coe_sub_self (r : ℝ) (z : EReal) : ↑r - (↑r - z) = z

Subtracting from a real number is an involution of EReal: r - (r - z) = z.

theorem Tdaf.ConvexAnalysis.eq_coe_sub_iff_coe_sub_eq {z w : EReal} {r : ℝ} : z = ↑r - w ↔ ↑r - z = w

Moving an EReal across a subtraction from a real number: z = r - w ↔ r - z = w. This is what turns the two conjugate criteria into a common value.

theorem Tdaf.ConvexAnalysis.neg_sub_coe (z : EReal) (r : ℝ) : -(z - ↑r) = ↑r - z

Negating a subtraction by a real number: -(z - r) = r - z.

theorem Tdaf.ConvexAnalysis.sub_coe_eq_sub_coe_comm {z w : EReal} {r s : ℝ} : z - ↑r = w - ↑s ↔ ↑r - z = ↑s - w

Reflecting both sides of an equation between differences by real numbers: z - r = w - s ↔ r - z = s - w.

theorem Tdaf.ConvexAnalysis.sub_coe_eq_sub_coe_iff {z w : EReal} {r s : ℝ} : z - ↑r = w - ↑s ↔ z + ↑s = w + ↑r

Equating two differences by real numbers: z - r = w - s ↔ z + s = w + r.

theorem Tdaf.ConvexAnalysis.sub_coe_eq_sub_coe_iff_neg {z w : EReal} {r s : ℝ} : z - ↑r = w - ↑s ↔ -w - ↑r = -z - ↑s

The reflection that exchanges a class with its conjugate class: z - r = w - s ↔ -w - r = -z - s. Both say z + s = w + r; the right-hand side is the left with the two EReals negated and exchanged, which is what conjugating a bifunction does.

Supergradients: the subdifferential of a concave function

def Tdaf.ConvexAnalysis.concaveSubgradient {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (g : E → EReal) (x : E) : Set F

The superdifferential of a concave g at x for the pairing B: the set of y : F with g z ≤ g x + ⟨z - x, y⟩ for every z. This is subgradient with the inequality turned around, and it is what Rockafellar writes ∂ for a concave function.

Equations

• Tdaf.ConvexAnalysis.concaveSubgradient B g x = {y : F | ∀ (z : E), g z ≤ g x + ↑((B (z - x)) y)}

@[simp]

theorem Tdaf.ConvexAnalysis.mem_concaveSubgradient {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : E → EReal} {x : E} {y : F} : y ∈ concaveSubgradient B g x ↔ ∀ (z : E), g z ≤ g x + ↑((B (z - x)) y)

theorem Tdaf.ConvexAnalysis.mem_concaveSubgradient_iff_neg_mem_subgradient_neg {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : E → EReal} {x : E} {y : F} : y ∈ concaveSubgradient B g x ↔ -y ∈ subgradient B (fun (z : E) => -g z) x

The sign dictionary: y is a supergradient of g at x exactly when -y is a subgradient of -g there.

theorem Tdaf.ConvexAnalysis.neg_mem_concaveSubgradient_iff {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : E → EReal} {x : E} {y : F} : -y ∈ concaveSubgradient B g x ↔ y ∈ subgradient B (fun (z : E) => -g z) x

theorem Tdaf.ConvexAnalysis.mem_concaveSubgradient_iff_forall_le_sub {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : E → EReal} {x : E} {y : F} : y ∈ concaveSubgradient B g x ↔ ∀ (z : E), ↑((B x) y) - g x ≤ ↑((B z) y) - g z

y ∈ ∂g x exactly when the infimum of ⟨·, y⟩ - g over the space is attained at x. Unconditional.

theorem Tdaf.ConvexAnalysis.mem_concaveSubgradient_iff_le_concaveConj {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : E → EReal} {x : E} {y : F} : y ∈ concaveSubgradient B g x ↔ ↑((B x) y) - g x ≤ concaveConj B g y

That infimum is the concave conjugate g* y. Unconditional.

theorem Tdaf.ConvexAnalysis.mem_concaveSubgradient_iff_concaveConj_eq {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : E → EReal} {x : E} {y : F} : y ∈ concaveSubgradient B g x ↔ concaveConj B g y = ↑((B x) y) - g x

The same as an equation: y ∈ ∂g x exactly when g* y = ⟨x, y⟩ - g x. Unconditional.

theorem Tdaf.ConvexAnalysis.convex_concaveSubgradient {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : E → EReal} {x : E} : Convex ℝ (concaveSubgradient B g x)

The superdifferential is convex, with no hypothesis on g.

Existence of a supergradient

theorem Tdaf.ConvexAnalysis.concaveSubgradient_nonempty_of_mem_relint_domConcave {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : E → EReal} {x : E} [IsCompatiblePairing B] (hg : ConcaveFn g) (hp : Proper fun (z : E) => -g z) (hx : x ∈ intrinsicInterior ℝ (domConcave g)) : (concaveSubgradient B g x).Nonempty

A proper concave function has a supergradient at every relative interior point of its effective domain.

The subdifferential of a saddle-function

def Tdaf.ConvexAnalysis.saddleSubgradient {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 × X → EReal) (p : U × X) : Set (V × Y)

The subdifferential of a saddle-function: ∂K (u, x) = ∂₁K (u, x) × ∂₂K (u, x), the supergradients of the concave slice through x paired with the subgradients of the convex slice through u.

Equations

• Tdaf.ConvexAnalysis.saddleSubgradient Bu Bx K p = Tdaf.ConvexAnalysis.concaveSubgradient Bu (fun (u : U) => K (u, p.2)) p.1 ×ˢ Tdaf.ConvexAnalysis.subgradient Bx (fun (x : X) => K (p.1, x)) p.2

@[simp]

theorem Tdaf.ConvexAnalysis.mem_saddleSubgradient {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 × X → EReal} {p : U × X} {q : V × Y} : q ∈ saddleSubgradient Bu Bx K p ↔ q.1 ∈ concaveSubgradient Bu (fun (u : U) => K (u, p.2)) p.1 ∧ q.2 ∈ subgradient Bx (fun (x : X) => K (p.1, x)) p.2

theorem Tdaf.ConvexAnalysis.convex_saddleSubgradient {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 × X → EReal} {p : U × X} : Convex ℝ (saddleSubgradient Bu Bx K p)

∂K (u, x) is convex with no hypothesis on K; being a product it is even a convex product set, which is what makes the set of saddle-points a convex product set.

def Tdaf.ConvexAnalysis.domSaddleSubgradient {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 × X → EReal) : Set (U × X)

The set where the subdifferential of a saddle-function is nonempty, dom ∂K.

Equations

• Tdaf.ConvexAnalysis.domSaddleSubgradient Bu Bx K = {p : U × X | (Tdaf.ConvexAnalysis.saddleSubgradient Bu Bx K p).Nonempty}

@[simp]

theorem Tdaf.ConvexAnalysis.mem_domSaddleSubgradient {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 × X → EReal} {p : U × X} : p ∈ domSaddleSubgradient Bu Bx K ↔ (saddleSubgradient Bu Bx K p).Nonempty

Tilting a saddle-function by a linear function

noncomputable def Tdaf.ConvexAnalysis.saddleTilt {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 × X → EReal) (q : V × Y) : U × X → EReal

Rockafellar's K - ⟨·, u*⟩ - ⟨·, x*⟩, the tilt of K by the linear function determined by q = (u*, x*). The two pairings are combined into one real coercion, which is what keeps the EReal arithmetic free of side conditions.

Equations

• Tdaf.ConvexAnalysis.saddleTilt Bu Bx K q p = K p - ↑((Bu p.1) q.1 + (Bx p.2) q.2)

theorem Tdaf.ConvexAnalysis.saddleTilt_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 × X → EReal) (q : V × Y) (p : U × X) : saddleTilt Bu Bx K q p = K p - ↑((Bu p.1) q.1 + (Bx p.2) q.2)

@[simp]

theorem Tdaf.ConvexAnalysis.saddleTilt_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 × X → EReal) : saddleTilt Bu Bx K 0 = K

@[simp]

theorem Tdaf.ConvexAnalysis.dom₁_saddleTilt {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 × X → EReal} {q : V × Y} : dom₁ (saddleTilt Bu Bx K q) = dom₁ K

@[simp]

theorem Tdaf.ConvexAnalysis.dom₂_saddleTilt {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 × X → EReal} {q : V × Y} : dom₂ (saddleTilt Bu Bx K q) = dom₂ K

theorem Tdaf.ConvexAnalysis.ProperSaddleFn.saddleTilt {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 × X → EReal} {q : V × Y} (hp : ProperSaddleFn K) : ProperSaddleFn (ConvexAnalysis.saddleTilt Bu Bx K q)

Subgradients are saddle-points of the tilted function

theorem Tdaf.ConvexAnalysis.mem_saddleSubgradient_iff_isSaddlePoint {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 × X → EReal} {p : U × X} {q : V × Y} : q ∈ saddleSubgradient Bu Bx K p ↔ IsSaddlePoint (saddleTilt Bu Bx K q) p

(u*, x*) ∈ ∂K (u, x) exactly when (u, x) is a saddle-point of K - ⟨·, u*⟩ - ⟨·, x*⟩. There are no hypotheses at all — not concavity, not convexity, not properness: both sides are the same pair of inequalities, one in each variable, with a real number moved across.

The effective domain of the subdifferential

theorem Tdaf.ConvexAnalysis.domSaddleSubgradient_subset_domSaddle {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 × X → EReal} (hp : ProperSaddleFn K) : domSaddleSubgradient Bu Bx K ⊆ domSaddle K

dom ∂K ⊆ dom K for a proper saddle-function; closedness is not needed. A subgradient pair at p makes p a saddle-point of the tilt, and the saddle-points of a proper saddle-function lie in its effective domain.

theorem Tdaf.ConvexAnalysis.kernelSet_subset_domSaddleSubgradient {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [AddCommGroup V] [Module ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [AddCommGroup Y] [Module ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} {K : U × X → EReal} [IsCompatiblePairing Bu] [IsCompatiblePairing Bx] (hK : ConcaveConvexFn K) (hs : SaddleStructure K) : kernelSet K ⊆ domSaddleSubgradient Bu Bx K

ri (dom K) ⊆ dom ∂K. Over ri (dom₁ K) the convex slice K (u, ·) is proper with effective domain exactly dom₂ K, so it has a subgradient there; the concave half is the same statement for saddleSwap K.

theorem Tdaf.ConvexAnalysis.kernelSet_subset_domSaddleSubgradient_subset_domSaddle {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [AddCommGroup V] [Module ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [AddCommGroup Y] [Module ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} {K : U × X → EReal} [IsCompatiblePairing Bu] [IsCompatiblePairing Bx] (hK : ConcaveConvexFn K) (hp : ProperSaddleFn K) (hcl : ClosedSaddleFn K) : kernelSet K ⊆ domSaddleSubgradient Bu Bx K ∧ domSaddleSubgradient Bu Bx K ⊆ domSaddle K

ri (dom K) ⊆ dom ∂K ⊆ dom K for a closed proper saddle-function.

The subdifferential of an equivalence class

def Tdaf.ConvexAnalysis.IsBifunSubgradientPair {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) : Prop

The subgradient relation of a bifunction: the point p = (u, y) and the pair q = (v, x) satisfy

(F u) x - ⟨x, y⟩ = (F* y) v - ⟨u, v⟩.

It is the equality case of the chain ⟨x, y⟩ - (F u) x ≤ ⟨F u, y⟩ ≤ ⟨u, F* y⟩ ≤ ⟨u, v⟩ - (F* y) v, and it turns out to be exactly membership in ∂K for every K in the class Ω (F).

Equations

• Tdaf.ConvexAnalysis.IsBifunSubgradientPair Bu Bx F p q = (F p.1 q.2 - ↑((Bx q.2) p.2) = Tdaf.ConvexAnalysis.adjointBifun Bu Bx F p.2 q.1 - ↑((Bu p.1) q.1))

theorem Tdaf.ConvexAnalysis.isBifunSubgradientPair_iff {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 ↔ ↑((Bx q.2) p.2) - F p.1 q.2 = ↑((Bu p.1) q.1) - adjointBifun Bu Bx F p.2 q.1

The relation read through the reflection z ↦ r - z: both differences are then the common value of the squeezed chain, namely K (u, y).

theorem Tdaf.ConvexAnalysis.isBifunSubgradientPair_def {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 ↔ F p.1 q.2 - ↑((Bx q.2) p.2) = adjointBifun Bu Bx F p.2 q.1 - ↑((Bu p.1) q.1)

theorem Tdaf.ConvexAnalysis.mem_saddleSubgradient_iff_isBifunSubgradientPair {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) (p : U × Y) (q : V × X) : q ∈ saddleSubgradient Bu Bx.flip K p ↔ IsBifunSubgradientPair Bu Bx F p q

For any K in the class Ω (F), the subdifferential ∂K is the relation IsBifunSubgradientPair attached to F. In particular ∂K depends only on the class.

Each half of ∂K (u, y) says that a conjugate of a slice is attained — F u in the convex variable, F* y in the concave one — so each says that a difference equals K (u, y); together they say the two differences are equal. Conversely the relation squeezes the chain ⟨x, y⟩ - (F u) x ≤ ⟨F u, y⟩ ≤ K (u, y) ≤ ⟨u, F* y⟩ ≤ ⟨u, v⟩ - (F* y) v between equal ends.

theorem Tdaf.ConvexAnalysis.mem_saddleSubgradient_upperConjSaddle_iff {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) (p : U × Y) (q : V × X) : p ∈ saddleSubgradient Bu.flip Bx (upperConjSaddle Bu Bx K) q ↔ IsBifunSubgradientPair Bu Bx F p q

The same relation read from the conjugate side, so the subdifferentials of conjugate classes are inverse to each other, exactly as ∂(f*) = (∂f)⁻¹ for convex functions. K̄* lies in the class Ω (F_*^*) at the flipped pairings, and the biadjoint identity turns the resulting condition into the relation reflected by sub_coe_eq_sub_coe_iff_neg.

theorem Tdaf.ConvexAnalysis.mem_saddleSubgradient_upperConjSaddle_zero_iff {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) (p : U × Y) : p ∈ saddleSubgradient Bu.flip Bx (upperConjSaddle Bu Bx K) 0 ↔ IsSaddlePoint K p

∂K* (0, 0) is the set of saddle-points of K. The conjugate-side reading at q = 0 is the direct reading at q = 0, which is the saddle-point property for the untilted K.

theorem Tdaf.ConvexAnalysis.convex_setOf_isSaddlePoint {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) : Convex ℝ {p : U × Y | IsSaddlePoint K p}

The saddle-points of K form a convex product set.

theorem Tdaf.ConvexAnalysis.exists_isSaddlePoint_iff_zero_mem_domSaddleSubgradient {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) : (∃ (p : U × Y), IsSaddlePoint K p) ↔ 0 ∈ domSaddleSubgradient Bu.flip Bx (upperConjSaddle Bu Bx K)

K has a saddle-point exactly when the origin lies in dom ∂K*.

Existence of a saddle-point

theorem Tdaf.ConvexAnalysis.exists_isSaddlePoint_of_zero_mem_kernelSet_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] [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 ∈ kernelSet (upperConjSaddle Bu Bx K)) : ∃ (p : U × Y), IsSaddlePoint K p

If the origin lies in the relative interior of the effective domain C* × D* of the conjugate class, then K has a saddle-point: ri (dom K*) ⊆ dom ∂K* makes ∂K* (0, 0) nonempty, and that set is the set of saddle-points.

theorem Tdaf.ConvexAnalysis.exists_isSaddlePoint_of_zero_mem_interior_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] [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) (h₁ : 0 ∈ interior (dom₁ (upperConjSaddle Bu Bx K))) (h₂ : 0 ∈ interior (dom₂ (upperConjSaddle Bu Bx K))) : ∃ (p : U × Y), IsSaddlePoint K p

The same with the hypothesis in the int form: (0, 0) ∈ int (dom K*) = int C* × int D*.

The Lagrangian in subgradient form

theorem Tdaf.ConvexAnalysis.zero_mem_saddleSubgradient_saddleLagrangian_iff {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)) : 0 ∈ saddleSubgradient Bu.flip Bx (saddleLagrangian Bu F) (v, x) ↔ v ∈ KuhnTucker Bu F ∧ x ∈ argmin (F 0)

(0, 0) ∈ ∂L (v, x) exactly when v is a Kuhn–Tucker vector for (P) and x is an optimal solution to (P). The subgradient condition says "(v, x) is a saddle-point of L", which the Lagrangian characterisation reads off. The pairing Bx is arbitrary data: the subgradient tested there is 0, so no property of it is used.