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.

Dirac couplings: when one marginal is pure

When the left marginal is pure a (and analogously on the right), the coupling collapses to the Dirac product (a, ·) <$> q. This is the key combinatorial ingredient behind anchoring: the relational logic must agree with the unary logic in this corner.

theorem SPMF.IsCoupling.dirac_left {α β : Type u} (a : α) {q : SPMF β} (hq : q.toPMF none = 0) : ((fun (x : β) => (a, x)) <$> q).IsCoupling (pure a) q

Dirac coupling on the left: (a, ·) <$> q is a coupling between pure a and q, provided q has no failure mass.

theorem SPMF.IsCoupling.dirac_right {α β : Type u} {p : SPMF α} (b : β) (hp : p.toPMF none = 0) : ((fun (x : α) => (x, b)) <$> p).IsCoupling p (pure b)

Dirac coupling on the right: (·, b) <$> p is a coupling between p and pure b, provided p has no failure mass.

theorem SPMF.IsCoupling.apply_eq_zero_of_pure_left {α β : Type u} {a : α} {q : SPMF β} {c : SPMF (α × β)} (hc : c.IsCoupling (pure a) q) {x : α} (b : β) (hxa : x ≠ a) : c (x, b) = 0

Pointwise characterization of any coupling whose left marginal is pure a: mass off the slice {a} × β is zero.

theorem SPMF.IsCoupling.apply_eq_zero_of_pure_right {α β : Type u} {p : SPMF α} {b : β} {c : SPMF (α × β)} (hc : c.IsCoupling p (pure b)) (a : α) {y : β} (hyb : y ≠ b) : c (a, y) = 0

Pointwise characterization of any coupling whose right marginal is pure b: mass off the slice α × {b} is zero.

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

For a coupling whose left marginal is pure a, the value at (a, b) matches the right marginal q b.

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

For a coupling whose right marginal is pure b, the value at (a, b) matches the left marginal p a.

theorem SPMF.IsCoupling.tsum_pure_left {α β : Type u} {a : α} {q : SPMF β} {c : SPMF (α × β)} (hc : c.IsCoupling (pure a) q) (g : α → β → ENNReal) : ∑' (z : α × β), c z * g z.1 z.2 = ∑' (b : β), q b * g a b

Anchoring identity for tsum-style expectations on the left: the expected value of g under any coupling between pure a and q is the marginal expectation ∑' b, q b * g a b.

theorem SPMF.IsCoupling.tsum_pure_right {α β : Type u} {p : SPMF α} {b : β} {c : SPMF (α × β)} (hc : c.IsCoupling p (pure b)) (g : α → β → ENNReal) : ∑' (z : α × β), c z * g z.1 z.2 = ∑' (a : α), p a * g a b

Anchoring identity for tsum-style expectations on the right: the expected value of g under any coupling between p and pure b is the marginal expectation ∑' a, p a * g a b.