Realizing a coupling along a source partition

A coupling with atomless source can be realized by a single measurable transport map at the resolution of any countable measurable source partition. For each cell A i, its graph plan agrees with the coupling on every rectangle A i × B, retaining the entire target law within that cell, rather than just the masses of a chosen target partition.

The construction transports the restricted source on each cell to the second marginal of the coupling restricted to that cell, then glues the maps. The gluing step, TauCeti.IsCoupling.exists_measurePreserving_restrict, applies to any disjoint measurable pieces covering the coupling and any disjoint source sets of matching masses. This is the measure-theoretic step in approximating couplings by graph plans: increasingly fine source partitions retain increasingly more information about the original coupling. No topology is needed for this step.

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.1, for the role of graph-plan density in the bounded continuous-cost problem.

theorem TauCeti.IsCoupling.exists_measurePreserving_restrict {X : Type u_1} {Y : Type u_2} {ι : Type u_3} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] [Nonempty Y] [Countable ι] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.NullSingletonClass μ] (hπ : IsCoupling π μ ν) {S : ι → Set (X × Y)} (hSm : ∀ (i : ι), MeasurableSet (S i)) (hSd : Pairwise (Function.onFun Disjoint S)) (hScov : ∀ᵐ (z : X × Y) ∂π, z ∈ ⋃ (i : ι), S i) {Z : ι → Set X} (hZm : ∀ (i : ι), MeasurableSet (Z i)) (hZd : Pairwise (Function.onFun Disjoint Z)) (hZμ : ∀ (i : ι), μ (Z i) = π (S i)) : ∃ (T : X → Y), MeasureTheory.MeasurePreserving T μ ν ∧ (∀ (i : ι), MeasureTheory.MeasurePreserving T (μ.restrict (Z i)) (π.restrict (S i)).snd) ∧ μ (⋃ (i : ι), Z i)ᶜ = 0

Let π be concentrated on a union of disjoint measurable pieces S i, and let Z i be disjoint measurable source sets with μ (Z i) = π (S i). Then one transport map sends μ restricted to each Z i to the second marginal of π restricted to S i, and the sets Z i exhaust μ.

theorem TauCeti.IsCoupling.exists_measurePreserving_graphPlan_prod_eq {X : Type u_1} {Y : Type u_2} {ι : Type u_3} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] [Nonempty Y] [Countable ι] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.NullSingletonClass μ] (hπ : IsCoupling π μ ν) {A : ι → Set X} (hAm : ∀ (i : ι), MeasurableSet (A i)) (hAd : Pairwise (Function.onFun Disjoint A)) (hAu : ⋃ (i : ι), A i = Set.univ) : ∃ (T : X → Y), MeasureTheory.MeasurePreserving T μ ν ∧ ∀ (i : ι) (B : Set Y), MeasurableSet B → (graphPlan T μ) (A i ×ˢ B) = π (A i ×ˢ B)

A coupling with atomless source has a graph-plan realization on every countable measurable source partition. The map preserves the full target law and the mass of every rectangle whose source side is a partition cell. Zero-mass cells are allowed.

theorem TauCeti.IsCoupling.exists_measurePreserving_map_graphPlan_eq {X : Type u_1} {Y : Type u_2} {ι : Type u_3} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] [Nonempty Y] [Countable ι] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.NullSingletonClass μ] (hπ : IsCoupling π μ ν) [MeasurableSpace ι] [MeasurableSingletonClass ι] {q : X → ι} (hq : Measurable q) : ∃ (T : X → Y), MeasureTheory.MeasurePreserving T μ ν ∧ MeasureTheory.Measure.map (Prod.map q id) (graphPlan T μ) = MeasureTheory.Measure.map (Prod.map q id) π

After observing the source through a countable-valued measurable map q, every coupling with atomless source is exactly the joint law of q and a measurable transport map. Thus the coupling and its graph-plan realization have identical pushforwards under Prod.map q id.