The subdifferential of a saddle-function as a monotone mapping

For a closed proper saddle-function K, the graph of ∂K is homeomorphic to the underlying space under (u, v, u*, v*) ↦ (u - u*, v + v*), and the mapping ρ : (u, v) ↦ {(-u*, v*) | (u*, v*) ∈ ∂K (u, v)} is maximal monotone.

Both come from the identification of ∂K with the partial inversion of ∂f, f the graph function of a convex bifunction representing the class of K. Partial inversion exchanges the second component of a relation's argument with that of its value and preserves the monotonicity form, so each is the matching fact about the subdifferential of a closed proper convex function.

Main definitions

• partialInvertEquiv — the involution ((u, y), (v, x)) ↦ ((u, x), (v, y)).
• partialInvertNegHomeomorph — the same with the sign flip, a linear homeomorphism.
• saddleMonotoneRel Bu Bx K — Rockafellar's ρ, as a relation.

Main results

• prodPairing_sub_partialInvertEquiv — partial inversion preserves the monotonicity form, so IsMaximalMonotoneRel.preimage_partialInvertEquiv transfers maximal monotonicity across it.
• saddleSubgradientHomeomorph — the graph of ∂K is homeomorphic to the underlying space (Corollary 37.5.1 in [^1]).
• isMaximalMonotoneRel_saddleMonotoneRel — ρ is maximal monotone (Corollary 37.5.2 in [^1]).
• isMaximalMonotoneRel_setOf_hasSaddleGradientAt — for a finite differentiable K the mapping is (u, v) ↦ (-∇₁K (u, v), ∇₂K (u, v)).

Implementation notes

The transfer lemmas need no symmetry and hold for arbitrary pairings. An inner product enters only where the corresponding facts about ∂f do, and there as a self-pairing rather than an InnerProductSpace instance: U × X carries the supremum norm, but prodPairing (innerₗ U) (innerₗ X) is a continuous inner pairing on it.

Two subdifferentials are in play — subgradientSaddle C D K for a real-valued K on an open rectangle, saddleSubgradient Bu Bx K for an EReal-valued one on the whole space — and they agree at C = D = univ, which is what the differentiable clause below needs.

References

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

Partial inversion

def Tdaf.ConvexAnalysis.partialInvertEquiv {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} : (U × Y) × V × X ≃ (U × X) × V × Y

Partial inversion, Rockafellar's word: the involution exchanging the second component of a relation's argument with that of its value, ((u, y), (v, x)) ↦ ((u, x), (v, y)).

Equations

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

@[simp]

theorem Tdaf.ConvexAnalysis.partialInvertEquiv_apply {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} (r : (U × Y) × V × X) : partialInvertEquiv r = ((r.1.1, r.2.2), r.2.1, r.1.2)

@[simp]

theorem Tdaf.ConvexAnalysis.partialInvertEquiv_symm_apply {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} (s : (U × X) × V × Y) : partialInvertEquiv.symm s = ((s.1.1, s.2.2), s.2.1, s.1.2)

theorem Tdaf.ConvexAnalysis.prodPairing_sub_partialInvertEquiv {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 →ₗ[ℝ] ℝ) (r s : (U × Y) × V × X) : ((prodPairing Bu Bx.flip) (r.1 - s.1)) (r.2 - s.2) = ((prodPairing Bu Bx) ((partialInvertEquiv r).1 - (partialInvertEquiv s).1)) ((partialInvertEquiv r).2 - (partialInvertEquiv s).2)

Partial inversion preserves the monotonicity form. No symmetry is needed: the X-half of the form is Bx.flip (y₁ - y₂) (x₁ - x₂) on the source and Bx (x₁ - x₂) (y₁ - y₂) on the target, which is the same number.

