Proposition 2.1, pp. 372–373 — a permutation coupling optimizes the uniform Kantorovich problem

Proved

CompOT.Assignment.proposition_2_1

by mikedeng1 · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

assignmentbirkhoffoptimal-transportp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1

Let $n>0$ , let $C$ be any real $n\times n$ cost matrix, and let $u$ be the histogram with entries $1/n$ . There is a permutation $\sigma^\star$ such that its scaled permutation coupling is optimal among all couplings in $U(u,u)$ , and $\sigma^\star$ minimizes the assignment objective among all permutations:

P_{\sigma^\star}\in U(u,u),\qquad \langle C,P_{\sigma^\star}\rangle\le\langle C,Q\rangle\quad(\forall Q\in U(u,u)),\qquad A_C(\sigma^\star)\le A_C(\tau)\quad(\forall\tau\in\operatorname{Perm}(n)).

Consequently, the Kantorovich relaxation of the uniform optimal assignment problem is tight.

Formalization Note The condition $n>0$ excludes the empty index set and division by zero. The cost is allowed to be negative; the book imposes no sign restriction on $C$ for this result. The minimization over couplings ranges over every feasible matrix, not only permutation matrices.

Preamble

import Mathlib
import Definitions.Def_CompOT_Assignment_Defs

Formal statement

namespace CompOT.Assignment

theorem proposition_2_1 {n : ℕ} (hn : 0 < n)
    (C : Matrix (Fin n) (Fin n) ℝ) :
    ∃ σ : Equiv.Perm (Fin n),
      IsOptimalCoupling C (uniform n) (uniform n) (permCoupling σ) ∧
      ∀ τ : Equiv.Perm (Fin n), assignmentCost C σ ≤ assignmentCost C τ := by sorry

end CompOT.Assignment

Source

Peyré & Cuturi, Computational Optimal Transport (FnT ML 2019), Proposition 2.1, pp. 372–373

Human review

Endorsed by Shuze Chen · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph