Monge's infimum equals Kantorovich's minimum for continuous costs

Let X and Y be second-countable spaces with standard Borel structures, for instance Polish spaces, with Y nonempty, and let c : X × Y → [0, ∞] be continuous, possibly unbounded and possibly infinite. For a finite atomless source measure μ, Pratelli's Theorem B says that the Monge infimum over transport maps equals the Kantorovich infimum over couplings. Neither a moment condition nor an integrable envelope of the cost is needed, and the Monge infimum need not be attained.

Construction

Fix a coupling π of finite cost and ε > 0. Enumerate countable bases tX and tY of the two topologies. The first n basic sets partition each space into finitely many cells, and the products of these cells are the level-n cell rectangles. Call a rectangle good if c oscillates by at most ε on it. By continuity, every point where c is finite lies in a good rectangle at some level. Keep each point in the first good rectangle containing it. The source sides of the kept rectangles form a graded laminar family, so the allocation theorem MeasureTheory.Measure.exists_disjoint_subset_measure_eq_of_laminar gives disjoint source sets Z i with the masses π puts on the pieces. Transporting μ on Z i to the second marginal of the corresponding piece of π produces a map, and inside each good rectangle its cost exceeds that of π by at most ε per unit mass.

Main statements

• TauCeti.IsCoupling.exists_hasLaw_transportMapCost_le — for an atomless finite source, a nonempty target type and a continuous cost, transport maps approach the cost of every coupling;
• TauCeti.mongeCost_eq_transportCost_of_continuous — Pratelli's theorem: the Monge and Kantorovich values agree for continuous costs, atomless finite sources and a nonempty target type.

References

• A. Pratelli, On the equality between Monge's infimum and Kantorovich's minimum in optimal mass transportation, Ann. I. H. Poincaré Probab. Statist. 43 (2007), 1--13, Theorem B and §4.

Cells generated by a sequence of sets

Good cell rectangles and the pieces of the decomposition

Transport maps approaching a coupling

theorem TauCeti.IsCoupling.exists_hasLaw_transportMapCost_le {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [SecondCountableTopology X] [MeasurableSpace X] [OpensMeasurableSpace X] [StandardBorelSpace X] [TopologicalSpace Y] [SecondCountableTopology Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] [StandardBorelSpace Y] [Nonempty Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} {c : X × Y → ENNReal} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.NullSingletonClass μ] (hπ : IsCoupling π μ ν) (hc : Continuous c) {η : ENNReal} (hη : 0 < η) : ∃ (T : X → Y), ProbabilityTheory.HasLaw T ν μ ∧ transportMapCost c μ T ≤ ∫⁻ (z : X × Y), c z ∂π + η

Transport maps approach every coupling. For an atomless finite source measure, a nonempty target type and a continuous cost c : X × Y → [0, ∞] on second-countable standard Borel spaces, the cost of every coupling π is approached from above by the costs of transport maps: for every η > 0 some transport map costs at most ∫⁻ c ∂π + η. No integrability of the cost is assumed.

theorem TauCeti.mongeCost_eq_transportCost_of_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [SecondCountableTopology X] [MeasurableSpace X] [OpensMeasurableSpace X] [StandardBorelSpace X] [TopologicalSpace Y] [SecondCountableTopology Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] [StandardBorelSpace Y] [Nonempty Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {c : X × Y → ENNReal} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.NullSingletonClass μ] (hc : Continuous c) : mongeCost c μ ν = transportCost c μ ν

Pratelli's theorem. For an atomless finite source measure, a nonempty target type and a continuous cost c : X × Y → [0, ∞] on second-countable standard Borel spaces, for instance Polish spaces, the Monge and Kantorovich values agree, whether finite or not. The cost may be unbounded and take the value ∞, and the Monge infimum need not be attained.