Pushforward measure ($f_{\ast }\mu$)

For a measurable map $f:X\to Y$, the pushforward of $\mu$ is the measureIt is the distribution induced on $Y$ by mapping points distributed according to $\mu$ through $f$.

Map a finite probability distribution through a function by summing the masses of source atoms with the same image. The image of the finite support is finite, and fibres partition the original support, so summing the output masses gives the original total one. Non-injective images require addition, not overwriting. A computational snapshot can evaluate each source image once and answer later mass queries by summing matching entries.

An orthogonally invariant random vector has a probability measure determined by its radial pushforward measure. Here $\sigma$ is normalized surface measure on a sphere, and the formula holds for bounded measurable $f$ and for nonnegative measurable $f$. It includes an atom of a measure at zero: the inner integral there is simply $f(0)$.

To prove the formula first for continuous bounded $f$, average $f(Qx)$ over normalized Haar measure of the compact orthogonal group. Right invariance makes this average depend only on $|x|$; averaging also over surface measure on a sphere identifies it with the spherical average. Invariance of $\mu$ and Fubini's theorem then give the identity. Uniqueness of finite Borel measures and measurable approximation extend it to the stated classes of $f$. No extra sphere-area factor belongs in an average against normalized surface measure on a sphere.

A homeomorphic embedding of a metric space induces a homeomorphic embedding of its probability measures for their weak topologies. The inverse continuity follows from the open-set Portmanteau theorem, since every relatively open set is the trace of an ambient open set. This does not give surjectivity onto $P(Z)$ when points of $Z$ are outside the embedded image.