Function to measure over discrete space?

Stream: Is there code for X?

[Markus de Medeiros]

Is there code for turning f : U -> ENNReal into a measure over the discrete space on U? I've used PMF.toMeasure before (at the moment I am converting that definition to work with functions that don't sum to 1) but I'm wondering if it's in Mathlib already.

[Markus de Medeiros]

Actually, I think I've dug up what I'm looking for, though it's not a generalization of PMF.toMeasure. For the record:

MeasureTheory.Measure.sum (fun u => f u • @MeasureTheory.Measure.dirac U ⊤ u)

[Yury G. Kudryashov]

Your solution LGTM