The transport cost induced by a pairing

Let E and F be real vector spaces paired by B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ, written ⟪x, y⟫ = B x y. This file defines the transport cost c (x, y) = -⟪x, y⟫ induced by the pairing and identifies its c-cyclically monotone sets with the cyclically monotone sets of convex analysis: those sets Γ ⊆ E × F for which no rearrangement of the targets of finitely many points increases the total pairing, ∑ i, ⟪x i, y (σ i)⟫ ≤ ∑ i, ⟪x i, y i⟫. The c-transform vocabulary of this cost is the Legendre–Fenchel vocabulary of the pairing with the signs reversed; that dictionary is recorded in TauCeti.MeasureTheory.OptimalTransport.CTransform.Pairing.

Main definitions

• TauCeti.pairingCost B — the transport cost (x, y) ↦ -B x y induced by a pairing.

Main statements

• TauCeti.pairingCost_flip — the pairing cost of the transposed pairing is the transposed pairing cost;
• TauCeti.isCyclicallyMonotone_pairingCost_iff — cyclical monotonicity for the pairing cost is the sum inequality ∑ i, B (x i) (y (σ i)) ≤ ∑ i, B (x i) (y i).

References

• R. T. Rockafellar, Characterization of the subdifferentials of convex functions, Pacific J. Math. 17 (1966), 497--510, where cyclically monotone sets are introduced.
• C. Villani, Topics in Optimal Transportation, Graduate Studies in Mathematics 58, 2003, §2.1 and §2.4.

def TauCeti.pairingCost {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (p : E × F) : ℝ

The transport cost (x, y) ↦ -B x y induced by a pairing B. Its c-transform vocabulary is the Legendre–Fenchel vocabulary of the pairing with the signs reversed.

Equations

• TauCeti.pairingCost B p = -(B p.1) p.2

@[simp]

theorem TauCeti.pairingCost_apply {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (p : E × F) : pairingCost B p = -(B p.1) p.2

theorem TauCeti.pairingCost_flip {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) : pairingCost B.flip = fun (p : F × E) => pairingCost B (p.2, p.1)

The pairing cost of the transposed pairing is the transposed pairing cost.

theorem TauCeti.isCyclicallyMonotone_pairingCost_iff {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {Γ : Set (E × F)} : IsCyclicallyMonotone (pairingCost B) Γ ↔ ∀ (n : ℕ) (x : Fin n → E) (y : Fin n → F), (∀ (i : Fin n), (x i, y i) ∈ Γ) → ∀ (σ : Equiv.Perm (Fin n)), ∑ i : Fin n, (B (x i)) (y (σ i)) ≤ ∑ i : Fin n, (B (x i)) (y i)

Cyclical monotonicity for the pairing cost is the classical condition: no rearrangement of the targets of finitely many points of the set increases the total pairing.