Let \(\Omega \) be a finite measurable space, \(\mu \) a finite measure on it, and \(S \subseteq \Omega \) any set. Then

In other words, a finite measure on a finite measurable space is determined by and recovers as a finite sum over its singleton masses.

Let \(Z : \Omega \to \alpha \) be a function from a finite measurable space to a finite type, \(\mu \) a finite measure on \(\Omega \), and \(P\) a predicate on \(\alpha \). Then

On a finite measurable space, two measures satisfy \(\mu \ll \nu \) if and only if for every \(\omega \in \Omega \), \(\nu (\{ \omega \} ) = 0\) implies \(\mu (\{ \omega \} ) = 0\).

For any probability measure \(\mu \) on a finite measurable space and any function \(f : \Omega \to \mathbb {R}\),

Let \(Z : \Omega \to \alpha \) be a measurable map from a finite measurable space to a finite discrete type, \(\mu \) a finite measure on \(\Omega \), and \(f : \alpha \to \mathbb {R}\). Then

Let \(Z : \Omega \to \alpha \) be a finite-valued random variable on a finite measurable space with finite measure \(\mu \), and let \(S \subseteq \Omega \). Then

This is the law of total probability expressed in real-valued measure notation.

Let \(\Omega \) be a nonempty finite discrete type and let \(S \subseteq \Omega \). Under the uniform probability measure on \(\Omega \),

Under the uniform measure on a nonempty finite discrete type \(\Omega \), the real-valued measure of a set \(S\) equals \(|\{ S\} | / |\Omega |\) where \(|\{ S\} |\) denotes the cardinality of the subtype \(\{ \omega : \Omega \mid \omega \in S\} \).

Any type carrying a FiniteProbabilitySpace instance is nonempty.

For a finite probability space \(\Omega \) and any set \(S \subseteq \Omega \), \(\mathrm{volume}(S) = \sum _{\omega \in S} \mathrm{toPMF}(\Omega )(\omega )\).

For any bijection \(e : \Omega \xrightarrow {\sim } \alpha \) with \(\alpha \) finite, the family \(a \mapsto \mathrm{volume}(\{ e^{-1}(a)\} )\) has sum \(1\) as an \(\mathtt{HasSum}\) statement.

For finite probability spaces \(\Omega _1\) and \(\Omega _2\) and any \((x, y) \in \Omega _1 \times \Omega _2\),

For finite probability spaces \(\Omega _1\) and \(\Omega _2\) and sets \(A \subseteq \Omega _1\), \(B \subseteq \Omega _2\),

If \((A_i)_{i \in \iota }\) is a pairwise-disjoint family of sets indexed by a finite type \(\iota \) in a finite probability space \(\Omega \), then

For a map \(\varphi : \Xi \to \Omega \) from a finite probability space and a finite set \(T \subseteq \Omega \),

For a finite probability space \(\Omega \) and a finset \(T \subseteq \Omega \),

For a finite probability space \(\Omega \) and any \(f : \Omega \to \mathbb {R}\),

For a finite probability space \(\Omega \) and any \(f : \Omega \to \mathbb {R}\),

Let \(\Omega \) be a finite probability space, \(\iota \) a finite index type, and \(f : \Omega \to \mathbb {R}\). For any coordinate \(i \in \iota \), integrating \(\omega _{\bullet } \mapsto f(\omega _i)\) over the product space \((j : \iota ) \to \Omega \) (with the product measure) equals \(\int _\Omega f\).

For a finite index type \(\iota \), finite probability spaces \(\Omega _i\) for each \(i\), and sets \(s_i \subseteq \Omega _i\),

For a finite probability space \(\Omega \) and \(S \subseteq \Omega \), \(\mathrm{volume}^{\mathbb {R}}(S) = \int _\Omega \mathbf{1}_S(\omega )\, d\omega \), where \(\mathbf{1}_S\) denotes the indicator of \(S\) as an element of \(\Omega \to \mathbb {R}\).

For a finite probability space \(\Omega \) and \(S \subseteq \Omega \),

For any finite probability space \(\Omega \), \(\sum _{\omega \in \Omega } \mathrm{toPMF}(\Omega )(\omega )_{\mathbb {R}} = 1\).

For any finite probability space \(\Omega \) and \(\omega \in \Omega \), \(0 \le \mathrm{toPMF}(\Omega )(\omega )_{\mathbb {R}}\).

For any finite probability space \(\Omega \), there exists \(\omega \in \Omega \) such that \(\mathrm{toPMF}(\Omega )(\omega )_{\mathbb {R}} \gt 0\).

If \(f : \Omega \to \mathbb {R}\) satisfies \(f(\omega ) \le c\) for all \(\omega \) in a finite probability space, then \(\int _\Omega f \le c\).

For a nonneg function \(f : \Omega \to \mathbb {R}\) on a finite probability space and \(\varepsilon \gt 0\),

If \(f : \Omega \to \mathbb {R}\) satisfies \(c \lt f(\omega )\) for every \(\omega \) in a finite probability space, then \(c \lt \int _\Omega f\).