Optimal plans of lower semicontinuous costs are cyclically monotone

For a lower semicontinuous cost c : X × Y → ℝ≥0∞ on Polish spaces, every optimal coupling of finite cost is concentrated on a measurable c-cyclically monotone set. The cost may take the value ∞. Unlike TauCeti.IsOptimalCoupling.isCyclicallyMonotone_support, continuity of the cost is not needed; in exchange, the statement concerns some set of full measure rather than the topological support of the plan.

The proof goes through strong duality instead of a perturbation of the plan. By TauCeti.isLUB_ofReal_kantorovichDualValue_integrable_of_lowerSemicontinuous there are integrable feasible pairs (φ n, ψ n) whose dual values tend to the optimal cost. Against an optimal plan π the defects c (x, y) - φ n x - ψ n y are nonnegative and their π-integrals tend to zero, so a subsequence of the defects tends to zero π-almost everywhere. On the set where this happens, each equality c (x, y) = lim (φ n x + ψ n y) survives passage to the limit, while a permutation of the targets only produces inequalities. That set is therefore c-cyclically monotone: it is an asymptotic contact set, generalising the contact set of a single dual feasible pair.

Main statements

• TauCeti.isCyclicallyMonotone_setOf_tendsto — the asymptotic contact set of a family of dual feasible pairs is c-cyclically monotone;
• TauCeti.IsCoupling.exists_seq_tendsto_ae_of_tendsto_kantorovichDualValue — if the dual values of feasible pairs tend to the cost of a plan, then along a subsequence their split sums converge to the cost almost everywhere for that plan;
• TauCeti.exists_seq_tendsto_kantorovichDualValue_of_lowerSemicontinuous — on Polish spaces a finite optimal cost of a lower semicontinuous cost is the limit of real integrable dual values;
• TauCeti.IsOptimalCoupling.exists_isCyclicallyMonotone_of_lowerSemicontinuous — an optimal plan of finite cost for a lower semicontinuous cost on Polish spaces is concentrated on a measurable c-cyclically monotone set.

The converse, that concentration on a c-cyclically monotone set forces optimality when the cost is finite-valued, is the Schachermayer--Teichmann theorem TauCeti.IsCoupling.isOptimalCoupling_iff_exists_isCyclicallyMonotone.

References

• C. Villani, Optimal Transport: Old and New, Grundlehren 338, Springer 2009, Theorem 5.10 (ii); the limit of a maximizing dual sequence follows the proof given there.
• L. Ambrosio and A. Pratelli, Existence and stability results in the L¹ theory of optimal transportation, in Optimal Transportation and Applications, Lecture Notes in Math. 1813, Springer 2003, Theorem 3.2.

theorem TauCeti.isCyclicallyMonotone_setOf_tendsto {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {ι : Type u_1} {l : Filter ι} [l.NeBot] {φ : ι → X → ℝ} {ψ : ι → Y → ℝ} (h : ∀ (i : ι), DualFeasible (fun (z : X × Y) => ↑(c z)) (φ i) (ψ i)) : IsCyclicallyMonotone c {z : X × Y | c z ≠ ⊤ ∧ Filter.Tendsto (fun (i : ι) => φ i z.1 + ψ i z.2) l (nhds (c z).toReal)}

Asymptotic contact sets are c-cyclically monotone. Let (φ i, ψ i) be a family of dual feasible pairs for c, indexed along a nontrivial filter. The set of pairs (x, y) of finite cost at which φ i x + ψ i y tends to c (x, y) is c-cyclically monotone. For a constant family this set is the contact set of a single feasible pair.

theorem TauCeti.IsCoupling.exists_seq_tendsto_ae_of_tendsto_kantorovichDualValue {X : Type u} {Y : Type v} {c : X × Y → ENNReal} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} (hπ : IsCoupling π μ ν) (hc : AEMeasurable c π) (hfin : ∫⁻ (z : X × Y), c z ∂π ≠ ⊤) {φ : ℕ → X → ℝ} {ψ : ℕ → Y → ℝ} (hφ : ∀ (n : ℕ), MeasureTheory.Integrable (φ n) μ) (hψ : ∀ (n : ℕ), MeasureTheory.Integrable (ψ n) ν) (hf : ∀ (n : ℕ), DualFeasible (fun (z : X × Y) => ↑(c z)) (φ n) (ψ n)) (hlim : Filter.Tendsto (fun (n : ℕ) => kantorovichDualValue μ ν (φ n) (ψ n)) Filter.atTop (nhds (∫⁻ (z : X × Y), c z ∂π).toReal)) : ∃ (ns : ℕ → ℕ), StrictMono ns ∧ ∀ᵐ (z : X × Y) ∂π, Filter.Tendsto (fun (k : ℕ) => φ (ns k) z.1 + ψ (ns k) z.2) Filter.atTop (nhds (c z).toReal)