theorem Tdaf.ConvexAnalysis.isMonotoneRel_preimage_partialInvertEquiv {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 →ₗ[ℝ] ℝ} {σ : SetRel (U × X) (V × Y)} : IsMonotoneRel (prodPairing Bu Bx.flip) (⇑partialInvertEquiv ⁻¹' σ) ↔ IsMonotoneRel (prodPairing Bu Bx) σ

theorem Tdaf.ConvexAnalysis.IsMaximalMonotoneRel.preimage_partialInvertEquiv {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 →ₗ[ℝ] ℝ} {σ : SetRel (U × X) (V × Y)} (h : IsMaximalMonotoneRel (prodPairing Bu Bx) σ) : IsMaximalMonotoneRel (prodPairing Bu Bx.flip) (⇑partialInvertEquiv ⁻¹' σ)

Maximal monotonicity transfers across partial inversion. This is the whole content of the maximal monotonicity of ρ, once ρ is identified with a partially inverted ∂f.

Partial inversion with a sign flip, as a homeomorphism

def Tdaf.ConvexAnalysis.partialInvertNegHomeomorph {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [TopologicalSpace U] [TopologicalSpace X] [TopologicalSpace Y] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] : (U × Y) × V × X ≃ₜ (U × X) × V × Y

Partial inversion with a sign flip on the first dual component, ((u, y), (v, x)) ↦ ((u, x), (-v, y)): the map along which ∂K is a preimage of ∂f.

Equations

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

@[simp]

theorem Tdaf.ConvexAnalysis.partialInvertNegHomeomorph_apply {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [TopologicalSpace U] [TopologicalSpace X] [TopologicalSpace Y] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] (r : (U × Y) × V × X) : partialInvertNegHomeomorph r = ((r.1.1, r.2.2), -r.2.1, r.1.2)

Rockafellar's ρ

def Tdaf.ConvexAnalysis.saddleMonotoneRel {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) : SetRel (U × Y) (V × X)

Rockafellar's ρ: the subdifferential of K with the sign of its concave half reversed, ρ (u, y) = {(-v, x) | (v, x) ∈ ∂K (u, y)}. The sign is what makes ρ monotone rather than monotone in one variable and antitone in the other.

Equations

• Tdaf.ConvexAnalysis.saddleMonotoneRel Bu Bx K = {r : (U × Y) × V × X | (-r.2.1, r.2.2) ∈ Tdaf.ConvexAnalysis.saddleSubgradient Bu Bx.flip K r.1}

@[simp]

theorem Tdaf.ConvexAnalysis.mem_saddleMonotoneRel {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} {r : (U × Y) × V × X} : r ∈ saddleMonotoneRel Bu Bx K ↔ (-r.2.1, r.2.2) ∈ saddleSubgradient Bu Bx.flip K r.1

ρ as a preimage of the subdifferential of f

theorem Tdaf.ConvexAnalysis.setOf_mem_saddleSubgradient_eq_preimage_homeomorph {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {F : Bifun U X} {K : U × Y → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hF : ConvexBifun F) (hcl : ClosedBifun F) (hK : K ∈ bifunSaddleClass Bu Bx F) : {r : (U × Y) × V × X | r.2 ∈ saddleSubgradient Bu Bx.flip K r.1} = ⇑partialInvertNegHomeomorph ⁻¹' subgradientRel (prodPairing Bu Bx) (graphFn F)

The graph of ∂K is the preimage of the graph of ∂f along partialInvertNegHomeomorph.

theorem Tdaf.ConvexAnalysis.saddleMonotoneRel_eq_preimage {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {F : Bifun U X} {K : U × Y → EReal} (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] (hF : ConvexBifun F) (hcl : ClosedBifun F) (hK : K ∈ bifunSaddleClass Bu Bx F) : saddleMonotoneRel Bu Bx K = ⇑partialInvertEquiv ⁻¹' subgradientRel (prodPairing Bu Bx) (graphFn F)

ρ is the graph of ∂f, partially inverted. The sign flip is absorbed into ρ, which is why no sign survives on the right.

The inner-product instance

theorem Tdaf.ConvexAnalysis.setOf_mem_saddleSubgradient_innerL_eq_preimage {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [FiniteDimensional ℝ X] {F : Bifun U X} {K : U × X → EReal} (hF : ConvexBifun F) (hcl : ClosedBifun F) (hK : K ∈ bifunSaddleClass (innerₗ U) (innerₗ X) F) : {r : (U × X) × U × X | r.2 ∈ saddleSubgradient (innerₗ U) (innerₗ X) K r.1} = ⇑partialInvertNegHomeomorph ⁻¹' subgradientRel (prodPairing (innerₗ U) (innerₗ X)) (graphFn F)

The same preimage description for a space paired with itself, where Bx.flip is Bx.

noncomputable def Tdaf.ConvexAnalysis.saddleSubgradientHomeomorph {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [FiniteDimensional ℝ X] {F : Bifun U X} {K : U × X → EReal} (hF : ConvexBifun F) (hcl : ClosedBifun F) (hpr : Proper (graphFn F)) (hK : K ∈ bifunSaddleClass (innerₗ U) (innerₗ X) F) : ↑{r : (U × X) × U × X | r.2 ∈ saddleSubgradient (innerₗ U) (innerₗ X) K r.1} ≃ₜ U × X

The graph of ∂K is homeomorphic to U × X under ((u, y), (v, x)) ↦ (u - v, x + y): it is the graph of ∂f partially inverted, and the graph of ∂f maps onto U × X by (z, z*) ↦ z + z*.

Equations

• Tdaf.ConvexAnalysis.saddleSubgradientHomeomorph hF hcl hpr hK = (Tdaf.ConvexAnalysis.partialInvertNegHomeomorph.sets ⋯).trans (Tdaf.ConvexAnalysis.subgradientRelHomeomorph ⋯)

@[simp]

theorem Tdaf.ConvexAnalysis.saddleSubgradientHomeomorph_apply {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [FiniteDimensional ℝ X] {F : Bifun U X} {K : U × X → EReal} (hF : ConvexBifun F) (hcl : ClosedBifun F) (hpr : Proper (graphFn F)) (hK : K ∈ bifunSaddleClass (innerₗ U) (innerₗ X) F) (r : ↑{r : (U × X) × U × X | r.2 ∈ saddleSubgradient (innerₗ U) (innerₗ X) K r.1}) : (saddleSubgradientHomeomorph hF hcl hpr hK) r = ((↑r).1.1 - (↑r).2.1, (↑r).2.2 + (↑r).1.2)

theorem Tdaf.ConvexAnalysis.isMaximalMonotoneRel_saddleMonotoneRel {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [FiniteDimensional ℝ X] {F : Bifun U X} {K : U × X → EReal} (hF : ConvexBifun F) (hcl : ClosedBifun F) (hpr : Proper (graphFn F)) (hK : K ∈ bifunSaddleClass (innerₗ U) (innerₗ X) F) : IsMaximalMonotoneRel (prodPairing (innerₗ U) (innerₗ X)) (saddleMonotoneRel (innerₗ U) (innerₗ X) K)

ρ : (u, v) ↦ {(-u*, v*) | (u*, v*) ∈ ∂K (u, v)} is maximal monotone: it is the partial inversion of ∂f, partial inversion preserves the monotonicity form, and the subdifferential of a closed proper convex function is maximal monotone.

The finite differentiable case

theorem Tdaf.ConvexAnalysis.lowerSimpleExt_univ {U : Type u_1} {X : Type u_2} (K : U × X → ℝ) : lowerSimpleExt Set.univ Set.univ K = fun (p : U × X) => ↑(K p)

A finite saddle-function is its own lower simple extension over the whole space: the bridge between the real-valued K and the EReal-valued one.

theorem Tdaf.ConvexAnalysis.concaveSubgradient_eq_subgradientFst {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (K : U × X → ℝ) (p : U × X) : concaveSubgradient (innerₗ U) (fun (u : U) => ↑(K (u, p.2))) p.1 = subgradientFst Set.univ K p

The concave subdifferential of the EReal reading of a finite saddle-function is ∂₁K.

theorem Tdaf.ConvexAnalysis.subgradient_eq_subgradientSnd {U : Type u_1} {X : Type u_2} [NormedAddCommGroup X] [InnerProductSpace ℝ X] (K : U × X → ℝ) (p : U × X) : subgradient (innerₗ X) (fun (x : X) => ↑(K (p.1, x))) p.2 = subgradientSnd Set.univ K p

The subdifferential of the EReal reading of a finite saddle-function is ∂₂K.

theorem Tdaf.ConvexAnalysis.saddleSubgradient_eq_subgradientSaddle {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup X] [InnerProductSpace ℝ X] (K : U × X → ℝ) (p : U × X) : saddleSubgradient (innerₗ U) (innerₗ X) (fun (q : U × X) => ↑(K q)) p = subgradientSaddle Set.univ Set.univ K p

Over the whole space the EReal-valued and the real-valued ∂K are the same set; the definitions differ only in where their junk values live.

theorem Tdaf.ConvexAnalysis.saddleSubgradient_eq_singleton_of_hasSaddleGradientAt {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup X] [InnerProductSpace ℝ X] {K : U × X → ℝ} (hK : ConcaveConvexOn Set.univ Set.univ K) {q p : U × X} (hd : HasSaddleGradientAt K q p) : saddleSubgradient (innerₗ U) (innerₗ X) (fun (z : U × X) => ↑(K z)) p = {q}

For the EReal-valued subdifferential as well: where a finite concave-convex K has a gradient, ∂K is the single point (∇₁K, ∇₂K).

theorem Tdaf.ConvexAnalysis.saddleMonotoneRel_eq_setOf_hasSaddleGradientAt {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → ℝ} (hK : ConcaveConvexOn Set.univ Set.univ K) (hdiff : ∀ (p : U × X), DifferentiableAt ℝ K p) : (saddleMonotoneRel (innerₗ U) (innerₗ X) fun (z : U × X) => ↑(K z)) = {r : (U × X) × U × X | HasSaddleGradientAt K (-r.2.1, r.2.2) r.1}

Rockafellar's ρ for a differentiable K is the graph of (u, v) ↦ (-∇₁K (u, v), ∇₂K (u, v)).

theorem Tdaf.ConvexAnalysis.isMaximalMonotoneRel_setOf_hasSaddleGradientAt {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [FiniteDimensional ℝ X] {K : U × X → ℝ} (hK : ConcaveConvexOn Set.univ Set.univ K) (hdiff : ∀ (p : U × X), DifferentiableAt ℝ K p) : IsMaximalMonotoneRel (prodPairing (innerₗ U) (innerₗ X)) {r : (U × X) × U × X | HasSaddleGradientAt K (-r.2.1, r.2.2) r.1}

If K is everywhere finite and differentiable, (u, v) ↦ (-∇₁K (u, v), ∇₂K (u, v)) is maximal monotone. Differentiability collapses ∂K to a point, so ρ is the graph of that mapping; the representing bifunction comes from the lower simple extension at C = D = univ.