The transport cost of two measures #

Given a cost c : X × Y → ℝ≥0∞, the transport cost of μ and ν is the infimum of ∫⁻ z, c z ∂π over the couplings π of μ and ν. This is the value of the primal Kantorovich problem, and it is the root definition of optimal transport: every later notion — Wasserstein distance, Kantorovich duality, transport maps — is a statement about this number or about the plans that attain it.

The definition is made for arbitrary measures on arbitrary measurable spaces, with an extended-nonnegative cost integrated by lintegral. Nothing is assumed about topology, finiteness, or normalisation, and no compactness is built in. An empty feasible set — for instance measures of different total mass — gives the value ∞, as does a cost that is too large on every plan; the two are separated by TauCeti.exists_isCoupling_of_transportCost_ne_top.

Main definitions #

TauCeti.transportCost c μ ν — the infimum of ∫⁻ z, c z ∂π over the couplings π of μ and ν;
TauCeti.IsOptimalCoupling c π μ ν — the predicate cutting out the optimal plans: π is a coupling of μ and ν whose cost is transportCost c μ ν.

Main statements #

TauCeti.transportCost_le_lintegral and TauCeti.le_transportCost — the two halves of the universal property of the infimum, with TauCeti.transportCost_lt_iff its order-theoretic restatement;
TauCeti.transportCost_mono, TauCeti.transportCost_congr, TauCeti.transportCost_const, TauCeti.transportCost_const_mul and TauCeti.transportCost_add_split — monotonicity in the cost, invariance under a change of cost that is a.e. invisible to every feasible plan, the value of a constant cost, positive scaling, and the effect of adding integrable terms depending on one variable each;
TauCeti.transportCost_comp_swap, TauCeti.transportCost_comm and TauCeti.transportCost_comp_prodMap — functoriality: exchanging the two factors, symmetry for a symmetric cost, and invariance under measurable equivalences of the two factors;
TauCeti.transportCost_dirac_left, TauCeti.transportCost_dirac_right and TauCeti.transportCost_dirac_dirac — the exact value when either marginal is a Dirac measure, where the plan is unique;
TauCeti.isOptimalCoupling_iff — optimality is minimality among feasible plans, so it does not depend on the value transportCost c μ ν being finite, with the left and right Dirac lemmas giving the first families of optimal plans;
TauCeti.transportCost_le_lintegral_of_hasLaw — the Monge-to-Kantorovich inequality: the transport cost of μ and ν is at most the cost ∫⁻ x, c (x, T x) ∂μ of any transport map T from μ to ν, with TauCeti.isOptimalCoupling_graphPlan_iff its equality case.

Implementation notes #

The infimum is written as an iterated ⨅ over plans and over proofs of TauCeti.IsCoupling, so that it is ∞ on an empty feasible set with no case split, and so that TauCeti.transportCost_le_lintegral is iInf₂_le.

Invariance of the transport cost under a change of the cost function needs the two costs to agree a.e. for every feasible plan, not merely μ.prod ν-a.e.: a coupling can be singular with respect to the product measure — the diagonal plan of μ with itself on a diffuse μ is — so a μ.prod ν-null set can carry all the mass of some competitor. This is why TauCeti.transportCost_congr quantifies over plans.

Measurability of the cost is assumed only where it is used, namely in the theorems that move an integral along a pushforward (TauCeti.transportCost_comp_swap, TauCeti.transportCost_comp_prodMap and the Dirac formulas). The order-theoretic API needs none.

The Monge-to-Kantorovich inequality is a statement about the transport cost, so it is stated here; the graph plan that witnesses it and the change of variables it uses come from TauCeti/MeasureTheory/OptimalTransport/GraphPlan/Basic.lean, which is below this module. Its inequality half needs no measurability of the cost at all, since only one half of the change of variables, MeasureTheory.lintegral_map_le, is used.

This supplies the nonnegative-cost interface from Layer 1, item 1 of the optimal-transport roadmap. The parallel signed EReal interface for costs bounded below by an integrable split function is a separate definition family and is not part of this module.

References #

C. Villani, Topics in Optimal Transportation, Graduate Studies in Mathematics 58, 2003, §1.1.1, where "Kantorovich's mass transportation problem consists in minimizing the linear functional π ↦ ∫ c dπ" over the transference plans. Villani takes μ and ν to be probability measures and c nonnegative measurable; TauCeti.transportCost drops the normalisation and reads c into ℝ≥0∞, so an infeasible pair simply gets the value ∞.