ThmDex – An index of mathematical definitions, results, and conjectures.
Tonelli's theorem for sums and integrals
Formulation 0
Let $M = (X, \mathcal{F}, \mu)$ be a D1158: Measure space such that
(i) $f_0, f_1, f_2, \ldots : X \to [0, \infty]$ are each a D5600: Basic Borel function on $M$
Then \begin{equation} \int_X \sum_{n \in \mathbb{N}} f_n \, d \mu = \sum_{n \in \mathbb{N}} \int_X f_n \, d \mu \end{equation}
Formulation 1
Let $M = (X, \mathcal{F}, \mu)$ be a D1158: Measure space such that
(i) $f_0, f_1, f_2, \ldots : X \to [0, \infty]$ are each a D5600: Basic Borel function on $M$
Then \begin{equation} \int_X \lim_{N \to \infty} \sum_{n = 0}^N f_n \, d \mu = \lim_{N \to \infty} \sum_{n = 0}^N \int_X f_n \, d \mu \end{equation}
Formulation 2
Let $M = (X, \mathcal{F}, \mu)$ be a D1158: Measure space such that
(i) $f_0, f_1, f_2, \ldots : X \to [0, \infty]$ are each a D5600: Basic Borel function on $M$
Then \begin{equation} \int_X \sum_{n = 0}^{\infty} f_n \, d \mu = \sum_{n = 0}^{\infty} \int_X f_n \, d \mu \end{equation}
Subresults
R3595: Probabilistic Tonelli's theorem
Proofs
Proof 0
Let $M = (X, \mathcal{F}, \mu)$ be a D1158: Measure space such that
(i) $f_0, f_1, f_2, \ldots : X \to [0, \infty]$ are each a D5600: Basic Borel function on $M$
Since each of $f_0, f_1, f_2, \ldots$ are unsigned, then the sequence $N \mapsto \sum_{n = 0}^N f_n$ is isotone in pointwise order. Hence, we may apply R1205: Monotone convergence theorem for unsigned integral to exchange the order of limit and integration to obtain \begin{equation} \int_X \sum_{n \in \mathbb{N}} f_n \, d \mu = \int_X \lim_{N \to \infty} \sum_{n = 0}^N f_n \, d \mu = \lim_{N \to \infty} \int_X \sum_{n = 0}^N f_n \, d \mu \end{equation} We may now apply R1233: Finite additivity of unsigned basic integral to conclude \begin{equation} \lim_{N \to \infty} \int_X \sum_{n = 0}^N f_n \, d \mu = \lim_{N \to \infty} \sum_{n = 0}^N \int_X f_n \, d \mu = \sum_{n \in \mathbb{N}} \int_X f_n \, d \mu \end{equation} $\square$