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) : Pr[q | mx >>= my] = ∑ x : α, Pr[=x | mx] * Pr[q | my x]