ThmDex – An index of mathematical definitions, results, and conjectures.
Result R4610 on D1732: Pushforward measure
Subresult of R4609:
Formulation 0
Let $P = (\Omega, \mathcal{F}, \mathbb{P})$ be a D1159: Probability space such that
(i) $X : \Omega \to \mathbb{R}$ is a D3161: Random real number on $P$
(ii) $\mu_X$ is a D204: Probability distribution measure for $X$
Let $M = (\mathbb{R}, \mathcal{B}(\mathbb{R}))$ be the D5072: Standard real borel measurable space such that
(i) $f : \mathbb{R} \to [0, \infty]$ is an D5610: Unsigned basic Borel function on $M$
Then \begin{equation} \mathbb{E} f(X) = \int_{\mathbb{R}} f \, d \mu_X \end{equation}
Subresults
R4611
Proofs
Proof 0
Let $P = (\Omega, \mathcal{F}, \mathbb{P})$ be a D1159: Probability space such that
(i) $X : \Omega \to \mathbb{R}$ is a D3161: Random real number on $P$
(ii) $\mu_X$ is a D204: Probability distribution measure for $X$
Let $M = (\mathbb{R}, \mathcal{B}(\mathbb{R}))$ be the D5072: Standard real borel measurable space such that
(i) $f : \mathbb{R} \to [0, \infty]$ is an D5610: Unsigned basic Borel function on $M$
This result is a particular case of R4609: . $\square$