Kantorovich–Rubinstein duality

For probability measures μ and ν with finite first moments on a separable metric space whose measurable structure is standard Borel, the 1-Wasserstein distance is the largest difference of expectations of a 1-Lipschitz real function:

W₁ (μ, ν) = ⨆ (f : X → ℝ) (_ : LipschitzWith 1 f), ENNReal.ofReal (∫ f ∂μ - ∫ f ∂ν).

This is the Kantorovich duality for the cost edist, in the special form that a distance cost allows: a single potential f replaces the pair (φ, ψ), with ψ = -f. It turns W₁ estimates into estimates on the expectations of Lipschitz test functions, and conversely. Since only the differences of expectations enter, the supremum may be restricted to the functions vanishing at a prescribed basepoint.

The inequality bounding a difference of expectations by W₁ (weak duality) holds on an arbitrary extended pseudometric space, for arbitrary measures, as soon as the test function is integrable. On a compact pseudometric space the full formula holds for all probability measures, with no moment hypothesis. In general, the finite-moment hypotheses make every 1-Lipschitz function integrable (TauCeti.HasFiniteMoment.integrable_of_lipschitzWith), so that the Bochner integrals on the right are the honest expectations; under them both sides are finite.

For finite measures of equal mass on a Polish pseudometric space and R ≥ 0, transport with cost min (dist x y) (2 * R) is the greatest difference of integrals over 1-Lipschitz real functions bounded in absolute value by R. No moment assumption is needed. For probability measures and R = 1, this gives the bounded-Lipschitz (Fortet–Mourier) convention with separate Lipschitz and supremum-norm bounds of one, corresponding to a primal cap of two. The bounded variant uses dual attainment and centers a conjugate potential whose oscillation is at most 2 * R; finite measures reduce to probability measures by normalization.

Main statements

• TauCeti.ofReal_integral_sub_integral_le_wassersteinEDist_one — the difference of expectations of an integrable 1-Lipschitz function is at most W₁, on an arbitrary extended pseudometric space;
• TauCeti.wassersteinEDist_one_eq_iSup_of_compactSpace — Kantorovich–Rubinstein duality for probability measures on a compact pseudometric space;
• TauCeti.wassersteinEDist_one_eq_iSup — Kantorovich–Rubinstein duality for probability measures with finite first moments on a second-countable pseudometric space with a standard Borel measurable structure, in particular on a Polish metric space;
• TauCeti.wassersteinEDist_one_eq_iSup_apply_eq_zero — the same formula with the test functions normalized to vanish at a basepoint;
• TauCeti.exists_lipschitzWith_norm_le_integral_sub_integral_eq_transportCost_truncated_dist — bounded-Lipschitz dual attainment for finite measures of equal mass on a Polish space;
• TauCeti.transportCost_truncated_dist_eq_iSup and TauCeti.transportCost_truncated_dist_eq_iSup_abs — the signed and absolute supremum formulas for the distance truncated at 2 * R.

References

• L. V. Kantorovich and G. S. Rubinstein, On a space of completely additive functions, Vestnik Leningrad. Univ. 13 (1958), no. 7, 52--59.
• C. Villani, Topics in Optimal Transportation, Graduate Studies in Mathematics 58, AMS 2003, Theorem 1.14.
• C. Villani, Optimal Transport: Old and New, Grundlehren 338, Springer 2009, Particular Case 5.16. For the bounded-Lipschitz variant, the ground distance is truncated at 2 * R.

theorem TauCeti.ofReal_integral_sub_integral_le_wassersteinEDist_one {X : Type u} [MeasurableSpace X] {μ ν : MeasureTheory.Measure X} [PseudoEMetricSpace X] {f : X → ℝ} (hf : LipschitzWith 1 f) (hμ : MeasureTheory.Integrable f μ) (hν : MeasureTheory.Integrable f ν) : ENNReal.ofReal (∫ (x : X), f x ∂μ - ∫ (x : X), f x ∂ν) ≤ wassersteinEDist 1 μ ν

Kantorovich–Rubinstein weak duality. The difference of the expectations of an integrable 1-Lipschitz real function under two measures is at most their 1-Wasserstein distance. No measurability of the ground distance and no finiteness of the measures is needed.

theorem TauCeti.wassersteinEDist_one_eq_iSup_of_compactSpace {X : Type u} [MeasurableSpace X] {μ ν : MeasureTheory.Measure X} [PseudoMetricSpace X] [CompactSpace X] [OpensMeasurableSpace X] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : wassersteinEDist 1 μ ν = ⨆ (f : X → ℝ), ⨆ (_ : LipschitzWith 1 f), ENNReal.ofReal (∫ (x : X), f x ∂μ - ∫ (x : X), f x ∂ν)

Kantorovich–Rubinstein duality on a compact space. For probability measures on a compact pseudometric space whose open sets are measurable, the 1-Wasserstein distance is the supremum of the differences of expectations of the 1-Lipschitz real functions.

theorem TauCeti.wassersteinEDist_one_eq_iSup {X : Type u} [MeasurableSpace X] {μ ν : MeasureTheory.Measure X} [PseudoMetricSpace X] [OpensMeasurableSpace X] [SecondCountableTopology X] [StandardBorelSpace X] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hμ : HasFiniteMoment 1 μ) (hν : HasFiniteMoment 1 ν) : wassersteinEDist 1 μ ν = ⨆ (f : X → ℝ), ⨆ (_ : LipschitzWith 1 f), ENNReal.ofReal (∫ (x : X), f x ∂μ - ∫ (x : X), f x ∂ν)

Kantorovich–Rubinstein duality. For probability measures with finite first moments on a second-countable pseudometric space whose measurable structure is standard Borel and contains the open sets — in particular on a Polish metric space with its Borel σ-algebra — the 1-Wasserstein distance is the supremum of the differences of expectations of the 1-Lipschitz real functions.

