nLab
pushforward measure

Contents

Contents

Definition

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

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

As a functor

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:XYf:X\to Y, the pushforward gives a well-defined, measurable map PXPYP X\to P Y (where PP denotes the Giry monad), making PP into a functor.

Properties

References

See also

Last revised on November 17, 2019 at 22:09:14. See the history of this page for a list of all contributions to it.