Tonelli's Theorem

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\struct {X, \Sigma_X, \mu}$ and $\struct {Y, \Sigma_Y, \nu}$ be $\sigma$-finite measure spaces.

Let $\struct {X \times Y, \Sigma_X \otimes \Sigma_Y, \mu \times \nu}$ be the product measure space of $\struct {X, \Sigma_X, \mu}$ and $\struct {Y, \Sigma_Y, \nu}$.

Let $f: X \times Y \to \overline \R_{\ge 0}$ be a positive $\Sigma_X \otimes \Sigma_Y$-measurable function.


Then:

$\ds \int_{X \times Y} f \map \rd {\mu \times \nu} = \int_Y \int_X \map f {x, y} \map {\d \mu} x \map {\d \nu} y = \int_X \int_Y \map f {x, y} \map {\d \nu} y \map {\d \mu} x$


Corollary

Let $\sequence {a_{n, m} }_{\tuple {n, m} \in \N^2}$ be a doubly subscripted sequence of non-negative real numbers.


Then:

$\ds \sum_{n \mathop = 1}^\infty \paren {\sum_{m \mathop = 1}^\infty a_{n, m} } = \sum_{m \mathop = 1}^\infty \paren {\sum_{n \mathop = 1}^\infty a_{n, m} }$


Proof

We rewrite the demand as:

$\ds \int_{X \times Y} f \map \rd {\mu \times \nu} = \int_Y \paren {\int_X f^y \rd \mu} \rd \nu = \int_X \paren {\int_Y f_x \rd \nu} \rd \mu$

where $f_x$ is the $x$-vertical section of $f$, and $f^y$ is the $y$-horizontal section of $f$.

From Horizontal Section of Measurable Function is Measurable, we have:

$f^y$ is $\Sigma_X$-measurable.

From Vertical Section of Measurable Function is Measurable, we have:

$f_x$ is $\Sigma_Y$-measurable.

From Integral of Horizontal Section of Measurable Function gives Measurable Function, we then have:

$\ds y \mapsto \int_X f^y \rd \mu$ is $\Sigma_Y$-measurable

and from Integral of Vertical Section of Measurable Function gives Measurable Function, we have:

$\ds x \mapsto \int_Y f_x \rd \nu$ is $\Sigma_X$-measurable.

So, both:

$\ds \int_Y \paren {\int_X f^y \rd \mu} \rd \nu$

and:

$\ds \int_X \paren {\int_Y f_x \rd \nu} \rd \mu$

are well-defined.


We first prove the case of:

$f = \chi_E$

where $E$ is a $\Sigma_X \otimes \Sigma_Y$-measurable set.

Lemma 1

Let $E \in \Sigma_X \otimes \Sigma_Y$.

Let:

$f = \chi_E$

where $\chi_E$ is the characteristic function of $E$.


Then:

$\ds \int_{X \times Y} f \map \rd {\mu \times \nu} = \int_Y \paren {\int_X f^y \rd \mu} \rd \nu = \int_X \paren {\int_Y f_x \rd \nu} \rd \mu$

$\Box$


Now consider the case of a positive simple $f$.

Lemma 2

Let $f : X \times Y \to \overline \R$ be a positive simple function.


Then:

$\ds \int_{X \times Y} f \map \rd {\mu \times \nu} = \int_Y \paren {\int_X f^y \rd \mu} \rd \nu = \int_X \paren {\int_Y f_x \rd \nu} \rd \mu$

$\Box$


Now take a general positive $\Sigma_X \otimes \Sigma_Y$-measurable function $f$.

We first show:

$\ds \int_{X \times Y} f \map \rd {\mu \times \nu} = \int_Y \paren {\int_X f^y \rd \mu} \rd \nu$

From Measurable Function is Pointwise Limit of Simple Functions:

there exists a increasing sequence of positive simple functions $\sequence {f_n}_{n \mathop \in \N}$ such that $f_n \to f$ pointwise.

From Simple Function is Measurable, we have:

for each $n \in \N$, the function $f_n$ is $\Sigma_X \otimes \Sigma_Y$-measurable.

From Horizontal Section of Measurable Function is Measurable, we have:

for each $n \in \N$, the function $\paren {f_n}^y$ is $\Sigma_X$-measurable, for each $y \in Y$.

From Horizontal Section preserves Increasing Sequences of Functions, we have:

the sequence $\sequence {\paren {f_n}^y}_{n \mathop \in \N}$ is increasing for each $y \in Y$.

Now, from Horizontal Section preserves Pointwise Limits of Sequences of Functions, we have:

$\paren {f_n}^y \to f^y$ pointwise for each $y \in Y$.

For each $n \in \N$ define a function $g_n : X \to \overline \R$ by:

$\ds \map {g_n} y = \int_X \paren {f_n}^y \rd \mu$

for each $y \in Y$.

Since $\sequence {\paren {f_n}^y}_{n \mathop \in \N}$ is an increasing sequence of $\Sigma_X$-measurable functions, we can apply the Monotone Convergence Theorem to obtain:

$\ds \lim_{n \mathop \to \infty} \map {g_n} y = \int_X f^y \rd \nu$

From Integral of Positive Measurable Function is Monotone, we have:

$\sequence {g_n}_{n \mathop \in \N}$ is increasing.

From Integral of Horizontal Section of Measurable Function gives Measurable Function, we have:

