Cyclical monotonicity for transport costs

This file defines finite c-cyclical monotonicity for a transport cost with values in an additive commutative monoid equipped with a comparison relation, which covers both the extended-nonnegative costs of the primal interface and the real costs of the c-transform interface. The definition is purely cost-theoretic: it does not require a measure, topology, or duality theory. A certified plan is almost-everywhere concentrated on a cyclically monotone set, and that set can be taken measurable as soon as the cost and both potentials are measurable.

For a continuous cost, optimality alone already forces cyclical monotonicity, on the topological support of the plan: if finitely many points of the support could be improved by permuting their targets, then by continuity so could all points of small neighbourhoods of them, and moving a little mass from those neighbourhoods to the permuted pairs would lower the total cost. This is the first step from optimality towards Kantorovich potentials, which are then built on the support by the Rüschendorf construction. The converse, and the corresponding statements for discontinuous costs, where concentration on a cyclically monotone set replaces the support, require additional hypotheses.

Main statements

• TauCeti.IsCyclicallyMonotone — finite c-cyclical monotonicity of a set of pairs;
• TauCeti.isCyclicallyMonotone_add_add_iff — adding a split cost a x + b y does not change the cyclically monotone sets;
• TauCeti.isCyclicallyMonotone_ofReal_iff — for a nonnegative real cost, the property is the same for the cost and for its image in ℝ≥0∞;
• TauCeti.IsOptimalCoupling.isCyclicallyMonotone_support — the support of an optimal coupling of finite cost for a continuous cost c : X × Y → ℝ≥0∞ is c-cyclically monotone.

References

• W. Gangbo and R. J. McCann, The geometry of optimal transportation, Acta Math. 177 (1996), 113--161, Theorem 2.3.
• L. Ambrosio and N. Gigli, A user's guide to optimal transport, in Modelling and Optimisation of Flows on Networks, Lecture Notes in Math. 2062, Springer 2013, Theorem 1.13; the perturbation by a product of normalized restrictions follows its proof.
• C. Villani, Optimal Transport: Old and New, Grundlehren 338, Springer 2009, Chapter 5 (cyclical monotonicity, and Theorem 5.10).

def TauCeti.IsCyclicallyMonotone {X : Type u} {Y : Type v} {M : Type w} [AddCommMonoid M] [LE M] (c : X × Y → M) (S : Set (X × Y)) : Prop

A set of pairs is c-cyclically monotone when no finite family of its points can be improved by permuting the targets: for every finite family (x i, y i) in the set and every permutation σ, the diagonal total cost ∑ i, c (x i, y i) is at most the rearranged total cost ∑ i, c (x i, y (σ i)).

This is Villani's finite-family form of the condition. A certified plan is almost-everywhere concentrated on a c-cyclically monotone set — measurably so when the cost and both potentials are measurable; the converse and any statement about topological support need additional hypotheses. Infinite costs allow forbidden rearrangements.

Equations

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

theorem TauCeti.isCyclicallyMonotone_iff {X : Type u} {Y : Type v} {M : Type w} [AddCommMonoid M] [LE M] {c : X × Y → M} {S : Set (X × Y)} : IsCyclicallyMonotone c S ↔ ∀ (n : ℕ) (x : Fin n → X) (y : Fin n → Y), (∀ (i : Fin n), (x i, y i) ∈ S) → ∀ (σ : Equiv.Perm (Fin n)), ∑ i : Fin n, c (x i, y i) ≤ ∑ i : Fin n, c (x i, y (σ i))

The defining finite-family inequality for c-cyclical monotonicity.

theorem TauCeti.IsCyclicallyMonotone.sum_le {X : Type u} {Y : Type v} {M : Type w} [AddCommMonoid M] [LE M] {c : X × Y → M} {S : Set (X × Y)} (h : IsCyclicallyMonotone c S) (n : ℕ) (x : Fin n → X) (y : Fin n → Y) (hmem : ∀ (i : Fin n), (x i, y i) ∈ S) (σ : Equiv.Perm (Fin n)) : ∑ i : Fin n, c (x i, y i) ≤ ∑ i : Fin n, c (x i, y (σ i))

