Lemmas for Probability Over Finite Spaces

This file houses lemmas about computations with MonadLiftT m SPMF semantics when mx : m α is defined via a binding/mapping operation over a finite type. In particular it provides Finset.sum versions of many tsum related probability lemmas.

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

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

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