Lean4
/-- Given a non-empty multiset `s` we construct the `PMF` which sends `a` to the fraction of
elements in `s` that are `a`. -/
def ofMultiset (s : Multiset α) (hs : s ≠ 0) : PMF α :=
⟨fun a => s.count a / (Multiset.card s),
ENNReal.summable.hasSum_iff.2
(calc
(∑' b : α, (s.count b : ℝ≥0∞) / (Multiset.card s)) = (Multiset.card s : ℝ≥0∞)⁻¹ * ∑' b, (s.count b : ℝ≥0∞) := by
simp_rw [ENNReal.div_eq_inv_mul, ENNReal.tsum_mul_left]
_ = (Multiset.card s : ℝ≥0∞)⁻¹ * ∑ b ∈ s.toFinset, (s.count b : ℝ≥0∞) :=
(congr_arg (fun x => (Multiset.card s : ℝ≥0∞)⁻¹ * x)
(tsum_eq_sum fun a ha => Nat.cast_eq_zero.2 <| by rwa [Multiset.count_eq_zero, ← Multiset.mem_toFinset]))
_ = 1 := by
rw [← Nat.cast_sum, Multiset.toFinset_sum_count_eq s,
ENNReal.inv_mul_cancel (Nat.cast_ne_zero.2 (hs ∘ Multiset.card_eq_zero.1)) (ENNReal.natCast_ne_top _)])⟩
