Projecting the lifted coupling to a repaired joint law

The old and new pairs share the second coordinate. Their probability of disagreement bounds the distance of their joint laws. Conversely, marginalization cannot increase distance, so the joint repair costs exactly the distance of the prescribed first marginal.

theorem Algebraic.Cutwidth.Extractor.Internal.exists_joint_marginal_replacement {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {p : α × β → ℝ} {q : α → ℝ} (hp : IsProbabilityWeight p) (hq : IsProbabilityWeight q) : ∃ (p' : α × β → ℝ), IsProbabilityWeight p' ∧ firstWeight p' = q ∧ (∀ (b : β), ∑ a : α, p' (a, b) = ∑ a : α, p (a, b)) ∧ weightDist p p' = weightDist (firstWeight p) q