Maximizing dual sequences converge almost everywhere on a plan. Let π couple μ and ν with finite cost ∫⁻ c ∂π, and let (φ n, ψ n) be integrable dual feasible pairs whose dual values tend to that cost. Then along a subsequence, φ n x + ψ n y tends to c (x, y) for π-almost every (x, y).

theorem TauCeti.exists_seq_tendsto_kantorovichDualValue_of_lowerSemicontinuous {X : Type u} {Y : Type v} {c : X × Y → ENNReal} [TopologicalSpace X] [MeasurableSpace X] [PolishSpace X] [BorelSpace X] [TopologicalSpace Y] [MeasurableSpace Y] [PolishSpace Y] [BorelSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hc : LowerSemicontinuous c) (hfin : transportCost c μ ν ≠ ⊤) : ∃ (φ : ℕ → X → ℝ) (ψ : ℕ → Y → ℝ), (∀ (n : ℕ), MeasureTheory.Integrable (φ n) μ) ∧ (∀ (n : ℕ), MeasureTheory.Integrable (ψ n) ν) ∧ (∀ (n : ℕ), DualFeasible (fun (z : X × Y) => ↑(c z)) (φ n) (ψ n)) ∧ Filter.Tendsto (fun (n : ℕ) => kantorovichDualValue μ ν (φ n) (ψ n)) Filter.atTop (nhds (transportCost c μ ν).toReal)

A maximizing dual sequence for a lower semicontinuous cost. On Polish spaces, a finite optimal cost of a lower semicontinuous cost c : X × Y → ℝ≥0∞ is the limit of the real values of integrable dual feasible pairs. Unlike TauCeti.isLUB_ofReal_kantorovichDualValue_integrable_of_lowerSemicontinuous, the dual values are not truncated at zero.

theorem TauCeti.IsOptimalCoupling.exists_isCyclicallyMonotone_of_lowerSemicontinuous {X : Type u} {Y : Type v} {c : X × Y → ENNReal} [TopologicalSpace X] [MeasurableSpace X] [PolishSpace X] [BorelSpace X] [TopologicalSpace Y] [MeasurableSpace Y] [PolishSpace Y] [BorelSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {π : MeasureTheory.Measure (X × Y)} (h : IsOptimalCoupling c π μ ν) (hc : LowerSemicontinuous c) (hfin : transportCost c μ ν ≠ ⊤) : ∃ (S : Set (X × Y)), MeasurableSet S ∧ IsCyclicallyMonotone c S ∧ π Sᶜ = 0

Optimal plans of lower semicontinuous costs are cyclically monotone. For a lower semicontinuous cost c : X × Y → ℝ≥0∞ and probability measures on Polish spaces, an optimal coupling of finite cost is concentrated on a measurable c-cyclically monotone set.

Finiteness of the optimal cost cannot be dropped: when it is infinite every coupling is optimal. For a continuous cost, TauCeti.IsOptimalCoupling.isCyclicallyMonotone_support gives the topological support as such a set.