Dual attainment for bounded continuous costs

For a bounded continuous nonnegative cost c on a product of two Polish spaces, the Kantorovich dual problem is attained: there is an integrable pair of potentials φ, ψ with φ x + ψ y ≤ c (x, y) whose value ∫ φ dμ + ∫ ψ dν equals the optimal transport cost. No compactness is assumed, so this is strong duality with dual attainment in the Polish regime.

The results are phrased through optimality certificates (TauCeti.IsDualCertificate): a coupling π together with integrable dual feasible potentials φ, ψ such that π is concentrated on the contact set {(x, y) | φ x + ψ y = c (x, y)}. Such a certificate proves at once that π is an optimal plan, that (φ, ψ) is an optimal dual pair, and that there is no duality gap. Here every optimal plan admits a certificate, so the dual optimizer may be chosen to certify any given optimal plan, not only one produced by an existence theorem.

The potentials obtained are c-conjugate: each is the real infimal transform of the other, φ x = ⨅ y, (c (x, y) - ψ y) and ψ y = ⨅ x, (c (x, y) - φ x). In particular they are bounded, and they inherit any uniform modulus of continuity that the sections of the cost share, through TauCeti.uniformContinuous_iInf_sub.

Main statements

• TauCeti.IsOptimalCoupling.exists_isDualCertificate_of_continuous — every optimal plan of a bounded continuous nonnegative cost between probability measures on spaces whose product is hereditarily Lindelöf (for instance second countable) is certified by a pair of c-conjugate integrable potentials;
• TauCeti.exists_isDualCertificate_of_continuous — on Polish spaces, an optimal plan together with such a certificate exists;
• TauCeti.isGreatest_kantorovichDualValue_integrable — strong duality with dual attainment on Polish spaces: the primal value is the maximum of the values of the integrable dual feasible pairs.

References

• C. Villani, Optimal Transport: Old and New, Grundlehren 338, Springer 2009, Chapter 5, Theorem 5.10, whose proof builds the dual optimizer from the cyclically monotone support of an optimal plan.
• L. Rüschendorf, On c-optimal random variables, Statist. Probab. Lett. 27 (1996), 267--270, for the c-concave potential of a cyclically monotone set.

theorem TauCeti.IsOptimalCoupling.exists_isDualCertificate_of_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [TopologicalSpace Y] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {c : X × Y → ℝ} [OpensMeasurableSpace X] [OpensMeasurableSpace Y] [OpensMeasurableSpace (X × Y)] [HereditarilyLindelofSpace (X × Y)] [MeasureTheory.IsProbabilityMeasure μ] {π : MeasureTheory.Measure (X × Y)} (hπ : IsOptimalCoupling (fun (z : X × Y) => ENNReal.ofReal (c z)) π μ ν) (hc : Continuous c) (hc0 : ∀ (z : X × Y), 0 ≤ c z) (hcb : BddAbove (Set.range c)) : ∃ (φ : X → ℝ) (ψ : Y → ℝ), IsDualCertificate (fun (z : X × Y) => ENNReal.ofReal (c z)) π μ ν φ ψ ∧ (∀ (x : X), φ x = ⨅ (y : Y), c (x, y) - ψ y) ∧ ∀ (y : Y), ψ y = ⨅ (x : X), c (x, y) - φ x

Optimal plans of bounded continuous costs are certified. Let c be a bounded continuous nonnegative cost and π an optimal coupling of two probability measures, on spaces whose product is hereditarily Lindelöf with measurable open sets (for instance, two second-countable Borel spaces). Then there are integrable potentials φ, ψ forming an optimality certificate with π: they are dual feasible and π is concentrated on their contact set. The potentials are c-conjugate, each being the real infimal transform of the other.

theorem TauCeti.exists_isDualCertificate_of_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [TopologicalSpace Y] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {c : X × Y → ℝ} [PolishSpace X] [BorelSpace X] [PolishSpace Y] [BorelSpace Y] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hc : Continuous c) (hc0 : ∀ (z : X × Y), 0 ≤ c z) (hcb : BddAbove (Set.range c)) : ∃ (π : MeasureTheory.Measure (X × Y)) (φ : X → ℝ) (ψ : Y → ℝ), IsDualCertificate (fun (z : X × Y) => ENNReal.ofReal (c z)) π μ ν φ ψ ∧ (∀ (x : X), φ x = ⨅ (y : Y), c (x, y) - ψ y) ∧ ∀ (y : Y), ψ y = ⨅ (x : X), c (x, y) - φ x

Existence of a certified optimal plan on Polish spaces. For a bounded continuous nonnegative cost and two probability measures on Polish spaces, there are an optimal coupling and a pair of c-conjugate integrable potentials certifying it.

theorem TauCeti.isGreatest_kantorovichDualValue_integrable {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [TopologicalSpace Y] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {c : X × Y → ℝ} [PolishSpace X] [BorelSpace X] [PolishSpace Y] [BorelSpace Y] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hc : Continuous c) (hc0 : ∀ (z : X × Y), 0 ≤ c z) (hcb : BddAbove (Set.range c)) : IsGreatest {r : ℝ | ∃ (φ : X → ℝ) (ψ : Y → ℝ), MeasureTheory.Integrable φ μ ∧ MeasureTheory.Integrable ψ ν ∧ (∀ (x : X) (y : Y), φ x + ψ y ≤ c (x, y)) ∧ kantorovichDualValue μ ν φ ψ = r} (transportCost (fun (z : X × Y) => ENNReal.ofReal (c z)) μ ν).toReal

Strong Kantorovich duality with dual attainment on Polish spaces. For a bounded continuous nonnegative cost and two probability measures on Polish spaces, the optimal transport cost is the greatest value of an integrable dual feasible pair: the dual supremum is attained.