Posterior has Sum

theorem posterior_hasSum (p : PMF α) (f : α → PMF β) (b : β)    (hb : b ∈ (p.bind f).support) :    HasSum (fun a =>      (p.bind fun a' => (f a').bind fun b' => PMF.pure (a', b')) (a, b) /        (p.bind f) b) 1 := by  have hne := (PMF.mem_support_iff _ _).mp hb  have hne_top := ne_top_of_le_ne_top one_ne_top (PMF.coe_le_one (p.bind f) b)  have : ∑' a, (p.bind fun a' => (f a').bind fun b' => PMF.pure (a', b')) (a, b) /      (p.bind f) b = 1 := by    simp only [div_eq_mul_inv]    rw [ENNReal.tsum_mul_right, bind_pair_tsum_fst]    exact ENNReal.mul_inv_cancel hne hne_top  exact this ▸ ENNReal.summable.hasSum