Integral with respect to Pushforward Measure

From ProofWiki
Jump to navigation Jump to search


Let $\struct {X, \Sigma, \mu}$ be a measure space.

Let $\struct {X', \Sigma'}$ be a measurable space.

Let $T: X \to X'$ be a $\Sigma \, / \, \Sigma'$-measurable mapping.

Let $f: X' \to \overline \R$ be a $\map T \mu$-integrable function, where $\map T \mu$ denotes the pushforward measure of $\mu$ under $T$.

Then $f \circ T: X \to \overline \R$ is $\mu$-integrable, and:

$\ds \int_{X'} f \rd \map T \mu = \int_X f \circ T \rd \mu$


Let $S \in \Sigma'$ be arbitrary.

We have:

\(\ds \int_{X'} \chi_S \rd \map T \mu\) \(=\) \(\ds \map T \mu \sqbrk S\)
\(\ds \) \(=\) \(\ds \map \mu {T^{-1} \sqbrk S}\)
\(\ds \) \(=\) \(\ds \int_X \chi_{T^{-1} \sqbrk S} \rd \mu\)
\(\ds \) \(=\) \(\ds \int_X \chi_S \circ T \rd \mu\)

By linearity, we obtain:

$\ds (1): \int_{X'} f \rd \map T \mu = \int_X f \circ T \rd \mu$

for simple $f: X' \to \hointr 0 \infty$.

Now let $f: X' \to \closedint 0 \infty$ be an arbitrary measurable map.

There is an increasing sequence $\sequence {f_n}_{n \mathop \in \N}$ of simple functions $f_n: X' \to \hointr 0 \infty$ that converges pointwise to $f$.

Note that $\sequence {f_n \circ T}_{n \mathop \in \N}$ is also an increasing sequence and converges pointwise to $f \circ T$.


\(\ds \int_{X'} f \rd \map T \mu\) \(=\) \(\ds \lim_{n \mathop \to \infty} \int_{X'} f_n \rd \map T \mu\) Monotone Convergence Theorem (Measure Theory)
\(\ds \) \(=\) \(\ds \lim_{n \mathop \to \infty} \int_X f_n \circ T \rd \mu\) from $(1)$
\(\ds \) \(=\) \(\ds \int_X f \circ T \rd \mu\) Monotone Convergence Theorem (Measure Theory)

Now suppose $f: X' \to \overline \R$ is $\map T \mu$-integrable.

Then $f^+, f^-: X' \to \closedint 0 \infty$ are both $\map T \mu$-integrable.

Thus by the previous result:

\(\ds \int_{X'} f \rd \map T \mu\) \(=\) \(\ds \int_{X'} f^+ \rd \map T \mu - \int_{X'} f^- \rd \map T \mu\)
\(\ds \) \(=\) \(\ds \int_X f^+ \circ T \rd \mu - \int_X f^- \circ T \rd \mu\)
\(\ds \) \(=\) \(\ds \int_X \paren {f^+ \circ T - f^- \circ T} \rd \mu\)
\(\ds \) \(=\) \(\ds \int_X f \circ T \rd \mu\)