Finite maximal coupling

Place the common mass min(p,q) on the diagonal and couple the two remaining nonnegative weights by their product divided by their common total mass. The two residual weights have disjoint supports, so the residual coupling is entirely off the diagonal. Zero residual mass is covered by the zero-mass cancellation lemma.

theorem Algebraic.Cutwidth.Extractor.Internal.exists_maximal_coupling {α : Type u_1} [Fintype α] {p q : α → ℝ} (hp : IsProbabilityWeight p) (hq : IsProbabilityWeight q) : ∃ (r : α × α → ℝ), IsProbabilityWeight r ∧ (∀ (a : α), ∑ b : α, r (a, b) = p a) ∧ (∀ (b : α), ∑ a : α, r (a, b) = q b) ∧ ∑ z : α × α with z.1 ≠ z.2, r z = weightDist p q