Transport costs along finite partitions

Two measures of equal finite mass can be transported cell by cell along matching finite measurable partitions of the two spaces. The deterministic estimate TauCeti.transportCost_le_sum_of_partition bounds their transport cost by the cost inside matching cells, weighted by the second measure, plus a bound on the cost times the mass by which the first measure exceeds the second cell by cell. The plan matches the common mass inside each cell (TauCeti.transportCost_le_mul_of_ae_mem) and moves the remaining mass arbitrarily; the estimate combines with the subadditivity of the transport cost in its marginals.

Main statements

• TauCeti.transportCost_le_mul_of_ae_mem — two measures of equal mass concentrated on sets on whose product the cost is at most η have transport cost at most η times their mass;
• TauCeti.transportCost_le_sum_of_partition — the transport cost of two measures of equal mass is controlled by matching finite partitions of the two spaces.

theorem TauCeti.transportCost_le_mul_of_ae_mem {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → ENNReal} {A : Set X} {B : Set Y} (hA : MeasurableSet A) (hB : MeasurableSet B) {η : ENNReal} (hc : ∀ x ∈ A, ∀ y ∈ B, c (x, y) ≤ η) {α : MeasureTheory.Measure X} {β : MeasureTheory.Measure Y} [MeasureTheory.IsFiniteMeasure α] (hαA : ∀ᵐ (x : X) ∂α, x ∈ A) (hβB : ∀ᵐ (y : Y) ∂β, y ∈ B) (h : α Set.univ = β Set.univ) : transportCost c α β ≤ η * α Set.univ

Transport inside a cell. Two measures of equal finite mass, concentrated on measurable sets A and B on whose product the cost is at most η, have transport cost at most η times their common mass.

theorem TauCeti.transportCost_le_sum_of_partition {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → ENNReal} {ι : Type u_3} [Fintype ι] {A : ι → Set X} {B : ι → Set Y} (hAm : ∀ (i : ι), MeasurableSet (A i)) (hBm : ∀ (i : ι), MeasurableSet (B i)) (hAd : Pairwise (Function.onFun Disjoint A)) (hBd : Pairwise (Function.onFun Disjoint B)) (hAu : ⋃ (i : ι), A i = Set.univ) (hBu : ⋃ (i : ι), B i = Set.univ) {η : ι → ENNReal} (hc : ∀ (i : ι), ∀ x ∈ A i, ∀ y ∈ B i, c (x, y) ≤ η i) {M : ENNReal} (hM : ∀ (z : X × Y), c z ≤ M) (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) [MeasureTheory.IsFiniteMeasure μ] (h : μ Set.univ = ν Set.univ) : transportCost c μ ν ≤ ∑ i : ι, η i * ν (B i) + M * ∑ i : ι, (μ (A i) - ν (B i))

Transport along matching partitions. Let A and B be finite measurable partitions of X and Y indexed by the same type, such that the cost is at most η i on A i × B i and at most M everywhere. Then two measures of equal finite mass have transport cost at most the sum of the η i weighted by the masses ν (B i), plus M times the total mass by which μ exceeds ν cell by cell.

The plan matches the common mass min (μ (A i)) (ν (B i)) inside each cell and moves the remaining mass arbitrarily, at cost at most M per unit of mass.