The quadratic cost and convex analysis

On a real inner product space E, the quadratic transport cost c (x, y) = ‖x - y‖ ^ 2 / 2 differs from the pairing cost -⟪x, y⟫ by the split term ‖x‖ ^ 2 / 2 + ‖y‖ ^ 2 / 2 (TauCeti.MeasureTheory.OptimalTransport.Cost.Quadratic, which also identifies the c-cyclically monotone sets of the quadratic cost with the classically cyclically monotone sets). Split terms are absorbed by the c-transform vocabulary, so the whole c-transform theory of the quadratic cost is the Legendre–Fenchel theory of the inner product: a potential φ is c-concave exactly when u = ‖·‖ ^ 2 / 2 - φ is a Legendre–Fenchel conjugate, its c-transform is ‖y‖ ^ 2 / 2 - u⋆ y, and its c-superdifferential is the graph of the subdifferential ∂u. Rockafellar's theorem then produces, from a c-cyclically monotone set, a conjugate u whose subdifferential graph contains it. This is the algebraic step of Brenier's theorem: applied to the support of a quadratic optimal plan, it yields the convex potential from which the Brenier map is later extracted, once finite dimension, absolute continuity of the source and almost-everywhere differentiability of u enter; none of these analytic and measure-theoretic hypotheses is used here. Every bridge in this file accounts for the factor 1 / 2 in the cost.

Main statements

• TauCeti.cTransform_norm_sub_sq_div_two, TauCeti.cTransformSymm_norm_sub_sq_div_two, TauCeti.isCConcave_norm_sub_sq_div_two_iff, TauCeti.isCConcaveSymm_norm_sub_sq_div_two_iff and TauCeti.cSuperdifferential_norm_sub_sq_div_two — the two c-transforms, c-concavity on the source and on the target, and the c-superdifferential for the quadratic cost in terms of the Legendre–Fenchel conjugate and the subdifferential of ‖·‖ ^ 2 / 2 - φ;
• TauCeti.IsCyclicallyMonotone.exists_fenchelConjugate_innerₗ_subset_subdifferential — Rockafellar's theorem for the quadratic cost: a c-cyclically monotone set lies in the subdifferential graph of a Legendre–Fenchel conjugate for the inner product.

References

• Y. Brenier, Polar factorization and monotone rearrangement of vector-valued functions, Comm. Pure Appl. Math. 44 (1991), 375--417.
• C. Villani, Topics in Optimal Transportation, Graduate Studies in Mathematics 58, 2003, §2.1 and Theorem 2.12, where the quadratic cost is reduced to convex analysis.

@[simp]

theorem TauCeti.cTransform_norm_sub_sq_div_two {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (φ : E → EReal) (y : E) : cTransform (fun (p : E × E) => ‖p.1 - p.2‖ ^ 2 / 2) φ y = ↑(‖y‖ ^ 2 / 2) - fenchelConjugate (innerₗ E) (fun (x : E) => ↑(‖x‖ ^ 2 / 2) - φ x) y

The c-transform of a potential φ for the quadratic cost is ‖y‖ ^ 2 / 2 - u⋆ y, where u = ‖·‖ ^ 2 / 2 - φ and u⋆ is its Legendre–Fenchel conjugate for the inner product.

@[simp]

theorem TauCeti.cTransformSymm_norm_sub_sq_div_two {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (ψ : E → EReal) (x : E) : cTransformSymm (fun (p : E × E) => ‖p.1 - p.2‖ ^ 2 / 2) ψ x = ↑(‖x‖ ^ 2 / 2) - fenchelConjugate (innerₗ E) (fun (y : E) => ↑(‖y‖ ^ 2 / 2) - ψ y) x

The symmetric c-transform of a potential ψ on the target for the quadratic cost is ‖x‖ ^ 2 / 2 - v⋆ x, where v = ‖·‖ ^ 2 / 2 - ψ and v⋆ is its Legendre–Fenchel conjugate for the inner product; the quadratic cost is symmetric, so the formula is the same as for the infimal c-transform.

theorem TauCeti.isCConcave_norm_sub_sq_div_two_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (φ : E → EReal) : IsCConcave (fun (p : E × E) => ‖p.1 - p.2‖ ^ 2 / 2) φ ↔ ∃ (g : E → EReal), (fun (x : E) => ↑(‖x‖ ^ 2 / 2) - φ x) = fenchelConjugate (innerₗ E) g

A potential φ is c-concave for the quadratic cost exactly when ‖·‖ ^ 2 / 2 - φ is a Legendre–Fenchel conjugate for the inner product.

theorem TauCeti.isCConcaveSymm_norm_sub_sq_div_two_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (ψ : E → EReal) : IsCConcaveSymm (fun (p : E × E) => ‖p.1 - p.2‖ ^ 2 / 2) ψ ↔ ∃ (g : E → EReal), (fun (y : E) => ↑(‖y‖ ^ 2 / 2) - ψ y) = fenchelConjugate (innerₗ E) g

A potential ψ on the target is c-concave for the quadratic cost exactly when ‖·‖ ^ 2 / 2 - ψ is a Legendre–Fenchel conjugate for the inner product; the quadratic cost is symmetric, so the criterion is the same as for potentials on the source.

@[simp]

theorem TauCeti.cSuperdifferential_norm_sub_sq_div_two {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (φ : E → EReal) : cSuperdifferential (fun (p : E × E) => ‖p.1 - p.2‖ ^ 2 / 2) φ = {p : E × E | p.2 ∈ subdifferential (innerₗ E) (fun (x : E) => ↑(‖x‖ ^ 2 / 2) - φ x) p.1}

The c-superdifferential of a potential φ for the quadratic cost is the graph of the subdifferential of ‖·‖ ^ 2 / 2 - φ for the inner product.

theorem TauCeti.isCyclicallyMonotone_norm_sub_sq_div_two_subdifferential {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → EReal) : IsCyclicallyMonotone (fun (p : E × E) => ‖p.1 - p.2‖ ^ 2 / 2) {p : E × E | p.2 ∈ subdifferential (innerₗ E) u p.1}

The subdifferential graph of any extended-real function on E is c-cyclically monotone for the quadratic cost.

theorem TauCeti.IsCyclicallyMonotone.exists_fenchelConjugate_innerₗ_subset_subdifferential {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S : Set (E × E)} (hS : IsCyclicallyMonotone (fun (p : E × E) => ‖p.1 - p.2‖ ^ 2 / 2) S) : ∃ (g : E → EReal), S ⊆ {p : E × E | p.2 ∈ subdifferential (innerₗ E) (fenchelConjugate (innerₗ E) g) p.1}

Rockafellar's theorem for the quadratic cost. A c-cyclically monotone set for the cost ‖x - y‖ ^ 2 / 2 lies in the subdifferential graph of a Legendre–Fenchel conjugate u = g⋆ for the inner product: y ∈ ∂u(x) for every (x, y) in the set.

theorem TauCeti.isCyclicallyMonotone_norm_sub_sq_div_two_iff_exists_fenchelConjugate {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Set (E × E)) : IsCyclicallyMonotone (fun (p : E × E) => ‖p.1 - p.2‖ ^ 2 / 2) S ↔ ∃ (g : E → EReal), S ⊆ {p : E × E | p.2 ∈ subdifferential (innerₗ E) (fenchelConjugate (innerₗ E) g) p.1}

c-cyclically monotone sets for the quadratic cost are exactly the subsets of subdifferential graphs of Legendre–Fenchel conjugates for the inner product. Every such conjugate is convex and lower semicontinuous for the norm topology.