ThmDex – An index of mathematical definitions, results, and conjectures.
Result R4609 on D1732: Pushforward measure
Formulation 0
Let $P = (\Omega, \mathcal{F}_{\Omega}, \mathbb{P})$ be a D1159: Probability space.
Let $M = (\Xi, \mathcal{F}_{\Xi})$ be a D1108: Measurable space such that
(i) $X : \Omega \to \Xi$ is a D202: Random variable from $P$ to $M$
(ii) $\mu_X : \mathcal{F}_{\Xi} \to [0, \infty]$ is a D204: Probability distribution measure for $X$
(iii) $f : \Xi \to [0, \infty]$ is a D313: Measurable function on $M_Y$
Then \begin{equation} \int_{\Omega} f(X) \, d \mathbb{P} = \int_{\Xi} f \, d \mu_X \end{equation}
Proofs
Proof 0
Let $P = (\Omega, \mathcal{F}_{\Omega}, \mathbb{P})$ be a D1159: Probability space.
Let $M = (\Xi, \mathcal{F}_{\Xi})$ be a D1108: Measurable space such that
(i) $X : \Omega \to \Xi$ is a D202: Random variable from $P$ to $M$
(ii) $\mu_X : \mathcal{F}_{\Xi} \to [0, \infty]$ is a D204: Probability distribution measure for $X$
(iii) $f : \Xi \to [0, \infty]$ is a D313: Measurable function on $M_Y$