§2.3, p. 372 — every scaled permutation matrix is a uniform coupling

Proved

CompOT.Assignment.perm_feasible

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

couplingoptimal-transportp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1permutation

Let $n>0$ and let $u$ be the histogram with every entry equal to $1/n$ . For every permutation $\sigma$ of $n$ indices, its scaled permutation matrix has both marginals equal to $u$ :

P_\sigma\in U(u,u).

Thus each feasible assignment supplies a feasible point of the Kantorovich relaxation.

Formalization Note The printed text immediately after (2.12) gives the row and column sums as $\mathbf1_n$ ; the displayed definition of $P_\sigma$ makes them $\mathbf1_n/n$ , as encoded here.

Preamble

import Mathlib
import Definitions.Def_CompOT_Assignment_Defs

Formal statement

namespace CompOT.Assignment

theorem perm_feasible {n : ℕ} (hn : 0 < n)
    (σ : Equiv.Perm (Fin n)) :
    permCoupling σ ∈ couplings (uniform n) (uniform n) := by sorry

end CompOT.Assignment

Source

Peyré & Cuturi, Computational Optimal Transport (FnT ML 2019), §2.3, p. 372, paragraph after (2.12)

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