Tonelli's Theorem

== 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 ===
== 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 ===
Now consider the case of a positive simple $f$. 
=== Lemma 2 ===
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: 
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: 
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.
== Also see ==
* Fubini's Theorem, a similar result pertaining to $\mu$-integrable functions.
== Sources ==
* 
* : $13.8$
* : $5.2$: Fubini's Theorem: Proposition $5.2.1 \text{ (b)}$
Category:Tonelli's Theorem
Category:Integral of Positive Measurable Function
Category:Product Measure