Transport costs of mixtures

For a fixed cost c, the transport cost is positively homogeneous and countably subadditive as a function of the pair of marginals:

transportCost c (a • μ) (a • ν) = a * transportCost c μ ν and transportCost c (∑ i, μ i) (∑ i, ν i) ≤ ∑ i, transportCost c (μ i) (ν i).

Together they say that the transport cost of a mixture (∑ i, a i • μ i, ∑ i, a i • ν i) is at most the corresponding mixture of the transport costs — the convexity of optimal transport in the two marginals. The reason is that couplings can be mixed: the sum of couplings of the pairs (μ i, ν i) couples the two sums (TauCeti.IsCoupling.sum), and the cost of a plan is additive in the plan.

No finiteness or normalisation is assumed of the measures, and the cost need not be measurable. Subadditivity cannot in general be improved to an equality: splitting δ_x + δ_y against itself as (δ_x, δ_y) + (δ_y, δ_x) with the cost edist gives a strict inequality whenever x ≠ y. Homogeneity is stated for a finite scaling factor. By homogeneity, two optimal plans for the same pair of marginals add up to an optimal plan for the doubled marginals; uniqueness theorems for optimal plans compare two optimal plans through their sum.

Main statements

• TauCeti.transportCost_smul — scaling both marginals by a finite factor scales the transport cost;
• TauCeti.transportCost_sum_le — countable subadditivity for MeasureTheory.Measure.sum;
• TauCeti.transportCost_finset_sum_le and TauCeti.transportCost_add_le — the finite and binary forms of subadditivity;
• TauCeti.transportCost_le_sum_of_split — transport cost along a splitting of both measures into a part matched cell by cell and a remainder bounded by the maximal cost;
• TauCeti.IsOptimalCoupling.add — the sum of two optimal plans for the same marginals is optimal for the doubled marginals;
• TauCeti.transportCost_smul_add_smul_lt — strict convexity in the target: when the optimal plans out of the source into a mixture of two distinct targets are induced by maps, the cost to the mixture is strictly below the mixture of the costs.

References

• C. Villani, Optimal Transport: Old and New, Grundlehren 338, Springer 2009, Theorem 4.8, the convexity of the optimal transport cost in the pair of marginals.

theorem TauCeti.transportCost_smul {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {a : ENNReal} (ha : a ≠ ⊤) (c : X × Y → ENNReal) (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) : transportCost c (a • μ) (a • ν) = a * transportCost c μ ν

Homogeneity of the transport cost. Scaling both marginals by the same finite factor scales the transport cost by that factor. At a = 0 both sides vanish, the zero plan coupling the two zero measures.

theorem TauCeti.IsOptimalCoupling.smul {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {a : ENNReal} {c : X × Y → ENNReal} {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (h : IsOptimalCoupling c π μ ν) (ha : a ≠ ⊤) : IsOptimalCoupling c (a • π) (a • μ) (a • ν)

Scaling an optimal plan by a finite factor preserves optimality, including at zero mass.

theorem TauCeti.transportCost_sum_le {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {ι : Type u_1} [Countable ι] (c : X × Y → ENNReal) (μ : ι → MeasureTheory.Measure X) (ν : ι → MeasureTheory.Measure Y) : transportCost c (MeasureTheory.Measure.sum μ) (MeasureTheory.Measure.sum ν) ≤ ∑' (i : ι), transportCost c (μ i) (ν i)

Countable subadditivity of the transport cost. The transport cost of the sums of two countable families of marginals is at most the sum of the transport costs of the pairs: near optimal plans of the pairs sum to a plan of the sums.

theorem TauCeti.transportCost_finset_sum_le {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {ι : Type u_1} (s : Finset ι) (c : X × Y → ENNReal) (μ : ι → MeasureTheory.Measure X) (ν : ι → MeasureTheory.Measure Y) : transportCost c (∑ i ∈ s, μ i) (∑ i ∈ s, ν i) ≤ ∑ i ∈ s, transportCost c (μ i) (ν i)

Finite subadditivity of the transport cost.

theorem TauCeti.transportCost_add_le {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] (c : X × Y → ENNReal) (μ μ' : MeasureTheory.Measure X) (ν ν' : MeasureTheory.Measure Y) : transportCost c (μ + μ') (ν + ν') ≤ transportCost c μ ν + transportCost c μ' ν'

Subadditivity of the transport cost for two pairs of marginals.

theorem TauCeti.IsOptimalCoupling.add {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → ENNReal} {π π' : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (h : IsOptimalCoupling c π μ ν) (h' : IsOptimalCoupling c π' μ ν) : IsOptimalCoupling c (π + π') (μ + μ) (ν + ν)

Two optimal plans add up to an optimal plan. If π and π' are optimal plans between μ and ν, their sum is an optimal plan between μ + μ and ν + ν, whose transport cost is twice that of μ and ν by homogeneity.

theorem TauCeti.transportCost_smul_add_smul_lt {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {a : ENNReal} [MeasurableEq Y] {c : X × Y → ENNReal} {π₀ π₁ : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν₀ ν₁ : MeasureTheory.Measure Y} {b : ENNReal} (hab : a + b = 1) (ha : a ≠ 0) (hb : b ≠ 0) (h₀ : IsOptimalCoupling c π₀ μ ν₀) (h₁ : IsOptimalCoupling c π₁ μ ν₁) (hgraph : ∀ (π : MeasureTheory.Measure (X × Y)), IsOptimalCoupling c π μ (a • ν₀ + b • ν₁) → ∃ (T : X → Y), AEMeasurable T μ ∧ π = graphPlan T μ) (hne : ν₀ ≠ ν₁) : transportCost c μ (a • ν₀ + b • ν₁) < a * transportCost c μ ν₀ + b * transportCost c μ ν₁

Strict convexity of the transport cost in the target. Let π₀ and π₁ be optimal plans from μ to ν₀ and to ν₁, and let a, b be nonzero weights with a + b = 1. If every optimal plan from μ to the mixture a • ν₀ + b • ν₁ is induced by a map and ν₀ ≠ ν₁, then the transport cost from μ to the mixture is strictly below the mixture of the two transport costs.

theorem TauCeti.transportCost_le_sum_of_split {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {ι : Type u_1} [Fintype ι] {c : X × Y → ENNReal} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsFiniteMeasure μ] {α α' : ι → MeasureTheory.Measure X} {β β' : ι → MeasureTheory.Measure Y} (hμ : μ = ∑ i : ι, α i + ∑ i : ι, α' i) (hν : ν = ∑ i : ι, β i + ∑ i : ι, β' i) (h : μ Set.univ = ν Set.univ) (hαβ : ∀ (i : ι), (α i) Set.univ = (β i) Set.univ) {w r : ι → ENNReal} (hcell : ∀ (i : ι), transportCost c (α i) (β i) ≤ w i) {M : ENNReal} (hM : ∀ (z : X × Y), c z ≤ M) (hα' : ∀ (i : ι), (α' i) Set.univ = r i) : transportCost c μ ν ≤ ∑ i : ι, w i + M * ∑ i : ι, r i

Transport along a splitting of both measures. If two finite measures of equal mass are split into pieces α i + α' i and β i + β' i, where α i and β i have equal mass and cost at most w i, and the cost is at most M everywhere, then the transport cost is at most the sum of the w i plus M times the total mass of the pieces α' i.