Disagreement-Aware Additive Bind Bounds

A family of bind-bound lemmas charging an exceptional set ("disagreement") to its mass plus per-point slack. They are the workhorses behind coupled game-hopping proofs that need to bound Pr[q | mx >>= my] by Pr[q | mx >>= oc] plus a small additive term.

These statements are framed for any monad m with [HasEvalSPMF m]; the canonical specialisation is m = ProbComp.

Main results

• probEvent_bind_le_add_of_disagree — 2-way base case.
• probEvent_bind_le_add_bad_of_disagree — 3-way with bad-event side.
• probEvent_bind_le_add_bad_of_disagree' — 3-way with per-step bad term in the IH.
• probEvent_bind_le_add_bad_disagree — 4-way merge.

theorem probEvent_bind_le_add_of_disagree {α β : Type u} {m : Type u → Type v} [Monad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] {mx : m α} {my oc : α → m β} {q : β → Prop} {D : α → Prop} {ε₁ ε₂ : ENNReal} (hD : probEvent mx D ≤ ε₁) (h : ∀ x ∈ support mx, ¬D x → probEvent (my x) q ≤ probEvent (oc x) q + ε₂) : probEvent (mx >>= my) q ≤ probEvent (mx >>= oc) q + ε₁ + ε₂

Disagreement-aware additive bind bound. If the disagreement set D has probability at most ε₁ under mx, and off D the continuation my is within ε₂ of the reference continuation oc, then Pr[q | mx >>= my] ≤ Pr[q | mx >>= oc] + ε₁ + ε₂. The exceptional set D is charged its full mass ε₁; everywhere else the per-point gap ε₂ is paid.

theorem probEvent_bind_le_add_bad_of_disagree {α β γ : Type u} {m : Type u → Type v} [Monad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] {mx : m α} {my oc : α → m β} {ob : α → m γ} {q : β → Prop} {r : γ → Prop} {D : α → Prop} {ε : ENNReal} (hbad : ∀ x ∈ support mx, D x → probEvent (ob x) r = 1) (h : ∀ x ∈ support mx, ¬D x → probEvent (my x) q ≤ probEvent (oc x) q + ε) : probEvent (mx >>= my) q ≤ probEvent (mx >>= oc) q + probEvent (mx >>= ob) r + ε

Three-way disagreement-aware additive bind bound (hop A). A coupled three-world variant of probEvent_bind_le_add_of_disagree: the three worlds share the sampling computation mx, and at each shared sample x, off the disagreement set D the my-world is bounded by the oc-world plus the per-step slack ε, while on D the ob-world (the bad world) already fires its event r with probability 1. The conclusion charges the disagreement to Pr[r | mx >>= ob].

theorem probEvent_bind_le_add_bad_of_disagree' {α β γ : Type u} {m : Type u → Type v} [Monad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] {mx : m α} {my oc : α → m β} {ob : α → m γ} {q : β → Prop} {r : γ → Prop} {D : α → Prop} {ε : ENNReal} (hbad : ∀ x ∈ support mx, D x → probEvent (ob x) r = 1) (h : ∀ x ∈ support mx, ¬D x → probEvent (my x) q ≤ probEvent (oc x) q + probEvent (ob x) r + ε) : probEvent (mx >>= my) q ≤ probEvent (mx >>= oc) q + probEvent (mx >>= ob) r + ε

Four-way disagreement-aware additive bind bound (hop A). A strengthening of probEvent_bind_le_add_bad_of_disagree: the per-step inductive hypothesis itself carries a bad-event term, so off the disagreement set D the my-world is bounded by the oc-world plus the per-shared-sample bad probability Pr[r | ob x] plus the slack ε. On D the ob-world already fires r with probability 1. Both cases are charged into the aggregate Pr[r | mx >>= ob], so the conclusion is the same shape as the three-way bound.

theorem probEvent_bind_le_add_bad_disagree {α β γ : Type u} {m : Type u → Type v} [Monad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] {mx : m α} {my oc : α → m β} {ob : α → m γ} {q : β → Prop} {r : γ → Prop} {D : α → Prop} {ε₁ ε₂ : ENNReal} (hD : probEvent mx D ≤ ε₁) (h : ∀ x ∈ support mx, ¬D x → probEvent (my x) q ≤ probEvent (oc x) q + probEvent (ob x) r + ε₂) : probEvent (mx >>= my) q ≤ probEvent (mx >>= oc) q + probEvent (mx >>= ob) r + ε₁ + ε₂

Four-way disagreement+bad additive bind bound. A merge of probEvent_bind_le_add_of_disagree with the three-world probEvent_bind_le_add_bad_of_disagree: the disagreement set D (a table-level exceptional set, not a bad event) is charged its full mass ε₁; everywhere off D the my-world is bounded by the oc-world plus the per-shared-sample bad probability Pr[r | ob x] plus the slack ε₂.