Proof of Proposition 2.1, p. 373 — Birkhoff extreme points in the book's scaling

Proved

CompOT.Assignment.birkhoff_extreme_points

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

birkhoffextreme-pointsoptimal-transportp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1

Let $n>0$ and let $u$ be the uniform histogram with mass $1/n$ at each index. The extreme points of the coupling polytope $U(u,u)$ are exactly the scaled permutation matrices:

\operatorname{Ext}(U(u,u))=\{P_\sigma:\sigma\in\operatorname{Perm}(n)\}.

This specializes Birkhoff's theorem to the normalization used for probability histograms in the matching proposition.

Formalization Note Mathlib's doubly stochastic matrices have row and column sums $1$ ; the statement here uses the book's row and column sums $1/n$ .

Preamble

import Mathlib
import Definitions.Def_CompOT_Assignment_Defs

Formal statement

namespace CompOT.Assignment

theorem birkhoff_extreme_points {n : ℕ} (hn : 0 < n) :
    Set.extremePoints ℝ (couplings (uniform n) (uniform n)) =
      {P : Matrix (Fin n) (Fin n) ℝ | ∃ σ : Equiv.Perm (Fin n), P = permCoupling σ} := by sorry

end CompOT.Assignment

Source

Peyré & Cuturi, Computational Optimal Transport (FnT ML 2019), proof of Proposition 2.1, p. 373, first sentence

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