Evaluation Distributions of Computations with Bind

File for lemmas about evalDist and support involving the monadic pure and bind.

@[simp]

theorem support_pure {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] (x : α) : support (pure x) = {x}

theorem mem_support_pure_iff {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] (x y : α) : x ∈ support (pure y) ↔ x = y

theorem mem_support_pure_iff' {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] (x y : α) : x ∈ support (pure y) ↔ y = x

@[simp]

theorem finSupport_pure {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] (x : α) : finSupport (pure x) = {x}

theorem mem_finSupport_pure_iff {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] (x y : α) : x ∈ finSupport (pure y) ↔ x = y

theorem mem_finSupport_pure_iff' {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] (x y : α) : x ∈ finSupport (pure y) ↔ y = x

@[simp]

theorem evalDist_pure {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {α : Type u} (x : α) : evalDist (pure x) = pure x

@[simp]

theorem evalDist_comp_pure {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] : evalDist ∘ pure = pure

@[simp]

theorem evalDist_comp_pure' {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (f : α → β) : evalDist ∘ pure ∘ f = pure ∘ f

@[simp]

theorem probOutput_pure {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [DecidableEq α] (x y : α) : Pr[= x | pure y] = if x = y then 1 else 0

@[simp]

theorem probOutput_pure_self {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (x : α) : Pr[= x | pure x] = 1

theorem probOutput_pure_eq_indicator {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (x y : α) : Pr[= x | pure y] = {y}.indicator (Function.const α 1) x

Fallback when we don't have decidable equality.

@[simp]

theorem probEvent_pure {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (x : α) (p : α → Prop) [DecidablePred p] : probEvent (pure x) p = if p x then 1 else 0

theorem probEvent_pure_eq_indicator {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (x : α) (p : α → Prop) : probEvent (pure x) p = {x : α | p x}.indicator (Function.const α 1) x

Fallback when we don't have decidable equality.

@[simp]

theorem probFailure_pure {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (x : α) : Pr[⊥ | pure x] = 0

@[simp]

theorem tsum_probOutput_pure {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (x : α) : ∑' (y : α), Pr[= y | pure x] = 1

@[simp]

theorem tsum_probOutput_pure' {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (x : α) : ∑' (y : α), Pr[= x | pure y] = 1

@[simp]

theorem sum_probOutput_pure {α : Type u} {m : Type u → Type v} [Monad m] [Fintype α] [HasEvalSPMF m] (x : α) : ∑ y : α, Pr[= y | pure x] = 1

@[simp]

theorem sum_probOutput_pure' {α : Type u} {m : Type u → Type v} [Monad m] [Fintype α] [HasEvalSPMF m] (x : α) : ∑ y : α, Pr[= x | pure y] = 1

@[simp]

theorem support_bind {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] (mx : m α) (my : α → m β) : support (mx >>= my) = ⋃ x ∈ support mx, support (my x)

theorem mem_support_bind_iff {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] (mx : m α) (my : α → m β) (y : β) : y ∈ support (mx >>= my) ↔ ∃ x ∈ support mx, y ∈ support (my x)

@[simp]

theorem finSupport_bind {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] [DecidableEq β] (mx : m α) (my : α → m β) : finSupport (mx >>= my) = (finSupport mx).biUnion fun (x : α) => finSupport (my x)

theorem mem_finSupport_bind_iff {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] [DecidableEq β] (mx : m α) (my : α → m β) (y : β) : y ∈ finSupport (mx >>= my) ↔ ∃ x ∈ finSupport mx, y ∈ finSupport (my x)

@[simp]

theorem evalDist_bind {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : α → m β) : evalDist (mx >>= my) = do let x ← evalDist mx evalDist (my x)

theorem evalDist_bind_of_support_eq_empty {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : α → m β) (h : support mx = ∅) : evalDist (mx >>= my) = failure

theorem probOutput_bind_eq_tsum {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : α → m β) (y : β) : Pr[= y | mx >>= my] = ∑' (x : α), Pr[= x | mx] * Pr[= y | my x]

theorem probEvent_bind_eq_tsum {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : α → m β) (q : β → Prop) : probEvent (mx >>= my) q = ∑' (x : α), Pr[= x | mx] * probEvent (my x) q

theorem probFailure_bind_eq_add_tsum {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : α → m β) : Pr[⊥ | mx >>= my] = Pr[⊥ | mx] + ∑' (x : α), Pr[= x | mx] * Pr[⊥ | my x]

theorem probFailure_bind_eq_add_tsum_support {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : α → m β) : Pr[⊥ | mx >>= my] = Pr[⊥ | mx] + ∑' (x : ↑(support mx)), Pr[= ↑x | mx] * Pr[⊥ | my ↑x]

@[simp]

theorem probFailure_bind_eq_zero_iff {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : α → m β) : Pr[⊥ | mx >>= my] = 0 ↔ Pr[⊥ | mx] = 0 ∧ ∀ x ∈ support mx, Pr[⊥ | my x] = 0

theorem probOutput_bind_eq_tsum_subtype {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : α → m β) (y : β) : Pr[= y | mx >>= my] = ∑' (x : ↑(support mx)), Pr[= ↑x | mx] * Pr[= y | my ↑x]

Version of probOutput_bind_eq_tsum that sums only over the subtype given by the support of the first computation. This can be useful to avoid looking at edge cases that can't actually happen in practice after the first computation. A common example is if the first computation does some error handling to avoids returning malformed outputs.

theorem probEvent_bind_eq_tsum_subtype {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : α → m β) (q : β → Prop) : probEvent (mx >>= my) q = ∑' (x : ↑(support mx)), Pr[= ↑x | mx] * probEvent (my ↑x) q

theorem probOutput_bind_eq_sum_finSupport {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [HasEvalFinset m] (mx : m α) (my : α → m β) [DecidableEq α] (y : β) : Pr[= y | mx >>= my] = ∑ x ∈ finSupport mx, Pr[= x | mx] * Pr[= y | my x]

theorem probEvent_bind_eq_sum_finSupport {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [HasEvalFinset m] (mx : m α) (my : α → m β) [DecidableEq α] (q : β → Prop) : probEvent (mx >>= my) q = ∑ x ∈ finSupport mx, Pr[= x | mx] * probEvent (my x) q

@[simp]

theorem support_bind_const {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] (mx : m α) (my : m β) : (support do let _ ← mx my) = {y : β | y ∈ support my ∧ (support mx).Nonempty}

@[simp]

theorem finSupport_bind_const {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] [HasEvalFinset m] [DecidableEq β] [DecidableEq α] (mx : m α) (my : m β) : (finSupport do let _ ← mx my) = if (finSupport mx).Nonempty then finSupport my else ∅

theorem probOutput_bind_of_const {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) {my : α → m β} {y : β} {r : ENNReal} (h : ∀ x ∈ support mx, Pr[= y | my x] = r) : Pr[= y | mx >>= my] = (1 - Pr[⊥ | mx]) * r

@[simp]

theorem probOutput_bind_const {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : m β) (y : β) : Pr[= y | do let _ ← mx my] = (1 - Pr[⊥ | mx]) * Pr[= y | my]

theorem probEvent_bind_of_const {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) {my : α → m β} {p : β → Prop} {r : ENNReal} (h : ∀ x ∈ support mx, probEvent (my x) p = r) : probEvent (mx >>= my) p = (1 - Pr[⊥ | mx]) * r

@[simp]

theorem probEvent_bind_const {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : m β) (p : β → Prop) : probEvent (do let _ ← mx my) p = (1 - Pr[⊥ | mx]) * probEvent my p

theorem probFailure_bind_of_const {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} {my : α → m β} {r : ENNReal} (h : ∀ x ∈ support mx, Pr[⊥ | my x] = r) : Pr[⊥ | mx >>= my] = Pr[⊥ | mx] + r * (1 - Pr[⊥ | mx])

Write the probability of mx >>= my failing given that my has constant failure chance over the possible outputs in support mx as a fixed expression without any sums.

theorem probFailure_bind_of_const' {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} {my : α → m β} {r : ENNReal} (hr : r ≠ ⊤) (h : ∀ x ∈ support mx, Pr[⊥ | my x] = r) : Pr[⊥ | mx >>= my] = Pr[⊥ | mx] + r - Pr[⊥ | mx] * r

@[simp]

theorem probFailure_bind_const {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : m β) : Pr[⊥ | do let _ ← mx my] = Pr[⊥ | mx] + Pr[⊥ | my] - Pr[⊥ | mx] * Pr[⊥ | my]

theorem probFailure_bind_eq_sub_mul {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : α → m β) (r : ENNReal) (hr : r ≠ ⊤) (h : ∀ x ∈ support mx, Pr[⊥ | my x] = r) : Pr[⊥ | mx >>= my] = 1 - (1 - Pr[⊥ | mx]) * (1 - r)

theorem probFailure_bind_le_add_of_forall {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} {my : α → m β} {r : ENNReal} (hr : ∀ x ∈ support mx, Pr[⊥ | my x] ≤ r) : Pr[⊥ | mx >>= my] ≤ Pr[⊥ | mx] + (1 - Pr[⊥ | mx]) * r

theorem probFailure_bind_le_of_forall' {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} {s : ENNReal} (h' : Pr[⊥ | mx] = s) (my : α → m β) {r : ENNReal} (hr : ∀ x ∈ support mx, Pr[⊥ | my x] ≤ r) : Pr[⊥ | mx >>= my] ≤ s + r

Version of probFailure_bind_le_of_forall with that allows a manual Pr[⊥ | mx] value.

theorem probFailure_bind_le_of_forall {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} (h' : Pr[⊥ | mx] = 0) {my : α → m β} {r : ENNReal} (hr : ∀ x ∈ support mx, Pr[⊥ | my x] ≤ r) : Pr[⊥ | mx >>= my] ≤ r

Version of probFailure_bind_le_of_forall when mx never fails.

theorem probFailure_bind_of_probFailure_eq_zero {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} (h' : Pr[⊥ | mx] = 0) {my : α → m β} : Pr[⊥ | mx >>= my] = ∑' (x : α), Pr[= x | mx] * Pr[⊥ | my x]

theorem mul_le_probEvent_bind {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} {my : α → m β} {p : α → Prop} {q : β → Prop} {r r' : ENNReal} (h : r ≤ probEvent mx p) (h' : ∀ x ∈ support mx, p x → r' ≤ probEvent (my x) q) : r * r' ≤ probEvent (mx >>= my) q

theorem probFailure_bind_congr {α β γ : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) {my : α → m β} {oc : α → m γ} (h : ∀ x ∈ support mx, Pr[⊥ | my x] = Pr[⊥ | oc x]) : Pr[⊥ | mx >>= my] = Pr[⊥ | mx >>= oc]

theorem probFailure_bind_congr' {α β γ : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) {my : α → m β} {oc : α → m γ} (h : ∀ (x : α), Pr[⊥ | my x] = Pr[⊥ | oc x]) : Pr[⊥ | mx >>= my] = Pr[⊥ | mx >>= oc]

theorem probOutput_bind_congr {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} {ob₁ ob₂ : α → m β} {y : β} (h : ∀ x ∈ support mx, Pr[= y | ob₁ x] = Pr[= y | ob₂ x]) : Pr[= y | mx >>= ob₁] = Pr[= y | mx >>= ob₂]

theorem probOutput_bind_congr' {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) {ob₁ ob₂ : α → m β} (y : β) (h : ∀ (x : α), Pr[= y | ob₁ x] = Pr[= y | ob₂ x]) : Pr[= y | mx >>= ob₁] = Pr[= y | mx >>= ob₂]

theorem probOutput_bind_mono {α β γ : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} {my : α → m β} {oc : α → m γ} {y : β} {z : γ} (h : ∀ x ∈ support mx, Pr[= y | my x] ≤ Pr[= z | oc x]) : Pr[= y | mx >>= my] ≤ Pr[= z | mx >>= oc]

theorem probEvent_bind_congr {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} {ob₁ ob₂ : α → m β} {q : β → Prop} (h : ∀ x ∈ support mx, probEvent (ob₁ x) q = probEvent (ob₂ x) q) : probEvent (mx >>= ob₁) q = probEvent (mx >>= ob₂) q

theorem probEvent_bind_congr' {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) {ob₁ ob₂ : α → m β} (q : β → Prop) (h : ∀ (x : α), probEvent (ob₁ x) q = probEvent (ob₂ x) q) : probEvent (mx >>= ob₁) q = probEvent (mx >>= ob₂) q

theorem probEvent_bind_mono {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} {my oc : α → m β} {q : β → Prop} (h : ∀ x ∈ support mx, probEvent (my x) q ≤ probEvent (oc x) q) : probEvent (mx >>= my) q ≤ probEvent (mx >>= oc) q

theorem probOutput_bind_congr_div_const {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} {ob₁ ob₂ : α → m β} {y : β} {r : ENNReal} (h : ∀ x ∈ support mx, Pr[= y | ob₁ x] = Pr[= y | ob₂ x] / r) : Pr[= y | mx >>= ob₁] = Pr[= y | mx >>= ob₂] / r

theorem probOutput_bind_congr_eq_add {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {γ₁ γ₂ : Type u} {mx : m α} {my : α → m β} {oc₁ : α → m γ₁} {oc₂ : α → m γ₂} {y : β} {z₁ : γ₁} {z₂ : γ₂} (h : ∀ x ∈ support mx, Pr[= y | my x] = Pr[= z₁ | oc₁ x] + Pr[= z₂ | oc₂ x]) : Pr[= y | mx >>= my] = Pr[= z₁ | mx >>= oc₁] + Pr[= z₂ | mx >>= oc₂]

theorem probOutput_bind_congr_le_add {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {γ₁ γ₂ : Type u} {mx : m α} {my : α → m β} {oc₁ : α → m γ₁} {oc₂ : α → m γ₂} {y : β} {z₁ : γ₁} {z₂ : γ₂} (h : ∀ x ∈ support mx, Pr[= y | my x] ≤ Pr[= z₁ | oc₁ x] + Pr[= z₂ | oc₂ x]) : Pr[= y | mx >>= my] ≤ Pr[= z₁ | mx >>= oc₁] + Pr[= z₂ | mx >>= oc₂]

theorem probOutput_bind_congr_add_le {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {γ₁ γ₂ : Type u} {mx : m α} {my : α → m β} {oc₁ : α → m γ₁} {oc₂ : α → m γ₂} {y : β} {z₁ : γ₁} {z₂ : γ₂} (h : ∀ x ∈ support mx, Pr[= z₁ | oc₁ x] + Pr[= z₂ | oc₂ x] ≤ Pr[= y | my x]) : Pr[= z₁ | mx >>= oc₁] + Pr[= z₂ | mx >>= oc₂] ≤ Pr[= y | mx >>= my]

theorem probOutput_bind_congr_le_sub {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {γ₁ γ₂ : Type u} {mx : m α} {my : α → m β} {oc₁ : α → m γ₁} {oc₂ : α → m γ₂} {y : β} {z₁ : γ₁} {z₂ : γ₂} (h : ∀ x ∈ support mx, Pr[= y | my x] ≤ Pr[= z₁ | oc₁ x] - Pr[= z₂ | oc₂ x]) (h' : ∀ x ∈ support mx, Pr[= z₂ | oc₂ x] ≤ Pr[= z₁ | oc₁ x]) : Pr[= y | mx >>= my] ≤ Pr[= z₁ | mx >>= oc₁] - Pr[= z₂ | mx >>= oc₂]

theorem probOutput_bind_congr_sub_le {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {γ₁ γ₂ : Type u} {mx : m α} {my : α → m β} {oc₁ : α → m γ₁} {oc₂ : α → m γ₂} {y : β} {z₁ : γ₁} {z₂ : γ₂} (h : ∀ x ∈ support mx, Pr[= z₁ | oc₁ x] - Pr[= z₂ | oc₂ x] ≤ Pr[= y | my x]) : Pr[= z₁ | mx >>= oc₁] - Pr[= z₂ | mx >>= oc₂] ≤ Pr[= y | mx >>= my]

theorem probEvent_bind_le_add {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} {my : α → m β} {p : α → Prop} {q : β → Prop} {ε₁ ε₂ : ENNReal} (h₁ : (probEvent mx fun (x : α) => ¬p x) ≤ ε₁) (h₂ : ∀ x ∈ support mx, p x → (probEvent (my x) fun (y : β) => ¬q y) ≤ ε₂) : (probEvent (mx >>= my) fun (y : β) => ¬q y) ≤ ε₁ + ε₂

Union bound for bind: if Pr[ ¬p | mx] ≤ ε₁ and Pr[ ¬q | my x] ≤ ε₂ for all x satisfying p, then Pr[ ¬q | mx >>= my] ≤ ε₁ + ε₂. Useful for sequential composition of error bounds.

theorem probEvent_bind_congr_le_add {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} {my oc : α → m β} {q : β → Prop} {ε : ENNReal} (h : ∀ x ∈ support mx, probEvent (my x) q ≤ probEvent (oc x) q + ε) : probEvent (mx >>= my) q ≤ probEvent (mx >>= oc) q + ε

probEvent version of probEvent_bind_mono with additive error bound.

theorem probEvent_bind_bind_swap {α β γ : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m α) (my : m β) (f : α → β → m γ) (q : γ → Prop) : probEvent (do let a ← mx let b ← my f a b) q = probEvent (do let b ← my let a ← mx f a b) q

Swapping two independent random draws preserves probability of any event.

theorem probOutput_bind_bind_swap {α β γ : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m α) (my : m β) (f : α → β → m γ) (z : γ) : Pr[= z | do let a ← mx let b ← my f a b] = Pr[= z | do let b ← my let a ← mx f a b]

Swapping two independent random draws preserves the probability of any fixed output.

theorem probEvent_compl_le_of_ge {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} {p : α → Prop} {ε : ENNReal} (hfail : Pr[⊥ | mx] = 0) (h : probEvent mx p ≥ 1 - ε) : (probEvent mx fun (x : α) => ¬p x) ≤ ε

If Pr[ p | mx] ≥ 1 - ε and mx never fails, then Pr[ ¬p | mx] ≤ ε.

theorem probEvent_ge_of_compl_le {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} {p : α → Prop} {ε : ENNReal} (hfail : Pr[⊥ | mx] = 0) (h : (probEvent mx fun (x : α) => ¬p x) ≤ ε) : probEvent mx p ≥ 1 - ε

If Pr[ ¬p | mx] ≤ ε and mx never fails, then Pr[ p | mx] ≥ 1 - ε.

theorem probEvent_exists_finset_le_sum {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {ι : Type u_1} (s : Finset ι) (mx : m α) (E : ι → α → Prop) : (probEvent mx fun (x : α) => ∃ i ∈ s, E i x) ≤ ∑ i ∈ s, probEvent mx (E i)

Union bound for finset-indexed events: the probability that some event in s holds is at most the sum of the individual event probabilities.