Strong Kantorovich duality for continuous costs on compact spaces

For probability measures μ and ν on two compact pseudometric spaces whose open sets are measurable, and a continuous nonnegative cost c on their product, the transport problem and its dual have the same value:

(transportCost (ENNReal.ofReal ∘ c) μ ν).toReal = sSup {kantorovichDualValue μ ν φ ψ},

the supremum running over the pairs of continuous potentials with φ x + ψ y ≤ c (x, y). Weak duality, proved for the general interface in TauCeti.MeasureTheory.OptimalTransport.Duality.Basic, gives one inequality; this file supplies the other one and hence closes the gap.

The proof is the finite approximation argument. Uniform continuity of c turns a δ-net of each factor into a pair of measurable maps qX : X → Fin n and qY : Y → Fin m moving no point by more than δ; pushing the two marginals forward along them produces a finite transport problem whose cost matrix is the cost read at the marked points. Kantorovich duality on finite spaces, already available as TauCeti.exists_cost_eq_finiteDualValue, solves that problem exactly. Its optimal transportation matrix is lifted back to a genuine coupling by gluing the conditional measures on the fibres, which bounds the continuous primal value from above; its optimal potentials are read back as step functions on the fibres, which bounds the continuous dual value from below. Both estimates lose only a multiple of the modulus of continuity, so letting the net refine closes the duality gap.

The smoothing result TauCeti.exists_continuous_feasible_pair_dominating replaces any feasible pair by a continuous one that dominates it pointwise: applying the infimal c-transform twice inherits the modulus of continuity of the cost. This is what upgrades the step-function potentials produced by the finite problem to the continuous potentials the theorem advertises, and it is also why the bounded-continuous and the integrable dual classes have the same supremum. The discretisation lemma TauCeti.exists_measurable_dist_lt is imported from TauCeti.MeasureTheory.MeasurableSpace.Metric; it applies to totally bounded pseudometric spaces, and is used here through isCompact_univ.totallyBounded.

Implementation notes

The transform is spelled here as the real infimum ⨅ x, (c (x, y) - φ x) rather than through the EReal-valued TauCeti.cTransform, because the relevant infima are bounded below and the whole computation stays inside ℝ. The bridge lemmas TauCeti.cTransform_coe and TauCeti.cTransformSymm_coe identify these real infima with the extended-real transforms, so the proof reuses the order-theoretic transform API from TauCeti.MeasureTheory.OptimalTransport.CTransform.Basic.

The cost is taken nonnegative because TauCeti.transportCost measures an ℝ≥0∞-valued cost. A continuous cost on a compact space is bounded below, so this costs no generality beyond an additive normalisation of the cost and of the potentials.

Main statements

• TauCeti.exists_continuous_feasible_pair_dominating — a feasible pair is dominated by a continuous feasible pair;
• TauCeti.exists_continuous_forall_add_le_transportCost_le — the approximate duality: for every ε > 0 there is a continuous feasible pair whose value is within ε of the primal value;
• TauCeti.isLUB_kantorovichDualValue_continuous — strong Kantorovich duality: the primal value is the least upper bound of the values of the continuous feasible pairs;
• TauCeti.isLUB_kantorovichDualValue_integrable — the same value is also the least upper bound over the larger integrable dual class, so the two classes agree;
• TauCeti.toReal_transportCost_eq_sSup and TauCeti.transportCost_eq_ofReal_sSup — the same statement read as an equality of a supremum, in ℝ and in ℝ≥0∞;
• TauCeti.transportCost_ne_top_of_continuous — the primal value is finite. Real-form weak duality is provided by TauCeti.DualFeasible.kantorovichDualValue_le_toReal_transportCost.

References

• C. Villani, Topics in Optimal Transportation, Graduate Studies in Mathematics 58, 2003, Theorem 1.3 and §1.1.
• C. Villani, Optimal Transport: Old and New, Grundlehren 338, 2009, Theorem 5.10.

Joseph K. Miller's Apache-2.0 Hydrodynamical/Vlasov_Meanfield_Formalization development at commit 31186ee11b1c478a35b1775db48384252eb06e22 and Daniel Lyng's Apache-2.0 danlyng/Econlib development at commit 003655ccf010cdf44c4f67d6675167b54ce0e9df contain related finite approximation proofs. The proof here was written independently against Tau Ceti's existing raw-measure, ℝ≥0∞-valued transport-cost and finite-duality APIs; no code was taken from either development.

This is Layer 2, item 4 of the optimal-transport roadmap, in its compact continuous case.

