Existence of an optimal transport plan

The primal Kantorovich problem minimises π ↦ ∫⁻ z, c z ∂π over the couplings of two fixed probability measures. This file proves that the minimum is attained for a lower semicontinuous cost: the infimum defining TauCeti.transportCost is a minimum, realised by a plan satisfying TauCeti.IsOptimalCoupling.

The proof is the direct method of the calculus of variations, with both of its ingredients already isolated. The feasible set is weakly compact and nonempty (TauCeti.isCompact_setOfPred_isCoupling, the product plan), and the objective is weakly lower semicontinuous (TauCeti.lowerSemicontinuous_lintegral_probabilityMeasure); a lower semicontinuous function on a nonempty compact set attains its infimum.

Nothing here needs the minimum to be finite. If every plan has infinite cost — which happens, for instance, when c is ∞ off the diagonal and the two marginals are mutually singular — the theorem still produces an optimal plan, of cost ∞; existence and finiteness are separate questions.

The cost is only assumed lower semicontinuous, not continuous, and this is the point: the costs of interest, such as edist raised to a power or the {0, ∞}-valued indicator of a closed constraint set, are lower semicontinuous, and lower semicontinuity is exactly what guarantees attainment of the infimum on the compact set of couplings.

Main statements

• TauCeti.exists_isOptimalCoupling_of_isTightMeasureSet — an optimal plan exists whenever both marginals are tight;
• TauCeti.exists_isOptimalCoupling — its Polish specialisation, where tightness is automatic;
• TauCeti.exists_coupling_isOptimalCoupling — the same statement with the plan delivered as an element of the bundled type TauCeti.Coupling;
• TauCeti.isCompact_setOfPred_isOptimalCoupling — the optimal plans themselves form a weakly compact set;
• TauCeti.transportCost_iSup_eq_iSup — minimization over a compact coupling set supplied by tight marginals commutes with an increasing supremum of lower-semicontinuous costs;
• TauCeti.transportCost_eq_iSup_transportCost_lscApprox — transport cost commutes with the canonical monotone approximation of a lower-semicontinuous cost;
• TauCeti.exists_isOptimalCoupling_edist and TauCeti.exists_isOptimalCoupling_edist_rpow — the acceptance instances: the Kantorovich–Rubinstein cost edist, and the p-Wasserstein cost edist ^ p, admit optimal plans on a Polish space.

References

• C. Villani, Optimal Transport: Old and New, Springer 2009, Theorem 4.1 — existence of an optimal coupling for a lower semicontinuous cost on Polish spaces.
• C. Villani, Topics in Optimal Transportation, AMS 2003, Theorem 1.3.
• F. Santambrogio, Optimal Transport for Applied Mathematicians, Springer 2015, Chapter 1 — the direct method for the Kantorovich problem.

The two factors are Borel metrizable spaces, one of the two second countable — the hypotheses under which the product is a Borel space and the coupling set is weakly compact. Metrizability is asked of the topology, not of a chosen distance, so a space known only to be Polish qualifies; the pseudometric that the direct method runs on is installed inside the proofs.

