**Theorem**(itg2mono): If $(f_n)_{n\in\Bbb N}$ is a sequence of measurable functions $\Bbb R\to[0,\infty)$ such that $$0\le f_1\le f_2\le\dots\le f_n\le\dots$$ and the pointwise limit $g$ of the sequence $(f_n)$ exists, then $g$ is measurable and $\int g=\lim_{n\to\infty}\int f_n$ (note that for increasing sequences, $\lim$ and $\sup$ are equivalent, so the statement may differ from the Metamath version for this reason).

**Proof**: First, we prove $g$ is measurable. (mbfmono) It is sufficient to prove that the inverse image $\{g>t\}=\{x\in\Bbb R|g(x)>t\}$ is measurable, which follows from $\{g>t\}=\bigcup_{n\in\Bbb N}\{f_n>t\}$, because $t<g(x)=\sup_{n\in\Bbb N}f_n(x)\iff\exists n\in\Bbb N:t<f_n(x)$ and the countable union of the measurable sets $\{f_n>t\}$ is measurable.

Before tackling the main claim $\int g=\lim_{n\to\infty}\int f_n$, we will need a few more lemmas, so let's get those down first.

**Theorem**(volsup): If $(A_n)_{n\in\Bbb N}$ is a sequence of measurable sets such that $A_1\subseteq A_2\subseteq\dots\subseteq A_n\subseteq\dots\subseteq\Bbb R$ and $\bigcup_{n\in\Bbb N}A_n=A$, then $\DeclareMathOperator{\vol}{vol}\vol(A)=\lim_{n\to\infty}\vol(A_n)$, where the limit may be $\infty$.

**Proof**: First, we address the case when there is an $A_k$ such that $\vol(A_k)=\infty$. In this case, $A_k\subseteq A$ implies $\vol(A)=\infty$, and $$\lim_{n\to\infty}\vol(A_n)=\sup_{n\to\infty}\vol(A_n)\ge\vol(A_k)=\infty$$ so $\lim_{n\to\infty}\vol(A_n)=\infty$ as well.

Otherwise, all the $\vol(A_n)$ are real, so we are free to do arithmetic on the volumes. Consider the sequence $B_n=A_n\setminus\bigcup_{k=1}^{n-1}A_k=A_n\setminus A_{n-1}$ (where the second representation is only valid for $n\ge2$). This is a set of pairwise-disjoint measurable sets, so from voliun we have $\vol(\bigcup_{n\in\Bbb N}B_n)=\sum_{n=1}^\infty\vol(B_n)$. Now each $B_n\subseteq A_n$, so $\bigcup_{n\in\Bbb N}B_n\subseteq A$, and each $x\in A$ is in some $A_k$, and for the minimal $k$, it is also in $B_k$. Thus $A=\bigcup_{n\in\Bbb N}B_n$. As for the sum, we prove by induction that $\sum_{k=1}^n\vol(B_n)=\vol(A_n)$ and therefore the sequence of partial sums of $\vol(B_n)$ is the sequence $\vol(A_n)$ and $\sum_{n=1}^\infty\vol(B_n)=\lim_{n\to\infty}\vol(A_n)$.

For $n=1$, we have $B_1=A_1$ so $\sum_{k=1}^1\vol(B_n)=\vol(A_1)$, and assuming that this is true for $n$, we have $$\sum_{k=1}^{n+1}\vol(B_n)=\vol(A_n)+\vol(B_{n+1})=\vol(A_n)+\vol(A_{n+1}\setminus A_n),$$ and since these are disjoint sets and $A_n\subseteq A_{n+1}$ we have $\vol(A_n)+\vol(A_{n+1}\setminus A_n)=\vol(A_{n+1})$. $$\tag*{$\blacksquare$}$$

Next we use this theorem to prove that the integral on simple functions respects limit operations on the base set.

**Theorem**(itg1climres): If $(A_n)_{n\in\Bbb N}$ is a sequence of measurable sets such that $A_1\subseteq A_2\subseteq\dots\subseteq A_n\subseteq\dots\subseteq\Bbb R$ and $\bigcup_{n\in\Bbb N}A_n=\Bbb R$, and $\phi$ is a simple function, then $\lim_{n\to\infty}\int_{A_n}\phi=\int\phi$.