theorem TauCeti.exists_continuous_feasible_pair_dominating {X : Type u} {Y : Type v} [PseudoMetricSpace X] [PseudoMetricSpace Y] {c : X × Y → ℝ} {φ : X → ℝ} {ψ : Y → ℝ} [CompactSpace X] [CompactSpace Y] [Nonempty X] [Nonempty Y] (hc : Continuous c) (hfeas : ∀ (x : X) (y : Y), φ x + ψ y ≤ c (x, y)) : ∃ (φ' : X → ℝ) (ψ' : Y → ℝ), Continuous φ' ∧ Continuous ψ' ∧ (∀ (x : X) (y : Y), φ' x + ψ' y ≤ c (x, y)) ∧ (∀ (x : X), φ x ≤ φ' x) ∧ ∀ (y : Y), ψ y ≤ ψ' y

Smoothing a dual pair. On compact pseudometric spaces, a feasible pair is dominated pointwise by continuous potentials satisfying the same Kantorovich constraint. The improved pair is obtained by applying the infimal c-transform twice, so it inherits the modulus of continuity of the cost.

Lifting a finite transport plan to a coupling

Strong duality

theorem TauCeti.exists_continuous_forall_add_le_transportCost_le {X : Type u} {Y : Type v} [PseudoMetricSpace X] [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [PseudoMetricSpace Y] [CompactSpace Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {c : X × Y → ℝ} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hc : Continuous c) (hc0 : ∀ (z : X × Y), 0 ≤ c z) {ε : ℝ} (hε : 0 < ε) : ∃ (φ : X → ℝ) (ψ : Y → ℝ), Continuous φ ∧ Continuous ψ ∧ (∀ (x : X) (y : Y), φ x + ψ y ≤ c (x, y)) ∧ transportCost (fun (z : X × Y) => ENNReal.ofReal (c z)) μ ν ≤ ENNReal.ofReal (kantorovichDualValue μ ν φ ψ + ε)

Approximate Kantorovich duality on compact spaces. For probability measures on compact pseudometric spaces, a continuous nonnegative cost, and every ε > 0, there is a pair of continuous potentials satisfying the Kantorovich constraint whose value is within ε of the primal transport cost. Together with weak duality this closes the duality gap.

theorem TauCeti.isLUB_kantorovichDualValue_continuous {X : Type u} {Y : Type v} [PseudoMetricSpace X] [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [PseudoMetricSpace Y] [CompactSpace Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {c : X × Y → ℝ} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hc : Continuous c) (hc0 : ∀ (z : X × Y), 0 ≤ c z) : IsLUB {r : ℝ | ∃ (φ : X → ℝ) (ψ : Y → ℝ), Continuous φ ∧ Continuous ψ ∧ (∀ (x : X) (y : Y), φ x + ψ y ≤ c (x, y)) ∧ kantorovichDualValue μ ν φ ψ = r} (transportCost (fun (z : X × Y) => ENNReal.ofReal (c z)) μ ν).toReal

Strong Kantorovich duality on compact pseudometrizable spaces. For probability measures on compact pseudometric spaces and a continuous nonnegative cost, the primal transport cost is the least upper bound of the values of the pairs of continuous potentials satisfying the Kantorovich constraint.

theorem TauCeti.isLUB_kantorovichDualValue_integrable {X : Type u} {Y : Type v} [PseudoMetricSpace X] [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [PseudoMetricSpace Y] [CompactSpace Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {c : X × Y → ℝ} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hc : Continuous c) (hc0 : ∀ (z : X × Y), 0 ≤ c z) : IsLUB {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 against the integrable dual class. For probability measures, enlarging the dual class from the continuous to the merely integrable potentials does not change the value of the dual problem: it is still the primal transport cost.

theorem TauCeti.toReal_transportCost_eq_sSup {X : Type u} {Y : Type v} [PseudoMetricSpace X] [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [PseudoMetricSpace Y] [CompactSpace Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {c : X × Y → ℝ} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hc : Continuous c) (hc0 : ∀ (z : X × Y), 0 ≤ c z) : (transportCost (fun (z : X × Y) => ENNReal.ofReal (c z)) μ ν).toReal = sSup {r : ℝ | ∃ (φ : X → ℝ) (ψ : Y → ℝ), Continuous φ ∧ Continuous ψ ∧ (∀ (x : X) (y : Y), φ x + ψ y ≤ c (x, y)) ∧ kantorovichDualValue μ ν φ ψ = r}

Strong Kantorovich duality for probability measures, read as an equality between the primal value and the supremum of the dual values over the continuous potentials.

theorem TauCeti.transportCost_eq_ofReal_sSup {X : Type u} {Y : Type v} [PseudoMetricSpace X] [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [PseudoMetricSpace Y] [CompactSpace Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {c : X × Y → ℝ} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hc : Continuous c) (hc0 : ∀ (z : X × Y), 0 ≤ c z) : transportCost (fun (z : X × Y) => ENNReal.ofReal (c z)) μ ν = ENNReal.ofReal (sSup {r : ℝ | ∃ (φ : X → ℝ) (ψ : Y → ℝ), Continuous φ ∧ Continuous ψ ∧ (∀ (x : X) (y : Y), φ x + ψ y ≤ c (x, y)) ∧ kantorovichDualValue μ ν φ ψ = r})

Strong Kantorovich duality for probability measures, read in ℝ≥0∞: the primal transport cost is the supremum of the dual values of the continuous feasible pairs.