nLab pushforward measure

Contents

Context

Measure and probability theory

measure theory

probability theory

Contents

Definition

In measure theory, the pushforward $f_\ast \mu$ of a measure $\mu$ on a measurable space $X$ along a measurable function $f \colon X \to Y$ to another measure space $Y$ assigns to a subset the original measure of the preimage under $f$ of that subset:

$(f_\ast\mu)( - ) \coloneqq \mu(f^{-1}(-)) \,.$

Properties

Relation to entropy

Proposition

(entropy does not increase under pushforward) Let $f \colon X \longrightarrow Y$ be a measurable function between measure spaces, and let $\mu$ be a probability distribution on $X$. Then the entropy of $\mu$ is larger or equal to that of its pushforward distribution $f_\ast \mu$:

$S(\mu) \;\geq\; S \big( f_\ast(\mu) \big) \,.$

(e.g. Austin, Prop. 2.7)

The construction of pushforward measures is how one can make the Giry monad, or other measure monads, functorial. Given a measurable (or continuous, etc.) map $f \colon X\to Y$, the pushforward gives a well-defined, measurable map $P X\to P Y$ (where $P$ denotes the Giry monad), making $P$ into a functor.