theorem TauCeti.exists_isOptimalCoupling_of_isTightMeasureSet {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace.MetrizableSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [TopologicalSpace.MetrizableSpace Y] [MeasurableSpace Y] [BorelSpace Y] [SecondCountableTopologyEither X Y] {c : X × Y → ENNReal} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {ν : MeasureTheory.Measure Y} [MeasureTheory.IsProbabilityMeasure ν] (hμ : MeasureTheory.IsTightMeasureSet {μ}) (hν : MeasureTheory.IsTightMeasureSet {ν}) (hc : LowerSemicontinuous c) : ∃ (π : MeasureTheory.Measure (X × Y)), IsOptimalCoupling c π μ ν

Primal attainment for a lower semicontinuous cost. If both marginals are tight, the transport cost of μ and ν is attained: some coupling π satisfies ∫⁻ z, c z ∂π = transportCost c μ ν. No finiteness is assumed or concluded — the optimal value may be ∞.

theorem TauCeti.isCompact_setOfPred_isOptimalCoupling {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace.MetrizableSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [TopologicalSpace.MetrizableSpace Y] [MeasurableSpace Y] [BorelSpace Y] [SecondCountableTopologyEither X Y] {c : X × Y → ENNReal} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {ν : MeasureTheory.Measure Y} [MeasureTheory.IsProbabilityMeasure ν] (hμ : MeasureTheory.IsTightMeasureSet {μ}) (hν : MeasureTheory.IsTightMeasureSet {ν}) (hc : LowerSemicontinuous c) : IsCompact {π : MeasureTheory.ProbabilityMeasure (X × Y) | IsOptimalCoupling c (↑π) μ ν}

The optimal plans form a compact set. An optimal plan is a coupling whose cost is at most the transport cost, the reverse inequality being automatic; so the optimal set is the intersection of the compact set of couplings with a weakly closed sublevel set of the cost functional. Together with TauCeti.exists_isOptimalCoupling_of_isTightMeasureSet, which makes it nonempty, this is the compactness a selection argument runs on.

theorem TauCeti.transportCost_iSup_eq_iSup {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace.MetrizableSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [TopologicalSpace.MetrizableSpace Y] [MeasurableSpace Y] [BorelSpace Y] [SecondCountableTopologyEither X Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {cs : ℕ → X × Y → ENNReal} (hμ : MeasureTheory.IsTightMeasureSet {μ}) (hν : MeasureTheory.IsTightMeasureSet {ν}) (hcs : ∀ (n : ℕ), LowerSemicontinuous (cs n)) (hmono : Monotone cs) : transportCost (fun (z : X × Y) => ⨆ (n : ℕ), cs n z) μ ν = ⨆ (n : ℕ), transportCost (cs n) μ ν

Monotone convergence of optimal transport costs for tight marginals. The transport cost of the pointwise supremum of an increasing sequence of lower-semicontinuous costs is the supremum of their transport costs. No finiteness assumption is made: both sides may be ∞.

Tightness is load-bearing because it makes the fixed-marginal coupling set compact. Without compactness, an escaping sequence of approximate minimizers can make the supremum of the minima strictly smaller than the minimum of the supremum.

theorem TauCeti.transportCost_eq_iSup_transportCost_lscApprox {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [T0Space X] [MeasurableSpace X] [BorelSpace X] [PseudoMetricSpace Y] [T0Space Y] [MeasurableSpace Y] [BorelSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [SecondCountableTopologyEither X Y] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {c : X × Y → ENNReal} (hμ : MeasureTheory.IsTightMeasureSet {μ}) (hν : MeasureTheory.IsTightMeasureSet {ν}) (hc : LowerSemicontinuous c) : transportCost c μ ν = ⨆ (n : ℕ), transportCost (fun (z : X × Y) => ↑((lscApprox c n) z)) μ ν

For tight marginals on metrizable spaces, the transport costs of the canonical bounded-continuous approximations of a lower-semicontinuous cost increase to the transport cost of the original cost. This is the minimization counterpart of TauCeti.lintegral_eq_iSup_lintegral_lscApprox.

The Polish specialisation is stated for Mathlib's PolishSpace, the topological notion: second countable and completely metrizable, with no distance chosen.

theorem TauCeti.exists_isOptimalCoupling {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y] {c : X × Y → ENNReal} (μ : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.Measure Y) [MeasureTheory.IsProbabilityMeasure ν] (hc : LowerSemicontinuous c) : ∃ (π : MeasureTheory.Measure (X × Y)), IsOptimalCoupling c π μ ν

Primal attainment on Polish spaces. Every finite Borel measure on a Polish space is tight, so a lower semicontinuous cost always admits an optimal transport plan between two probability measures there.

theorem TauCeti.exists_coupling_isOptimalCoupling {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y] {c : X × Y → ENNReal} (μ : MeasureTheory.ProbabilityMeasure X) (ν : MeasureTheory.ProbabilityMeasure Y) (hc : LowerSemicontinuous c) : ∃ (π : Coupling μ ν), IsOptimalCoupling c ↑↑π ↑μ ↑ν

Primal attainment with the optimal plan delivered inside the bundled coupling type, which is the domain the probability transport problem is optimised over.

theorem TauCeti.exists_isOptimalCoupling_edist {X : Type u_3} [PseudoEMetricSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : ∃ (π : MeasureTheory.Measure (X × X)), IsOptimalCoupling (fun (z : X × X) => edist z.1 z.2) π μ ν

On a Polish space with a compatible extended pseudometric, the Kantorovich–Rubinstein cost edist admits an optimal transport plan between any two probability measures. The chosen extended pseudometric need not be complete.

theorem TauCeti.exists_isOptimalCoupling_edist_rpow {X : Type u_3} [PseudoEMetricSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (p : ℝ) : ∃ (π : MeasureTheory.Measure (X × X)), IsOptimalCoupling (fun (z : X × X) => edist z.1 z.2 ^ p) π μ ν

The cost edist ^ p underlying the p-Wasserstein distance admits an optimal transport plan on a Polish space with a compatible extended pseudometric, without completeness of that chosen pseudometric. The exponent is unrestricted because ENNReal.rpow is continuous for every real exponent; the case the Wasserstein distances use is 1 ≤ p.