$\sequence {g_n}_{n \mathop \in \N}$ is $\Sigma_Y$-measurable.

For each $n \in \N$, we have:

\(\ds \int_{X \times Y} f_n \map \rd {\mu \times \nu}\) \(=\) \(\ds \int_Y \paren {\int_X \paren {f_n}^y \rd \mu} \rd \nu\) from our work with simple functions
\(\ds \) \(=\) \(\ds \int_Y g_n \rd \nu\)

Since $\sequence {f_n}_{n \mathop \in \N}$ is an increasing sequence of $\Sigma_X \otimes \Sigma_Y$-measurable functions converging pointwise to $f$, we have:

$\ds \lim_{n \mathop \to \infty} \int_{X \times Y} f_n \map \rd {\mu \times \nu} = \int_{X \times Y} f \map \rd {\mu \times \nu}$

from the Monotone Convergence Theorem.

Since $\sequence {g_n}_{n \mathop \in \N}$ is an increasing sequence of $\Sigma_X \otimes \Sigma_Y$-measurable functions with:

$\ds g_n \to \int_X f^y \rd \mu$ pointwise.

So:

$\ds \lim_{n \mathop \to \infty} \int_Y g_n \rd \nu = \int_Y \paren {\int_X f^y \rd \mu} \rd \nu$

by the Monotone Convergence Theorem.

So we obtain:

$\ds \int_{X \times Y} f \map \rd {\mu \times \nu} = \int_Y \paren {\int_X f^y \rd \mu} \rd \nu$


We now show:

$\ds \int_{X \times Y} f \map \rd {\mu \times \nu} = \int_X \paren {\int_Y f_x \rd \nu} \rd \mu$

From Measurable Function is Pointwise Limit of Simple Functions:

there exists a increasing sequence of positive simple functions $\sequence {f_n}_{n \mathop \in \N}$ such that $f_n \to f$ pointwise.

From Simple Function is Measurable, we have:

for each $n \in \N$, the function $f_n$ is $\Sigma_X \otimes \Sigma_Y$-measurable.

From Vertical Section of Measurable Function is Measurable, we have:

for each $n \in \N$, the function $\paren {f_n}_x$ is $\Sigma_Y$-measurable, for each $x \in X$.

From Vertical Section preserves Increasing Sequences of Functions, we have:

the sequence $\sequence {\paren {f_n}_x}_{n \mathop \in \N}$ is increasing for each $x \in X$.

Now, from Vertical Section preserves Pointwise Limits of Sequences of Functions, we have:

$\paren {f_n}_x \to f_x$ pointwise for each $x \in X$.

For each $n \in \N$ define a function $h_n : X \to \overline \R$ by:

$\ds \map {h_n} x = \int_Y \paren {f_n}_x \rd \nu$

for each $x \in X$.

Since $\sequence {\paren {f_n}_x}_{n \mathop \in \N}$ is an increasing sequence of $\Sigma_Y$-measurable functions, we can apply the Monotone Convergence Theorem to obtain:

$\ds \lim_{n \mathop \to \infty} \map {h_n} x = \int_Y f_x \rd \nu$

From Integral of Positive Measurable Function is Monotone, we have:

$\sequence {h_n}_{n \mathop \in \N}$ is increasing.

From Integral of Vertical Section of Measurable Function gives Measurable Function, we have:

$\sequence {h_n}_{n \mathop \in \N}$ is $\Sigma_X$-measurable.

For each $n \in \N$, we have:

\(\ds \int_{X \times Y} f_n \map \rd {\mu \times \nu}\) \(=\) \(\ds \int_X \paren {\int_Y \paren {f_n}_x \rd \nu} \rd \mu\) from our work with simple functions
\(\ds \) \(=\) \(\ds \int_X h_n \rd \mu\)

Since $\sequence {f_n}_{n \mathop \in \N}$ is an increasing sequence of $\Sigma_X \otimes \Sigma_Y$-measurable functions converging pointwise to $f$, we have:

$\ds \lim_{n \mathop \to \infty} \int_{X \times Y} f_n \map \rd {\mu \times \nu} = \int_{X \times Y} f \map \rd {\mu \times \nu}$

from the Monotone Convergence Theorem.

Since $\sequence {h_n}_{n \mathop \in \N}$ is an increasing sequence of $\Sigma_X \otimes \Sigma_Y$-measurable functions with:

$\ds h_n \to \int_X f^y \rd \mu$ pointwise.

So:

$\ds \lim_{n \mathop \to \infty} \int_Y h_n \rd \nu = \int_X \paren {\int_Y f_x \rd \nu} \rd \mu$

by the Monotone Convergence Theorem.

So we obtain:

$\ds \int_{X \times Y} f \map \rd {\mu \times \nu} = \int_X \paren {\int_Y f_x \rd \nu} \rd \mu$

giving:

$\ds \int_{X \times Y} f \map \rd {\mu \times \nu} = \int_Y \int_X \map f {x, y} \map {\d \mu} x \map {\d \nu} y = \int_X \int_Y \map f {x, y} \map {\d \nu} y \map {\d \mu} x$

as was the demand.

$\blacksquare$


Also see


Source of Name

This entry was named for Leonida Tonelli.


Sources

Retrieved from "https://proofwiki.org/w/index.php?title=Tonelli%27s_Theorem&oldid=639284"