Cyclically monotone sets are subdifferentials of convex functions

Let E and F be real vector spaces paired by B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ, written ⟪x, y⟫ = B x y. A set Γ ⊆ E × F is cyclically monotone when for all finitely many points (x i, y i) of Γ and every permutation σ,

∑ i, ⟪x i, y (σ i)⟫ ≤ ∑ i, ⟪x i, y i⟫.

Rockafellar's theorem says that these are exactly the subsets of the graph of the subdifferential ∂f of a proper lower-semicontinuous convex function f : E → EReal. This file proves the algebraic form of that statement on a bare dual pair: a set is cyclically monotone exactly when it lies in the subdifferential graph of a Legendre–Fenchel conjugate f = g⋆. Such a conjugate is convex, and it is lower semicontinuous for every topology on E compatible with the pairing. When the set is nonempty, f is moreover proper: it is never ⊥ (TauCeti.apply_ne_bot_of_mem_subdifferential) and it is finite at the first coordinate of every point of the set (TauCeti.mem_subdifferential_iff_add_fenchelConjugate_eq). The converse description of closed proper convex functions as conjugates is the Fenchel–Moreau theorem, which needs a separation theorem and is not part of this file.

Cyclical monotonicity for the pairing is c-cyclical monotonicity for the transport cost c (x, y) = -⟪x, y⟫ (TauCeti.MeasureTheory.OptimalTransport.Cost.Pairing), whose c-transform dictionary in TauCeti.MeasureTheory.OptimalTransport.CTransform.Pairing is the Legendre–Fenchel vocabulary with the signs reversed.

Main statements

• TauCeti.isCyclicallyMonotone_pairingCost_subdifferential — the graph of the subdifferential of any extended-real function is cyclically monotone;
• TauCeti.IsCyclicallyMonotone.exists_fenchelConjugate_subset_subdifferential — Rockafellar's theorem: a cyclically monotone set lies in the graph of the subdifferential of a Legendre–Fenchel conjugate, and TauCeti.isCyclicallyMonotone_pairingCost_iff_exists_fenchelConjugate, the resulting characterisation.

References

• R. T. Rockafellar, Characterization of the subdifferentials of convex functions, Pacific J. Math. 17 (1966), 497--510, Theorem 1.
• R. T. Rockafellar, Convex Analysis, Princeton Mathematical Series 28, 1970, Theorem 24.8.
• C. Villani, Topics in Optimal Transportation, Graduate Studies in Mathematics 58, 2003, Theorem 2.27.

theorem TauCeti.isCyclicallyMonotone_pairingCost_subdifferential {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) : IsCyclicallyMonotone (pairingCost B) {p : E × F | p.2 ∈ subdifferential B f p.1}

The graph of the subdifferential of any extended-real function is cyclically monotone.

theorem TauCeti.IsCyclicallyMonotone.exists_fenchelConjugate_subset_subdifferential {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {Γ : Set (E × F)} (hΓ : IsCyclicallyMonotone (pairingCost B) Γ) : ∃ (g : F → EReal), Γ ⊆ {p : E × F | p.2 ∈ subdifferential B (fenchelConjugate B.flip g) p.1}

Rockafellar's theorem. A cyclically monotone set lies in the graph of the subdifferential of a Legendre–Fenchel conjugate g⋆, hence of a convex function that is lower semicontinuous for every topology compatible with the pairing, and is never ⊥ as soon as the set is nonempty (TauCeti.apply_ne_bot_of_mem_subdifferential).

theorem TauCeti.isCyclicallyMonotone_pairingCost_iff_exists_fenchelConjugate {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (Γ : Set (E × F)) : IsCyclicallyMonotone (pairingCost B) Γ ↔ ∃ (g : F → EReal), Γ ⊆ {p : E × F | p.2 ∈ subdifferential B (fenchelConjugate B.flip g) p.1}

Cyclically monotone sets are exactly the subsets of subdifferential graphs of Legendre–Fenchel conjugates. Every such conjugate is convex and lower semicontinuous for every topology on E compatible with the pairing.