Kantorovich duality for lower-semicontinuous costs

This file extends Kantorovich duality from continuous finite costs to arbitrary lower-semicontinuous costs c : X × Y → ℝ≥0∞, first on compact metrizable spaces and then on Polish spaces. In particular, the cost may be unbounded or take the value ∞, so the common primal and dual value is retained in ℝ≥0∞.

The bridge is the monotone bounded-continuous approximation TauCeti.lscApprox. For tight marginals on metrizable spaces, minimization over the compact coupling set commutes with this increasing supremum:

transportCost c μ ν = ⨆ n, transportCost (lscApprox c n) μ ν.

For the nontrivial inequality, the sublevel sets of the approximate integral functionals are a decreasing sequence of nonempty closed subsets of the compact coupling set. A plan in their intersection has c-cost bounded by the supremum of the approximate optimal values. Applying continuous compact duality at every approximation then identifies the original transport cost with the supremum of the positive parts of the values of continuous dual-feasible potentials. On Polish spaces the approximations are bounded and Lipschitz, so their certifying potentials, being conjugate to each other, are bounded and uniformly continuous; the supremum may therefore be restricted to bounded continuous potentials.

Main statements

• TauCeti.isLUB_ofReal_kantorovichDualValue_continuous_of_lowerSemicontinuous — strong Kantorovich duality for a lower-semicontinuous extended-nonnegative cost on compact metrizable spaces, in a form that permits the value ∞;
• TauCeti.transportCost_eq_sSup_ofReal_kantorovichDualValue_continuous_of_lowerSemicontinuous — the same result as an equality with the supremum of the continuous dual values.
• TauCeti.isLUB_ofReal_kantorovichDualValue_integrable_of_lowerSemicontinuous — strong Kantorovich duality on Polish spaces, with the supremum taken over integrable feasible pairs.
• TauCeti.isLUB_ofReal_kantorovichDualValue_boundedContinuous_of_lowerSemicontinuous — the same duality with the supremum taken over feasible pairs of bounded continuous functions.

References

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

The nonnegative case treated here is the base case for costs bounded below by integrable split marginal terms: subtracting such a lower bound reduces a signed cost to a nonnegative one.

theorem TauCeti.isLUB_ofReal_kantorovichDualValue_continuous_of_lowerSemicontinuous {X : Type u} {Y : Type v} [TopologicalSpace X] [MeasurableSpace X] [TopologicalSpace Y] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {c : X × Y → ENNReal} [TopologicalSpace.MetrizableSpace X] [CompactSpace X] [BorelSpace X] [TopologicalSpace.MetrizableSpace Y] [CompactSpace Y] [BorelSpace Y] (hc : LowerSemicontinuous c) : IsLUB {r : ENNReal | ∃ (φ : X → ℝ) (ψ : Y → ℝ), Continuous φ ∧ Continuous ψ ∧ DualFeasible (fun (z : X × Y) => ↑(c z)) φ ψ ∧ ENNReal.ofReal (kantorovichDualValue μ ν φ ψ) = r} (transportCost c μ ν)

Strong Kantorovich duality for lower-semicontinuous costs on compact metrizable spaces. The primal transport cost is the least upper bound, in ℝ≥0∞, of the positive parts of the values of continuous dual-feasible potential pairs.

The extended-nonnegative codomain is essential: an unbounded or infinite-valued cost can have primal value ∞, in which case the continuous dual values are unbounded rather than attaining a real supremum.

theorem TauCeti.transportCost_eq_sSup_ofReal_kantorovichDualValue_continuous_of_lowerSemicontinuous {X : Type u} {Y : Type v} [TopologicalSpace X] [MeasurableSpace X] [TopologicalSpace Y] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {c : X × Y → ENNReal} [TopologicalSpace.MetrizableSpace X] [CompactSpace X] [BorelSpace X] [TopologicalSpace.MetrizableSpace Y] [CompactSpace Y] [BorelSpace Y] (hc : LowerSemicontinuous c) : transportCost c μ ν = sSup {r : ENNReal | ∃ (φ : X → ℝ) (ψ : Y → ℝ), Continuous φ ∧ Continuous ψ ∧ DualFeasible (fun (z : X × Y) => ↑(c z)) φ ψ ∧ ENNReal.ofReal (kantorovichDualValue μ ν φ ψ) = r}

