diff --git a/Cslib/Probability/PMF.lean b/Cslib/Probability/PMF.lean
index af21c67c9..e34927505 100644
--- a/Cslib/Probability/PMF.lean
+++ b/Cslib/Probability/PMF.lean
@@ -136,4 +136,30 @@ theorem posteriorDist_eq_prior_of_outputIndist (p : PMF α) (f : α → PMF β)
   exact ENNReal.mul_div_cancel_right ((PMF.mem_support_iff _ _).mp (hbind ▸ hb))
     (PMF.apply_ne_top _ _)
 
+/-- Real-valued probability masses are summable, even on an infinite ambient type. -/
+theorem summable_toReal (p : PMF α) : Summable (fun a => (p a).toReal) :=
+  ENNReal.summable_toReal p.tsum_coe_ne_top
+
+/-- The real-valued masses of any discrete distribution sum to one. -/
+@[simp] theorem tsum_toReal (p : PMF α) : ∑' a, (p a).toReal = 1 := by
+  rw [← ENNReal.tsum_toReal_eq p.apply_ne_top, p.tsum_coe, ENNReal.toReal_one]
+
+/-- The real-valued probabilities of a finite distribution sum to one. -/
+theorem sum_toReal [Fintype α] (p : PMF α) :
+    ∑ a, (p a).toReal = 1 := by simpa using tsum_toReal p
+
+/-- Randomized postprocessing averages the outcome probabilities over any discrete input. -/
+theorem bind_apply_toReal_tsum (p : PMF α) (kernel : α → PMF β) (b : β) :
+    (p.bind kernel b).toReal = ∑' a, (p a).toReal * (kernel a b).toReal := by
+  rw [PMF.bind_apply, ENNReal.tsum_toReal_eq (fun a =>
+    ENNReal.mul_ne_top (p.apply_ne_top a) ((kernel a).apply_ne_top b))]
+  simp
+
+/-- The probability of an outcome after a finite random choice is its weighted average. -/
+theorem bind_apply_toReal [Fintype α] (p : PMF α)
+    (kernel : α → PMF β) (b : β) :
+    (p.bind kernel b).toReal =
+      ∑ a, (p a).toReal * (kernel a b).toReal := by
+  simpa using bind_apply_toReal_tsum p kernel b
+
 end Cslib.Probability.PMF