Coupling for probability distributions

class PMF.IsCoupling {α : Type u_1} {β : Type u_2} (c : PMF (α × β)) (p : PMF α) (q : PMF β) : Prop

• map_fst : map Prod.fst c = p
• map_snd : map Prod.snd c = q

def PMF.Coupling {α : Type u_1} {β : Type u_2} (p : PMF α) (q : PMF β) : Type (max 0 u_1 u_2)

class SPMF.IsCoupling {α β : Type u} (c : SPMF (α × β)) (p : SPMF α) (q : SPMF β) : Prop

• map_fst : Prod.fst <$> c = p
• map_snd : Prod.snd <$> c = q

theorem SPMF.IsCoupling.ext_iff {α β : Type u} {c : SPMF (α × β)} {p : SPMF α} {q : SPMF β} {x y : c.IsCoupling p q} : x = y ↔ True

theorem SPMF.IsCoupling.ext {α β : Type u} {c : SPMF (α × β)} {p : SPMF α} {q : SPMF β} {x y : c.IsCoupling p q} : x = y

def SPMF.Coupling {α β : Type u} (p : SPMF α) (q : SPMF β) : Type u

theorem SPMF.IsCoupling.pure_iff {α β : Type u} {a : α} {b : β} {c : SPMF (α × β)} : c.IsCoupling (pure a) (pure b) ↔ c = pure (a, b)

The coupling of two pure values must be the pure pair of those values

theorem SPMF.IsCoupling.none_iff {α β : Type u} {c : SPMF (α × β)} : c.IsCoupling failure failure ↔ c = failure

theorem SPMF.IsCoupling.bind {α₁ α₂ β₁ β₂ : Type u} {p : SPMF α₁} {q : SPMF α₂} {f : α₁ → SPMF β₁} {g : α₂ → SPMF β₂} (c : p.Coupling q) (d : α₁ → α₂ → SPMF (β₁ × β₂)) (h : ∀ (a₁ : α₁) (a₂ : α₂), ↑↑c (some (a₁, a₂)) ≠ 0 → (d a₁ a₂).IsCoupling (f a₁) (g a₂)) : (do let p ← ↑c d p.1 p.2).IsCoupling (p >>= f) (q >>= g)

Main theorem about coupling and bind operations

theorem SPMF.IsCoupling.exists_bind {α₁ α₂ β₁ β₂ : Type u} {p : SPMF α₁} {q : SPMF α₂} {f : α₁ → SPMF β₁} {g : α₂ → SPMF β₂} (c : p.Coupling q) (h : ∀ (a₁ : α₁) (a₂ : α₂), ∃ (d : SPMF (β₁ × β₂)), d.IsCoupling (f a₁) (g a₂)) : ∃ (d : SPMF (β₁ × β₂)), d.IsCoupling (p >>= f) (q >>= g)

Existential version of IsCoupling.bind

theorem SPMF.IsCoupling.refl {α : Type u} (p : SPMF α) : (do let a ← p pure (a, a)).IsCoupling p p

Every SPMF has a diagonal self-coupling.

noncomputable def SPMF.Coupling.refl {α : Type u} (p : SPMF α) : p.Coupling p

Diagonal self-coupling witness.

theorem SPMF.bind_const_of_toPMF_none_eq_zero {α β : Type u} {p : SPMF α} (hp : p.toPMF none = 0) (q : SPMF β) : (do let _ ← p q) = q

Binding against a constant q collapses to q when the scrutinee has no failure mass.

theorem SPMF.IsCoupling.prod {α β : Type u} {p : SPMF α} {q : SPMF β} (hp : p.toPMF none = 0) (hq : q.toPMF none = 0) : (do let a ← p let b ← q pure (a, b)).IsCoupling p q

Product coupling: when both distributions have no failure mass, their independent product forms a coupling.

This is the core coupling result for reasoning about pairs of computations that never fail individually (e.g., OracleComp spec α via HasEvalPMF): the product distribution do let a ← p; let b ← q; pure (a, b) witnesses that the pair has marginals (p, q).

noncomputable def SPMF.Coupling.prod {α β : Type u} {p : SPMF α} {q : SPMF β} (hp : p.toPMF none = 0) (hq : q.toPMF none = 0) : p.Coupling q

Product coupling witness.