Kantorovich duality on finite spaces

On finite source and target spaces the transport problem is a linear program: minimise ∑ i, ∑ j, c (i, j) * A i j over the transportation matrices A with prescribed marginals μ and ν. Its dual maximises ∑ i, μ i * φ i + ∑ j, ν j * ψ j over the pairs of real potentials satisfying φ i + ψ j ≤ c (i, j).

This file proves that the two problems have the same value, that both are attained, and that a feasible pair of a plan and a potential pair is simultaneously optimal exactly when the plan is concentrated on the contact set of the potentials.

Unlike the rest of the theory the cost here is an honest real number, negative values included, because a linear program has no reason to be nonnegative. Consequently the primal value is measured by TauCeti.TransportMatrix.cost rather than by TauCeti.transportCost, whose ℝ≥0∞-valued lintegral cannot see cancellation. The two marginal integrals of the dual are likewise packaged as TauCeti.finiteDualValue, which asks for no measurable structure on the two finite spaces; TauCeti.finiteDualValue_eq_kantorovichDualValue and TauCeti.TransportMatrix.cost_eq_integral identify both with the measure-level definitions as soon as one is available. The feasibility constraint used here is likewise the real form of the canonical TauCeti.DualFeasible, by TauCeti.dualFeasible_ofReal_iff whenever the cost is nonnegative.

The hard half of the duality is the minimax theorem: the Lagrangian ∑ q, (c q - φ q.1 - ψ q.2) * f q + (∑ i, μ i * φ i + ∑ j, ν j * ψ j) is affine in the plan f, which ranges over the compact convex standard simplex, and affine in the potentials, which range over the whole of (ι → ℝ) × (κ → ℝ). Sion's minimax theorem exchanges the two extrema. Taking the potentials unbounded is what forces the extended-real codomain: the inner supremum is ⊤ at a plan whose marginals are wrong.

Main definitions

• TauCeti.finiteDualValue — the value of a pair of potentials against two probability mass functions. The primal value is TauCeti.TransportMatrix.cost, which belongs to the transportation-matrix file.

Main statements

• TauCeti.TransportMatrix.finiteDualValue_le_cost — weak duality;
• TauCeti.TransportMatrix.exists_forall_cost_le and TauCeti.exists_forall_finiteDualValue_le — primal and dual attainment;
• TauCeti.exists_cost_eq_finiteDualValue — strong duality, together with both attainments;
• TauCeti.exists_isLeast_cost_isGreatest_finiteDualValue — the same statement read as an optimal value shared by the two problems;
• TauCeti.TransportMatrix.cost_eq_finiteDualValue_iff — complementary slackness;
• TauCeti.TransportMatrix.forall_cost_le_and_forall_finiteDualValue_le_iff — the optimality certificate: a plan and a feasible pair are optimal for their problems exactly when the plan lives on the contact set of the pair, and TauCeti.TransportMatrix.forall_cost_le_and_forall_finiteDualValue_le_iff_mem_contactSet — the same certificate read through TauCeti.contactSet;
• TauCeti.TransportMatrix.forall_cost_le_iff_exists_forall_add_le_and_support_subset_contactSet — existential complementary slackness, with finite dual attainment supplying the potentials;
• TauCeti.finiteDualValue_eq_kantorovichDualValue and TauCeti.TransportMatrix.cost_eq_integral — the bridges to the measure-level dual and primal values.

References

• C. Villani, Topics in Optimal Transportation, Graduate Studies in Mathematics 58, 2003, §1.1.2, for the finite duality and complementary slackness.
• M. Sion, On general minimax theorems, Pacific J. Math. 8 (1958), 171--176.
• Mathlib.Topology.Sion, formalized by Antoine Chambert-Loir and Anatole Dedecker.

This is Layer 2, item 3 of the optimal-transport roadmap.

def TauCeti.finiteDualValue {ι : Type u} {κ : Type v} [Fintype ι] [Fintype κ] (μ : PMF ι) (ν : PMF κ) (φ : ι → ℝ) (ψ : κ → ℝ) : ℝ

The value of a pair of Kantorovich potentials against two probability mass functions on finite types: the sum of the two marginal expectations.

theorem TauCeti.finiteDualValue_def {ι : Type u} {κ : Type v} [Fintype ι] [Fintype κ] (μ : PMF ι) (ν : PMF κ) (φ : ι → ℝ) (ψ : κ → ℝ) : finiteDualValue μ ν φ ψ = ∑ i : ι, (μ i).toReal * φ i + ∑ j : κ, (ν j).toReal * ψ j

The defining formula for the dual value. The body of the definition is not exposed, so this is the lemma downstream modules should rewrite with.

