Lemmas for Probability Over Finite Spaces

This file houses lemmas about HasEvalDist m and related classes when a computation mx : m α is defined via a binding/mapping operation over a finite type. In particular Finset.sum versions of many tsum related lemmas about HasEvalDist.

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

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

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

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

Union bound: the probability that some event E i holds is at most the sum of the individual probabilities, over a finite index set s.