§2.3, p. 372 — the cost of a scaled permutation coupling is the assignment objective

Proved

CompOT.Assignment.assignment_cost

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

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

Let $n>0$ , let $C$ be an $n\times n$ cost matrix, and let $\sigma$ be a permutation. The scaled permutation matrix $P_\sigma$ has transport cost equal to the assignment objective:

\langle C,P_\sigma\rangle=\frac1n\sum_{i=1}^{n} C_{i,\sigma(i)}=A_C(\sigma).

This identifies the objective of the combinatorial assignment problem with the linear objective used in its transport relaxation.

Formalization Note The condition $n>0$ excludes division by zero; Fin n indexes the same $n$ entries starting at zero.

Preamble

import Mathlib
import Definitions.Def_CompOT_Assignment_Defs

Formal statement

namespace CompOT.Assignment

theorem assignment_cost {n : ℕ} (hn : 0 < n)
    (C : Matrix (Fin n) (Fin n) ℝ) (σ : Equiv.Perm (Fin n)) :
    frob C (permCoupling σ) = assignmentCost C σ := by sorry

end CompOT.Assignment

Source

Peyré & Cuturi, Computational Optimal Transport (FnT ML 2019), §2.3, p. 372, display following (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