theorem TauCeti.wassersteinEDist_one_eq_iSup_apply_eq_zero {X : Type u} [MeasurableSpace X] {μ ν : MeasureTheory.Measure X} [PseudoMetricSpace X] [OpensMeasurableSpace X] [SecondCountableTopology X] [StandardBorelSpace X] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hμ : HasFiniteMoment 1 μ) (hν : HasFiniteMoment 1 ν) (x₀ : X) : wassersteinEDist 1 μ ν = ⨆ (f : X → ℝ), ⨆ (_ : LipschitzWith 1 f), ⨆ (_ : f x₀ = 0), ENNReal.ofReal (∫ (x : X), f x ∂μ - ∫ (x : X), f x ∂ν)

Kantorovich–Rubinstein duality, normalized at a basepoint. Under the hypotheses of TauCeti.wassersteinEDist_one_eq_iSup, the supremum may be taken over the 1-Lipschitz real functions vanishing at any prescribed point x₀: subtracting a constant does not change a difference of expectations under two probability measures.

theorem TauCeti.ofReal_integral_sub_integral_le_transportCost_truncated_dist {X : Type u} [MeasurableSpace X] {μ ν : MeasureTheory.Measure X} [PseudoMetricSpace X] {R : ℝ} [OpensMeasurableSpace X] [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {f : X → ℝ} (hf : LipschitzWith 1 f) (hfb : ∀ (x : X), ‖f x‖ ≤ R) : ENNReal.ofReal (∫ (x : X), f x ∂μ - ∫ (x : X), f x ∂ν) ≤ transportCost (fun (z : X × X) => ENNReal.ofReal (min (dist z.1 z.2) (2 * R))) μ ν

Bounded-Lipschitz weak duality for the truncated distance cost. The bound R on each potential produces the cap 2 * R on the cost.

theorem TauCeti.exists_lipschitzWith_norm_le_integral_sub_integral_eq_transportCost_truncated_dist {X : Type u} [MeasurableSpace X] {μ ν : MeasureTheory.Measure X} [PseudoMetricSpace X] {R : ℝ} [PolishSpace X] [BorelSpace X] [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hR : 0 ≤ R) (hmass : μ Set.univ = ν Set.univ) : ∃ (f : X → ℝ), LipschitzWith 1 f ∧ (∀ (x : X), ‖f x‖ ≤ R) ∧ ENNReal.ofReal (∫ (x : X), f x ∂μ - ∫ (x : X), f x ∂ν) = transportCost (fun (z : X × X) => ENNReal.ofReal (min (dist z.1 z.2) (2 * R))) μ ν

Transport with truncated distance admits a maximizing 1-Lipschitz test function bounded by half the cap, for finite measures of equal mass. No first-moment assumption is needed, and zero mass and the zero-cap case are included.

theorem TauCeti.isGreatest_ofReal_integral_sub_integral_boundedLipschitz {X : Type u} [MeasurableSpace X] {μ ν : MeasureTheory.Measure X} [PseudoMetricSpace X] {R : ℝ} [PolishSpace X] [BorelSpace X] [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hR : 0 ≤ R) (hmass : μ Set.univ = ν Set.univ) : IsGreatest {r : ENNReal | ∃ (f : X → ℝ), LipschitzWith 1 f ∧ (∀ (x : X), ‖f x‖ ≤ R) ∧ ENNReal.ofReal (∫ (x : X), f x ∂μ - ∫ (x : X), f x ∂ν) = r} (transportCost (fun (z : X × X) => ENNReal.ofReal (min (dist z.1 z.2) (2 * R))) μ ν)

Bounded-Lipschitz Kantorovich–Rubinstein duality with attainment. The cost capped at 2 * R is the greatest difference of integrals of a 1-Lipschitz function bounded by R, for finite measures of equal mass. Both constraints are separate; this is the maximum-norm convention, not their sum.

theorem TauCeti.transportCost_truncated_dist_eq_iSup {X : Type u} [MeasurableSpace X] {μ ν : MeasureTheory.Measure X} [PseudoMetricSpace X] {R : ℝ} [PolishSpace X] [BorelSpace X] [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hR : 0 ≤ R) (hmass : μ Set.univ = ν Set.univ) : transportCost (fun (z : X × X) => ENNReal.ofReal (min (dist z.1 z.2) (2 * R))) μ ν = ⨆ (f : X → ℝ), ⨆ (_ : LipschitzWith 1 f), ⨆ (_ : ∀ (x : X), ‖f x‖ ≤ R), ENNReal.ofReal (∫ (x : X), f x ∂μ - ∫ (x : X), f x ∂ν)

Bounded-Lipschitz duality in supremum form. A uniform bound R on the test functions corresponds to truncation of the ground distance at 2 * R, for finite measures of equal mass.

theorem TauCeti.transportCost_truncated_dist_eq_iSup_abs {X : Type u} [MeasurableSpace X] {μ ν : MeasureTheory.Measure X} [PseudoMetricSpace X] {R : ℝ} [PolishSpace X] [BorelSpace X] [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hR : 0 ≤ R) (hmass : μ Set.univ = ν Set.univ) : transportCost (fun (z : X × X) => ENNReal.ofReal (min (dist z.1 z.2) (2 * R))) μ ν = ⨆ (f : X → ℝ), ⨆ (_ : LipschitzWith 1 f), ⨆ (_ : ∀ (x : X), ‖f x‖ ≤ R), ENNReal.ofReal |∫ (x : X), f x ∂μ - ∫ (x : X), f x ∂ν|

The absolute-difference form of bounded-Lipschitz duality for finite measures of equal mass. The test class is closed under negation, so its signed and absolute suprema coincide.