theorem TauCeti.finiteDualValue_add_const_add_const {ι : Type u} {κ : Type v} [Fintype ι] [Fintype κ] (μ : PMF ι) (ν : PMF κ) (φ : ι → ℝ) (ψ : κ → ℝ) (a b : ℝ) : (finiteDualValue μ ν (fun (i : ι) => φ i + a) fun (j : κ) => ψ j + b) = finiteDualValue μ ν φ ψ + a + b

Shifting the two potentials by two constants shifts the dual value by their sum: both marginals have total mass one.

theorem TauCeti.finiteDualValue_add_const {ι : Type u} {κ : Type v} [Fintype ι] [Fintype κ] (μ : PMF ι) (ν : PMF κ) (φ : ι → ℝ) (ψ : κ → ℝ) (a : ℝ) : finiteDualValue μ ν (fun (i : ι) => φ i + a) ψ = finiteDualValue μ ν φ ψ + a

Adding a constant to the first potential adds it to the dual value: the first marginal has total mass one.

theorem TauCeti.finiteDualValue_add_const_sub_const {ι : Type u} {κ : Type v} [Fintype ι] [Fintype κ] (μ : PMF ι) (ν : PMF κ) (φ : ι → ℝ) (ψ : κ → ℝ) (a : ℝ) : (finiteDualValue μ ν (fun (i : ι) => φ i + a) fun (j : κ) => ψ j - a) = finiteDualValue μ ν φ ψ

The dual value is unchanged by the opposite additive shifts of the two potentials, which is the normalisation freedom of the dual problem: both marginals have total mass one.

theorem TauCeti.finiteDualValue_mono {ι : Type u} {κ : Type v} [Fintype ι] [Fintype κ] {μ : PMF ι} {ν : PMF κ} {φ φ' : ι → ℝ} {ψ ψ' : κ → ℝ} (hφ : ∀ (i : ι), φ i ≤ φ' i) (hψ : ∀ (j : κ), ψ j ≤ ψ' j) : finiteDualValue μ ν φ ψ ≤ finiteDualValue μ ν φ' ψ'

The dual value is monotone in both potentials.

The standard-simplex picture

Convexity and compactness arguments are run on real-valued plans, which form a closed subset of the standard simplex on the product.

The algebraic core

The difference between the cost of a plan and the value of a pair of potentials is the total mass the plan puts on the pointwise gap c (i, j) - φ i - ψ j.

theorem TauCeti.TransportMatrix.cost_sub_finiteDualValue {ι : Type u} {κ : Type v} [Fintype ι] [Fintype κ] {μ : PMF ι} {ν : PMF κ} (A : TransportMatrix μ ν) (c : ι × κ → ℝ) (φ : ι → ℝ) (ψ : κ → ℝ) : cost c A - finiteDualValue μ ν φ ψ = ∑ q : ι × κ, (c q - φ q.1 - ψ q.2) * A.toRealFun q

The cost of a plan exceeds the value of a pair of potentials by the mass the plan puts on the pointwise gap.

theorem TauCeti.TransportMatrix.finiteDualValue_le_cost {ι : Type u} {κ : Type v} [Fintype ι] [Fintype κ] {μ : PMF ι} {ν : PMF κ} {c : ι × κ → ℝ} {φ : ι → ℝ} {ψ : κ → ℝ} (A : TransportMatrix μ ν) (h : ∀ (i : ι) (j : κ), φ i + ψ j ≤ c (i, j)) : finiteDualValue μ ν φ ψ ≤ cost c A

Weak duality on finite spaces: every dual-feasible pair of potentials is worth at most the cost of every transport plan.

theorem TauCeti.TransportMatrix.cost_eq_finiteDualValue_iff {ι : Type u} {κ : Type v} [Fintype ι] [Fintype κ] {μ : PMF ι} {ν : PMF κ} {c : ι × κ → ℝ} {φ : ι → ℝ} {ψ : κ → ℝ} (A : TransportMatrix μ ν) (h : ∀ (i : ι) (j : κ), φ i + ψ j ≤ c (i, j)) : cost c A = finiteDualValue μ ν φ ψ ↔ ∀ (i : ι) (j : κ), A.matrix i j ≠ 0 → φ i + ψ j = c (i, j)

Complementary slackness: a transport plan and a dual-feasible pair of potentials have the same value exactly when the plan is concentrated on the contact set of the potentials.

Primal attainment

theorem TauCeti.isCompact_realPlans {ι : Type u} {κ : Type v} [Fintype ι] [Fintype κ] {μ : PMF ι} {ν : PMF κ} : IsCompact (RealPlans μ ν)

