Kantorovich duality

DefinitionCoupling of two probability measures#✓fully proved

Let \(\mu\) and \(\nu\) be probability measures on measurable spaces \(X\) and \(Y\). A probability measure \(\pi\) on \(X \times Y\) is a coupling of \(\mu\) and \(\nu\) when its marginals are \(\mu\) and \(\nu\), that is, when the pushforward of \(\pi\) under the projection \(X \times Y \to X\) is \(\mu\) and the pushforward of \(\pi\) under the projection \(X \times Y \to Y\) is \(\nu\).

def IsCoupling {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
    (μ : ProbabilityMeasure X) (ν : ProbabilityMeasure Y)
    (π : ProbabilityMeasure (X × Y)) : Prop :=
  (μ : Measure X) = (π : Measure (X × Y)).map Prod.fst ∧
    (ν : Measure Y) = (π : Measure (X × Y)).map Prod.snd

Used by 2

Used byKantorovich duality on compact metric spaces · Values of the transport cost over couplings

DefinitionValues of the transport cost over couplings#✓fully proved

Let \(\mu\) and \(\nu\) be probability measures on measurable spaces \(X\) and \(Y\), and let \(c : X \times Y \to \mathbb{R}\). The primal values of \(c\) for \(\mu\) and \(\nu\) form the set of real numbers \(\int c \, d\pi\), where \(\pi\) ranges over the couplings of \(\mu\) and \(\nu\).

Here \(\int c \, d\pi\) is the Bochner integral, which is \(0\) when \(c\) is not \(\pi\)-integrable.

def primalValues {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
    (μ : ProbabilityMeasure X) (ν : ProbabilityMeasure Y)
    (c : X × Y → ℝ) : Set ℝ :=
  {r : ℝ | ∃ π : ProbabilityMeasure (X × Y),
    IsCoupling μ ν π ∧ r = ∫ p, c p ∂(π : Measure (X × Y))}

Uses 1 · Used by 1

Statement usesCoupling of two probability measures

Used byKantorovich duality on compact metric spaces

DefinitionDual feasible pair of potentials#✓fully proved

Let \(X\) and \(Y\) be topological spaces and let \(c : X \times Y \to \mathbb{R}\). A pair of functions \(\varphi : X \to \mathbb{R}\) and \(\psi : Y \to \mathbb{R}\) is dual feasible for the cost \(c\) when \(\varphi\) and \(\psi\) are continuous and \(\varphi(x) + \psi(y) \le c(x, y)\) for all \(x \in X\) and \(y \in Y\).

def DualFeasible {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    (c : X × Y → ℝ) (φ : X → ℝ) (ψ : Y → ℝ) : Prop :=
  Continuous φ ∧ Continuous ψ ∧ ∀ x y, φ x + ψ y ≤ c (x, y)

Used by 1

Used byKantorovich duality on compact metric spaces

TheoremKantorovich duality on compact metric spaces#✓fully proved

Let \(X\) and \(Y\) be nonempty compact metric spaces, each carrying its Borel \(\sigma\)-algebra, let \(\mu\) and \(\nu\) be probability measures on \(X\) and \(Y\), and let \(c : X \times Y \to \mathbb{R}\) be continuous. Then the infimum of \(\int c \, d\pi\) over all couplings \(\pi\) of \(\mu\) and \(\nu\) equals the supremum of \(\int \varphi \, d\mu + \int \psi \, d\nu\) over all pairs of continuous functions \(\varphi : X \to \mathbb{R}\) and \(\psi : Y \to \mathbb{R}\) such that \(\varphi(x) + \psi(y) \le c(x, y)\) for all \(x \in X\) and \(y \in Y\).

theorem kantorovich_duality_compact
    {X Y : Type*}
    [MetricSpace X] [MetricSpace Y]
    [CompactSpace X] [CompactSpace Y]
    [Nonempty X] [Nonempty Y]
    [MeasurableSpace X] [MeasurableSpace Y]
    [BorelSpace X] [BorelSpace Y]
    (μ : ProbabilityMeasure X) (ν : ProbabilityMeasure Y)
    (c : X × Y → ℝ) (hc : Continuous c) :
    sInf (primalValues μ ν c) =
    sSup {r : ℝ | ∃ φ : X → ℝ, ∃ ψ : Y → ℝ,
      DualFeasible c φ ψ ∧
      r = (∫ x, φ x ∂(μ : Measure X)) + ∫ y, ψ y ∂(ν : Measure Y)}

Sources

• L. V. Kantorovich, On the Translocation of Masses (1942); English transl. J. Math. Sci. 133 (2006), 1381-1382, DOI 10.1007/S10958-006-0049-2; modern ref C. Villani, Topics in Optimal Transportation (2003).

Uses 3

Statement usesDual feasible pair of potentials · Values of the transport cost over couplings

Proof usesCoupling of two probability measures

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.