Existence of optimal multi-marginal couplings

The multi-marginal couplings of finitely many tight probability measures μ i on spaces X i (for instance, any probability measures on Polish spaces) form, under the separation hypotheses of Prokhorov's theorem, a weakly compact set of probability measures on the product ∀ i, X i. If moreover the spaces X i are second countable metrizable Borel spaces, a lower semicontinuous cost c : (∀ i, X i) → ℝ≥0∞ attains its infimum on it. This is the multi-marginal form of the existence theorem for optimal transport plans, and the argument is the same.

• Closedness: being a multi-coupling says that each coordinate pushforward π.map (eval i) is μ i, and pushing forward along a continuous coordinate projection is weakly continuous.
• Tightness: for n marginals, if K i is a compact set missing at most ε / n of the mass of μ i, the compact box univ.pi K misses at most ε of the mass of every multi-coupling, because the complement of the box is covered by the preimages of the complements of its sides.
• Compactness then follows from Prokhorov's theorem, and existence of a minimizer from the lower semicontinuity of π ↦ ∫⁻ c ∂π for the weak topology.

The index type is finite, and the minimum value may be ∞.

Main statements

• TauCeti.isClosed_setOfPred_isMultiCoupling: the multi-couplings are weakly closed;
• TauCeti.isTightMeasureSet_setOfPred_isMultiCoupling: the multi-couplings of tight measures form a tight family;
• TauCeti.isCompact_setOfPred_isMultiCoupling: Prokhorov's theorem for multi-couplings;
• TauCeti.exists_isMultiCoupling_isMinOn_lintegral: a lower semicontinuous cost has an optimal multi-coupling.

References

• B. Pass, Multi-marginal optimal transport: theory and applications, ESAIM Math. Model. Numer. Anal. 49 (2015), 1771--1790, Section 2, for existence of optimal multi-marginal plans.

theorem TauCeti.isClosed_setOfPred_isMultiCoupling {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → MeasurableSpace (X i)] [∀ (i : ι), OpensMeasurableSpace (X i)] [OpensMeasurableSpace ((i : ι) → X i)] [∀ (i : ι), T1Space (MeasureTheory.ProbabilityMeasure (X i))] (μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)) : IsClosed {π : MeasureTheory.ProbabilityMeasure ((i : ι) → X i) | Measure.IsMultiCoupling ↑π fun (i : ι) => ↑(μ i)}

The multi-couplings of probability measures are weakly closed. The multi-coupling set is the intersection, over the coordinates i, of the preimages of {μ i} under the weakly continuous coordinate pushforwards. The T1Space hypotheses make these singletons closed.

theorem TauCeti.isTightMeasureSet_setOfPred_isMultiCoupling {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → MeasurableSpace (X i)] [Finite ι] {μ : (i : ι) → MeasureTheory.Measure (X i)} (hμ : ∀ (i : ι), MeasureTheory.IsTightMeasureSet {μ i}) : MeasureTheory.IsTightMeasureSet {π : MeasureTheory.Measure ((i : ι) → X i) | Measure.IsMultiCoupling π μ}

The multi-couplings of finitely many tight measures form a tight family. A compact box univ.pi K misses, for every multi-coupling, at most the total mass that the marginals give the complements of its sides. No hypothesis beyond the topologies is needed.

theorem TauCeti.isCompact_setOfPred_isMultiCoupling {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → MeasurableSpace (X i)] [Finite ι] [∀ (i : ι), OpensMeasurableSpace (X i)] [∀ (i : ι), T1Space (MeasureTheory.ProbabilityMeasure (X i))] [BorelSpace ((i : ι) → X i)] [T2Space ((i : ι) → X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} (hμ : ∀ (i : ι), MeasureTheory.IsTightMeasureSet {↑(μ i)}) : IsCompact {π : MeasureTheory.ProbabilityMeasure ((i : ι) → X i) | Measure.IsMultiCoupling ↑π fun (i : ι) => ↑(μ i)}

Prokhorov's theorem for multi-couplings. The multi-couplings of finitely many tight probability measures form a weakly compact set: it is tight, hence relatively compact, and closed.

theorem TauCeti.exists_isMultiCoupling_isMinOn_lintegral {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → MeasurableSpace (X i)] [Finite ι] [Nonempty ι] [∀ (i : ι), TopologicalSpace.MetrizableSpace (X i)] [∀ (i : ι), SecondCountableTopology (X i)] [∀ (i : ι), BorelSpace (X i)] {μ : (i : ι) → MeasureTheory.Measure (X i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (hμ : ∀ (i : ι), MeasureTheory.IsTightMeasureSet {μ i}) {c : ((i : ι) → X i) → ENNReal} (hc : LowerSemicontinuous c) : ∃ (γ : MeasureTheory.Measure ((i : ι) → X i)), Measure.IsMultiCoupling γ μ ∧ IsMinOn (fun (γ' : MeasureTheory.Measure ((i : ι) → X i)) => ∫⁻ (x : (i : ι) → X i), c x ∂γ') {γ' : MeasureTheory.Measure ((i : ι) → X i) | Measure.IsMultiCoupling γ' μ} γ

Existence of an optimal multi-coupling. For finitely many tight probability measures on second countable metrizable Borel spaces, for instance Polish spaces, a lower semicontinuous cost c : (∀ i, X i) → ℝ≥0∞ attains its infimum over the multi-couplings: some multi-coupling γ satisfies ∫⁻ c ∂γ ≤ ∫⁻ c ∂γ' for every multi-coupling γ'. The minimum may be ∞. The index type is nonempty, so that every multi-coupling is a probability measure.