Probability measure

Measure;

Probability space;

class probability_measure (P : finset ι → [0,1]) :=
(countably_additive : {A i}i ⊆ P, pairwise_disjoint A, P(⋃ i, A i) = ∑ i, P(A i) )
(measure_whole_space : P(Ω) = 1)

Each prob. distribution is an instance of a probability measure.

• Random variable is instance of probability measure”

References

• Wikipedia;