Strong compact duality for a lower-semicontinuous extended-nonnegative cost, written as an equality between the primal value and the supremum of the positive parts of all continuous dual values. This formulation remains meaningful when the common value is ∞.

theorem TauCeti.isLUB_ofReal_kantorovichDualValue_integrable_of_lowerSemicontinuous {X : Type u} {Y : Type v} [TopologicalSpace X] [MeasurableSpace X] [TopologicalSpace Y] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {c : X × Y → ENNReal} [PolishSpace X] [BorelSpace X] [PolishSpace Y] [BorelSpace Y] (hc : LowerSemicontinuous c) : IsLUB {r : ENNReal | ∃ (φ : X → ℝ) (ψ : Y → ℝ), MeasureTheory.Integrable φ μ ∧ MeasureTheory.Integrable ψ ν ∧ DualFeasible (fun (z : X × Y) => ↑(c z)) φ ψ ∧ ENNReal.ofReal (kantorovichDualValue μ ν φ ψ) = r} (transportCost c μ ν)

Strong Kantorovich duality for nonnegative lower-semicontinuous costs on Polish spaces. The primal transport cost is the least upper bound, in ℝ≥0∞, of the positive parts of the values of all integrable dual-feasible pairs. Both the cost and the common value may be infinite.

Unlike dual attainment for bounded continuous costs, this theorem asserts equality of primal and dual values only: an unbounded lower-semicontinuous cost need not have an integrable dual optimizer.

theorem TauCeti.transportCost_eq_sSup_ofReal_kantorovichDualValue_integrable_of_lowerSemicontinuous {X : Type u} {Y : Type v} [TopologicalSpace X] [MeasurableSpace X] [TopologicalSpace Y] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {c : X × Y → ENNReal} [PolishSpace X] [BorelSpace X] [PolishSpace Y] [BorelSpace Y] (hc : LowerSemicontinuous c) : transportCost c μ ν = sSup {r : ENNReal | ∃ (φ : X → ℝ) (ψ : Y → ℝ), MeasureTheory.Integrable φ μ ∧ MeasureTheory.Integrable ψ ν ∧ DualFeasible (fun (z : X × Y) => ↑(c z)) φ ψ ∧ ENNReal.ofReal (kantorovichDualValue μ ν φ ψ) = r}

Polish lower-semicontinuous Kantorovich duality, written as equality with the supremum of the positive parts of all integrable dual values.

theorem TauCeti.isLUB_ofReal_kantorovichDualValue_boundedContinuous_of_lowerSemicontinuous {X : Type u} {Y : Type v} [TopologicalSpace X] [MeasurableSpace X] [TopologicalSpace Y] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {c : X × Y → ENNReal} [PolishSpace X] [BorelSpace X] [PolishSpace Y] [BorelSpace Y] (hc : LowerSemicontinuous c) : IsLUB {r : ENNReal | ∃ (φ : BoundedContinuousFunction X ℝ) (ψ : BoundedContinuousFunction Y ℝ), DualFeasible (fun (z : X × Y) => ↑(c z)) ⇑φ ⇑ψ ∧ ENNReal.ofReal (kantorovichDualValue μ ν ⇑φ ⇑ψ) = r} (transportCost c μ ν)

Kantorovich duality over bounded continuous potentials on Polish spaces. The primal transport cost of a nonnegative lower-semicontinuous cost is the least upper bound, in ℝ≥0∞, of the positive parts of the values of dual-feasible pairs of bounded continuous functions. Both the cost and the common value may be infinite.

The bounded continuous pairs form a smaller class than the integrable ones of TauCeti.isLUB_ofReal_kantorovichDualValue_integrable_of_lowerSemicontinuous, so this is the stronger statement. Bounded continuous potentials are the ones that can be tested against weakly convergent families of measures.