The c-transform for the cost induced by a pairing

Let E and F be real vector spaces paired by B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ, written ⟪x, y⟫ = B x y. The transport cost c (x, y) = -⟪x, y⟫ induced by the pairing (TauCeti.MeasureTheory.OptimalTransport.Cost.Pairing) turns the c-transform vocabulary of optimal transport into the Legendre–Fenchel vocabulary of convex analysis with the signs reversed: the infimal c-transform of a potential φ is -(-φ)⋆, where ⋆ is the Legendre–Fenchel conjugate, a potential is c-concave exactly when -φ is a conjugate, and the c-superdifferential of φ is the graph of the subdifferential of -φ. This file records that dictionary. Costs that differ from the pairing cost by a split term a x + b y, such as the quadratic cost ‖x - y‖ ^ 2 / 2 on an inner product space, reduce to it through the split-shift lemmas of TauCeti.MeasureTheory.OptimalTransport.CTransform.Basic.

Main statements

• TauCeti.cTransform_pairingCost and TauCeti.cTransformSymm_pairingCost — the two c-transforms for the pairing cost are the negated Legendre–Fenchel conjugates of the negated potentials, for the pairing and for its transpose;
• TauCeti.isCConcave_pairingCost_iff and TauCeti.isCConcaveSymm_pairingCost_iff — a potential on the source, respectively on the target, is c-concave for the pairing cost exactly when its negative is a conjugate for the transposed pairing, respectively for the pairing;
• TauCeti.cSuperdifferential_pairingCost — the c-superdifferential for the pairing cost is the graph of the subdifferential of the negated potential.

References

• C. Villani, Topics in Optimal Transportation, Graduate Studies in Mathematics 58, 2003, §2.1 and §2.4, where the translation between the quadratic cost and convex analysis is carried out.

@[simp]

theorem TauCeti.cTransform_pairingCost {E : Type u_1} {F : Type u_2} [AddCommMonoid F] [Module ℝ F] [AddCommMonoid E] [Module ℝ E] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (φ : E → EReal) (y : F) : cTransform (pairingCost B) φ y = -fenchelConjugate B (fun (x : E) => -φ x) y

The infimal c-transform for the pairing cost is the negative of the Legendre–Fenchel conjugate of the negated potential: φᶜ y = -(-φ)⋆ y.

@[simp]

theorem TauCeti.cTransformSymm_pairingCost {E : Type u_1} {F : Type u_2} [AddCommMonoid F] [Module ℝ F] [AddCommMonoid E] [Module ℝ E] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (ψ : F → EReal) (x : E) : cTransformSymm (pairingCost B) ψ x = -fenchelConjugate B.flip (fun (y : F) => -ψ y) x

The symmetric c-transform for the pairing cost is the negative of the Legendre–Fenchel conjugate, for the transposed pairing, of the negated potential.

theorem TauCeti.isCConcave_pairingCost_iff {E : Type u_1} {F : Type u_2} [AddCommMonoid F] [Module ℝ F] [AddCommMonoid E] [Module ℝ E] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (φ : E → EReal) : IsCConcave (pairingCost B) φ ↔ ∃ (g : F → EReal), (fun (x : E) => -φ x) = fenchelConjugate B.flip g

A potential is c-concave for the pairing cost exactly when its negative is a Legendre–Fenchel conjugate for the transposed pairing.

theorem TauCeti.isCConcaveSymm_pairingCost_iff {E : Type u_1} {F : Type u_2} [AddCommMonoid F] [Module ℝ F] [AddCommMonoid E] [Module ℝ E] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (ψ : F → EReal) : IsCConcaveSymm (pairingCost B) ψ ↔ ∃ (g : E → EReal), (fun (y : F) => -ψ y) = fenchelConjugate B g

A potential on the target is c-concave for the pairing cost exactly when its negative is a Legendre–Fenchel conjugate for the pairing.

@[simp]

theorem TauCeti.cSuperdifferential_pairingCost {E : Type u_1} {F : Type u_2} [AddCommMonoid F] [Module ℝ F] [AddCommGroup E] [Module ℝ E] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (φ : E → EReal) : cSuperdifferential (pairingCost B) φ = {p : E × F | p.2 ∈ subdifferential B (fun (x : E) => -φ x) p.1}

The c-superdifferential of a potential for the pairing cost is the graph of the subdifferential of the negated potential.