Finite weighted Hall theorem

From finite flows to a coupling

theorem GaudisCrypt.PMF.exists_coupling_of_hall {X : Type u_3} {Y : Type u_4} (p : PMF X) (q : PMF Y) (R : X → Y → Prop) (hpq : ∀ (A : Set X), p.toOuterMeasure A ≤ q.toOuterMeasure {y : Y | ∃ x ∈ A, R x y}) : ∃ (μ : PMF (X × Y)), PMF.map Prod.fst μ = p ∧ PMF.map Prod.snd μ = q ∧ ∀ w ∈ μ.support, R w.1 w.2

Discrete Strassen theorem (coupling lifting). Two discrete probability distributions p, q satisfying Hall's marginal-domination condition p(A) ≤ q(R(A)) for all A admit a coupling μ with marginals p and q that is supported on R.

SubProbability.exists_coupling_of_hall in GaudisCrypt/Logic/PRHL2.lean transfers this to SubProbabilitys.

References: V. Strassen, "The existence of probability measures with given marginals", Ann. Math. Statist. 36(2):423–439, 1965; for the finite case in exactly this Hall form, T. Koperberg, "Couplings and Matchings: combinatorial notes on Strassen's theorem", arXiv:2202.02092.