Apply cyclical monotonicity to a finite family and a permutation.

theorem TauCeti.IsCyclicallyMonotone.mono {X : Type u} {Y : Type v} {M : Type w} [AddCommMonoid M] [LE M] {c : X × Y → M} {S S' : Set (X × Y)} (h : IsCyclicallyMonotone c S') (hSS' : S ⊆ S') : IsCyclicallyMonotone c S

Cyclical monotonicity passes to subsets.

theorem TauCeti.IsCyclicallyMonotone.add_le_add_swap {X : Type u} {Y : Type v} {M : Type w} [AddCommMonoid M] [LE M] {c : X × Y → M} {S : Set (X × Y)} (h : IsCyclicallyMonotone c S) {x₁ x₂ : X} {y₁ y₂ : Y} (h₁ : (x₁, y₁) ∈ S) (h₂ : (x₂, y₂) ∈ S) : c (x₁, y₁) + c (x₂, y₂) ≤ c (x₁, y₂) + c (x₂, y₁)

The two-point form of cyclical monotonicity. Swapping the targets of two points of a c-cyclically monotone set does not lower the total cost.

@[simp]

theorem TauCeti.isCyclicallyMonotone_empty {X : Type u} {Y : Type v} {M : Type w} [AddCommMonoid M] [Preorder M] (c : X × Y → M) : IsCyclicallyMonotone c ∅

The empty set is cyclically monotone for every cost.

@[simp]

theorem TauCeti.isCyclicallyMonotone_add_add_iff {X : Type u} {Y : Type v} {M : Type w} [AddCommMonoid M] [LE M] [AddRightMono M] [AddRightReflectLE M] (c : X × Y → M) (a : X → M) (b : Y → M) {S : Set (X × Y)} : IsCyclicallyMonotone (fun (p : X × Y) => c p + a p.1 + b p.2) S ↔ IsCyclicallyMonotone c S

Cyclical monotonicity is insensitive to split costs. Adding a function of the source alone and a function of the target alone to the cost does not change which sets are cyclically monotone: both extra terms contribute the same total to the diagonal and to any rearrangement of the targets.

theorem TauCeti.isCyclicallyMonotone_ofReal_iff {X : Type u} {Y : Type v} {c : X × Y → ℝ} (hc : ∀ (z : X × Y), 0 ≤ c z) {S : Set (X × Y)} : IsCyclicallyMonotone (fun (z : X × Y) => ENNReal.ofReal (c z)) S ↔ IsCyclicallyMonotone c S

For a nonnegative real cost, cyclical monotonicity is the same condition for the cost and for its image in ℝ≥0∞, since ENNReal.ofReal is additive and order-reflecting on nonnegative reals. This moves the property between the extended-nonnegative primal interface and the real c-transform interface.

theorem TauCeti.IsOptimalCoupling.isCyclicallyMonotone_support {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [MeasurableSpace X] [MeasurableSpace Y] [OpensMeasurableSpace (X × Y)] {c : X × Y → ENNReal} {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsFiniteMeasure μ] (h : IsOptimalCoupling c π μ ν) (hc : Continuous c) (hfin : transportCost c μ ν ≠ ⊤) : IsCyclicallyMonotone c π.support

The support of an optimal plan is cyclically monotone (Gangbo--McCann). For a continuous cost c : X × Y → ℝ≥0∞ and finite measures, the topological support of an optimal coupling of finite total cost is c-cyclically monotone.

Finiteness of the optimal cost cannot be dropped: when it is infinite every coupling is optimal. Continuity is used to spread a violation of cyclical monotonicity at finitely many points of the support to sets of positive measure; for discontinuous costs the relevant statement is concentration on some cyclically monotone set rather than a statement about the support. When the support has full measure (MeasureTheory.Measure.measure_compl_support, for instance when X × Y is second countable), the plan is concentrated on this closed set.