**Proof**: We expand out the definition of the integral on simple functions: $\int\phi=\sum_{x\in\Bbb R^*}x\vol(\phi^{-1}\{x\})$, where the sum is nominally over all nonzero reals but is only nonzero for finitely many $x$. We can distribute the limit over the sum: $$\lim_{n\to\infty}\int_{A_n}\phi=\lim_{n\to\infty}\sum_{x\in\Bbb R^*}x\vol(\phi^{-1}\{x\}\cap A_n)=\sum_{x\in\Bbb R^*}x\lim_{n\to\infty}\vol(\phi^{-1}\{x\}\cap A_n),$$ so we are reduced to proving $\lim_{n\to\infty}\vol(\phi^{-1}\{x\}\cap A_n)=\vol(\phi^{-1}\{x\})$, which is an application of volsup above, taking the sets $(\phi^{-1}\{x\}\cap A_n)_{n\in\Bbb N}$ as our increasing sequence. $$\tag*{$\blacksquare$}$$

Now we are finally ready to return to our proof of the main theorem itg2mono. The easy direction of our equality is $\lim_{n\to\infty}\int f_n\le\int g$, which is true because each $f_n\le g$ so $\int f_n\le\int g$ by itg2le. Now the definition of $\int g$ is as a supremum over all simple functions $\phi\le g$. Thus to show $\int g\le\lim_{n\to\infty}\int f_n$ we can show that $S:=\lim_{n\to\infty}\int f_n$ is an upper bound on $\int\phi$ for any $\phi\le g$. Now we are going to prove that $t\int\phi\le S$ for any $0<t<1$, but to get from there to $\int\phi\le S$ takes a little trickery.

We assume that $\int\phi>S$ to start with. Since $S\in[0,\infty]$ and $\int\phi\in\Bbb R$ to start with (remember that $S$ is a supremum, possibly infinite, of integrals of nonnegative functions, while $\phi$ is a simple function whose integral is real but possibly negative), the inequality $\int\phi>S$ immediately implies $S\in\Bbb R$ and $\int\phi>0$. Now we can use alrple to use that for any $x>0$, $\int\phi\le S+x$ and hence prove that $\int\phi\ge S$ (in contradiction to our assumption, thus showing $\int\phi\ge S$ unconditionally). Define $t=\max(\frac12,\frac S{S+x})$, which is valid since $S\ge 0$ and $x>0$. Then $t\ge\frac12>0$ and $t\le\frac S{S+x}<1$, so by our lemma below, $t\int\phi\le S$. Since $\int\phi>0$ and $t>0$ we can infer $S>0$, so we can cancel the $S$ and multiply by $S+x$ in $\frac S{S+x}\int\phi\le t\int\phi\le S$ to get $\int\phi\le S+x$ as we wanted to show.

Now all that remains to prove is our lemma:

**Lemma**(itg2monolem): For any $0<t<1$, and any simple function $\phi\le g$, we have $\int\phi\le \lim_{n\to\infty}\int f_n$.

**Proof**: Define the sequence $A_n=\{x\in\Bbb R|t\phi(x)\le f_n(x)\}$. Then $\int_{A_n}t\phi\le\int f_n$ because the restricted function $t\phi\upharpoonright A_n$ is always dominated by $f_n$: if $x\notin A_n$ then $(t\phi\upharpoonright A_n)(x)=0\le f(n)$ and if $x\in A_n$ then $(t\phi\upharpoonright A_n)(x)=t\phi(x)\le f(n)$. We can take this inequality in the limit, and thus $$\int t\phi=\lim_{n\to\infty}\int_{A_n}t\phi\le\lim_{n\to\infty}\int f_n,$$ where the first equality is none other than our earlier lemma itg1climres, which can be applied because $A_n=\{0\le f_n-t\phi\}$ is a measurable set (since $f_n-t\phi$ is a sum of a simple function and a measurable function, which is measurable), the $A_n$ sets form an inclusion chain since $f_{n+1}\le f_n$, and the union of all of them is $\Bbb R$ because either $\phi(x)>0$ in which case $t\phi(x)<\phi(x)\le g(x)$ and there is some $f_n(x)>t\phi(x)$, or $\phi(x)\le0$ in which case $t\phi(x)\le0\le f_n(x)$ for every $n$. This completes the proof. $$\tag*{$\blacksquare$}$$

## No comments:

## Post a Comment