Real transportation plans with prescribed finite marginals form a compact set. This permits continuous auxiliary objectives to select a plan among the minimizers of a transport cost.

theorem TauCeti.realPlans_nonempty {ι : Type u} {κ : Type v} [Fintype ι] [Fintype κ] (μ : PMF ι) (ν : PMF κ) : (RealPlans μ ν).Nonempty

The real plans with prescribed marginals form a nonempty set: the independent plan is one.

theorem TauCeti.TransportMatrix.exists_forall_cost_le {ι : Type u} {κ : Type v} [Fintype ι] [Fintype κ] (c : ι × κ → ℝ) (μ : PMF ι) (ν : PMF κ) : ∃ (A : TransportMatrix μ ν), ∀ (B : TransportMatrix μ ν), cost c A ≤ cost c B

Primal attainment: on finite spaces the transport problem has a minimiser.

Dual attainment

The dual problem is invariant under the opposite shifts of the two potentials, so its supremum is unchanged by restricting to potentials normalised at a base point. Two infimal c-transforms turn an arbitrary feasible pair into a normalised one with at least the same value, and normalised pairs are confined to a box.

theorem TauCeti.exists_forall_finiteDualValue_le {ι : Type u} {κ : Type v} [Fintype ι] [Fintype κ] (c : ι × κ → ℝ) (μ : PMF ι) (ν : PMF κ) : ∃ (φ : ι → ℝ) (ψ : κ → ℝ), (∀ (i : ι) (j : κ), φ i + ψ j ≤ c (i, j)) ∧ ∀ (φ' : ι → ℝ) (ψ' : κ → ℝ), (∀ (i : ι) (j : κ), φ' i + ψ' j ≤ c (i, j)) → finiteDualValue μ ν φ' ψ' ≤ finiteDualValue μ ν φ ψ

Dual attainment: on finite spaces the dual problem has a maximiser.

Strong duality

The Lagrangian of the transport problem is affine and continuous in the plan, which ranges over the compact convex standard simplex, and affine and continuous in the potentials, which range over the whole of (ι → ℝ) × (κ → ℝ). Sion's minimax theorem exchanges the two extrema. The inner supremum is ⊤ at a plan with the wrong marginals, whence the extended-real codomain.

theorem TauCeti.exists_cost_eq_finiteDualValue {ι : Type u} {κ : Type v} [Fintype ι] [Fintype κ] (c : ι × κ → ℝ) (μ : PMF ι) (ν : PMF κ) : ∃ (A : TransportMatrix μ ν) (φ : ι → ℝ) (ψ : κ → ℝ), (∀ (B : TransportMatrix μ ν), TransportMatrix.cost c A ≤ TransportMatrix.cost c B) ∧ (∀ (i : ι) (j : κ), φ i + ψ j ≤ c (i, j)) ∧ TransportMatrix.cost c A = finiteDualValue μ ν φ ψ

Kantorovich duality on finite spaces: the transport problem and its dual have the same value, and both are attained.

theorem TauCeti.exists_isLeast_cost_isGreatest_finiteDualValue {ι : Type u} {κ : Type v} [Fintype ι] [Fintype κ] (c : ι × κ → ℝ) (μ : PMF ι) (ν : PMF κ) : ∃ (V : ℝ), IsLeast {r : ℝ | ∃ (A : TransportMatrix μ ν), TransportMatrix.cost c A = r} V ∧ IsGreatest {r : ℝ | ∃ (φ : ι → ℝ) (ψ : κ → ℝ), (∀ (i : ι) (j : κ), φ i + ψ j ≤ c (i, j)) ∧ finiteDualValue μ ν φ ψ = r} V

The common optimal value of the two problems: the transport problem attains its infimum and the dual problem attains its supremum, at the same real number.

theorem TauCeti.TransportMatrix.forall_cost_le_and_forall_finiteDualValue_le_iff {ι : Type u} {κ : Type v} [Fintype ι] [Fintype κ] {μ : PMF ι} {ν : PMF κ} {c : ι × κ → ℝ} {φ : ι → ℝ} {ψ : κ → ℝ} (A : TransportMatrix μ ν) (hfeas : ∀ (i : ι) (j : κ), φ i + ψ j ≤ c (i, j)) : ((∀ (B : TransportMatrix μ ν), cost c A ≤ cost c B) ∧ ∀ (φ' : ι → ℝ) (ψ' : κ → ℝ), (∀ (i : ι) (j : κ), φ' i + ψ' j ≤ c (i, j)) → finiteDualValue μ ν φ' ψ' ≤ finiteDualValue μ ν φ ψ) ↔ ∀ (i : ι) (j : κ), A.matrix i j ≠ 0 → φ i + ψ j = c (i, j)

