Probability measure (source code)

= Probability measure
{wiki}

A probability measure is a <measure> with total mass one.