§2.3, p. 371 — transposing a coupling swaps its marginals

Proved

CompOT.Assignment.coupling_transpose

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

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

A matrix $P$ transports the histogram $a$ to $b$ exactly when its transpose transports $b$ to $a$ :

P\in U(a,b)\quad\Longleftrightarrow\quad P^{\mathsf T}\in U(b,a).

This symmetry is useful when comparing transport problems with their source and target roles reversed.

Preamble

import Mathlib
import Definitions.Def_CompOT_Assignment_Defs

Formal statement

namespace CompOT.Assignment

theorem coupling_transpose {n m : ℕ} (a : Fin n → ℝ) (b : Fin m → ℝ)
    (P : Matrix (Fin n) (Fin m) ℝ) :
    P ∈ couplings a b ↔ P.transpose ∈ couplings b a := by sorry

end CompOT.Assignment

Source

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

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