The optimality certificate. A transport plan and a dual-feasible pair of potentials are optimal for their respective problems exactly when the plan is concentrated on the contact set of the pair.

theorem TauCeti.TransportMatrix.forall_cost_le_and_forall_finiteDualValue_le_iff_mem_contactSet {ι : Type u} {κ : Type v} [Fintype ι] [Fintype κ] {μ : PMF ι} {ν : PMF κ} {c : ι × κ → ℝ} {φ : ι → ℝ} {ψ : κ → ℝ} (A : TransportMatrix μ ν) (hfeas : ∀ (i : ι) (j : κ), φ i + ψ j ≤ c (i, j)) : ((∀ (B : TransportMatrix μ ν), cost c A ≤ cost c B) ∧ ∀ (φ' : ι → ℝ) (ψ' : κ → ℝ), (∀ (i : ι) (j : κ), φ' i + ψ' j ≤ c (i, j)) → finiteDualValue μ ν φ' ψ' ≤ finiteDualValue μ ν φ ψ) ↔ ∀ (i : ι) (j : κ), A.matrix i j ≠ 0 → (i, j) ∈ contactSet c (fun (i : ι) => ↑(φ i)) fun (j : κ) => ↑(ψ j)

The optimality certificate, through the contact set. The pointwise equality of TauCeti.TransportMatrix.forall_cost_le_and_forall_finiteDualValue_le_iff says exactly that every pair carrying mass lies in TauCeti.contactSet of the coerced potentials.

theorem TauCeti.TransportMatrix.toPMF_support_subset_contactSet_coe_iff {ι : Type u} {κ : Type v} [Fintype ι] [Fintype κ] {μ : PMF ι} {ν : PMF κ} (A : TransportMatrix μ ν) (c : ι × κ → ℝ) (φ : ι → ℝ) (ψ : κ → ℝ) : (A.toPMF.support ⊆ contactSet c (fun (i : ι) => ↑(φ i)) fun (j : κ) => ↑(ψ j)) ↔ ∀ (i : ι) (j : κ), A.matrix i j ≠ 0 → φ i + ψ j = c (i, j)

Containment of the support of a transportation matrix in the contact set of real-valued potentials is the pointwise complementary-slackness condition on every nonzero entry.

theorem TauCeti.TransportMatrix.forall_cost_le_iff_exists_forall_add_le_and_support_subset_contactSet {ι : Type u} {κ : Type v} [Fintype ι] [Fintype κ] {μ : PMF ι} {ν : PMF κ} (A : TransportMatrix μ ν) (c : ι × κ → ℝ) : (∀ (B : TransportMatrix μ ν), cost c A ≤ cost c B) ↔ ∃ (φ : ι → ℝ) (ψ : κ → ℝ), (∀ (i : ι) (j : κ), φ i + ψ j ≤ c (i, j)) ∧ A.toPMF.support ⊆ contactSet c (fun (i : ι) => ↑(φ i)) fun (j : κ) => ↑(ψ j)

Existential complementary slackness for a finite transport plan. A transportation matrix minimizes a real cost exactly when there is a dual-feasible pair of potentials whose contact set contains the support of the matrix. Finite Kantorovich duality supplies the potentials, so they need not be selected in advance.

The measure-level reading

Neither the primal nor the dual value needs a measurable structure on the two finite spaces. When one is available, both agree with the measure-level definitions of the rest of the theory.

theorem TauCeti.finiteDualValue_eq_kantorovichDualValue {ι : Type u} {κ : Type v} [Fintype ι] [Fintype κ] [MeasurableSpace ι] [MeasurableSingletonClass ι] [MeasurableSpace κ] [MeasurableSingletonClass κ] (μ : PMF ι) (ν : PMF κ) (φ : ι → ℝ) (ψ : κ → ℝ) : finiteDualValue μ ν φ ψ = kantorovichDualValue μ.toMeasure ν.toMeasure φ ψ

The dual value of a pair of potentials against two probability mass functions is the Kantorovich dual value against the measures they define.

theorem TauCeti.TransportMatrix.cost_eq_integral {ι : Type u} {κ : Type v} [Fintype ι] [Fintype κ] {μ : PMF ι} {ν : PMF κ} [MeasurableSpace ι] [MeasurableSingletonClass ι] [MeasurableSpace κ] [MeasurableSingletonClass κ] (c : ι × κ → ℝ) (A : TransportMatrix μ ν) : cost c A = ∫ (q : ι × κ), c q ∂A.toPMF.toMeasure

The cost of a finite transportation matrix is the integral of the cost function against the probability measure the matrix defines.