Pushforward of a finite probability distribution (source code)

= Pushforward of a finite probability distribution
{title2=$q(y)=\sum_{x:f(x)=y}p(x)$}

For a <finite probability distribution> $p$ with support $S$ and a total <function> $f:S\to Y$, assign each image value the combined mass of its preimages. Its support is exactly the finite image $f(S)$, listed without repetitions. Every listed mass is positive because it contains at least one positive source mass.

The <fiber of a function> construction gives a <set partition> of $S$, so finite summation gives $\sum_yq(y)=\sum_{x\in S}p(x)=1$. This proves nonnegativity and normalization without assuming that $f$ is injective. In code, mapping support values and then overwriting repeated image keys is incorrect; repeated keys must have their masses added. For example, mapping a uniform distribution on four consecutive <integers> to parity produces two outcomes with mass one half each.