Proof of Dominated Convergence Theorem

Conventions. In this proof $\int^{+}_{X}u\,d\mu$ is the integral of $u\in\mathcal{M}^{+}$ and $\int_{X}h\,d\mu$ that of $h\in\mathcal{L}^{1}(\mu)$. Real numbers $\ge0$ lie in $[0,\infty]$, where their sums are the real ones, and the order of $[-\infty,\infty]$ agrees with that of $\mathbb{R}$ on reals (The Extended Real Line, Its Order, and [0,∞] (ii), Addition and Multiplication on [0,∞] (i), Order and Suprema in the Extended Real Line (i)). Real arithmetic and order are those of the ordered field $\mathbb{R}$, read in the type $\mathrm{Real}$ (The Real Numbers Form an Ordered Field in Which Every Nonempty Set Bounded Above Has a Supremum (i), The Real Numbers as a Type (iv), The Real Numbers as a Type (v), The Real Numbers as a Type (vi), Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (i)).

Step 1: the limit is measurable and dominated by $g$. Let $x\in X$. Then $0\le|f_{1}(x)|\le g(x)$, so $g(x)\ge0$ (Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication (ii), Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (iii)). As $f_{m}(x)\to f(x)$, we have $|f_{m}(x)|\to|f(x)|$, and $|f_{m}(x)|\le g(x)$ for all $m$ gives

$$|f(x)|\le g(x)$$

(Limits of Sequences of Real Numbers: Uniqueness, Boundedness, Constants, Tails, Arithmetic, Quotients, Absolute Values, Finite Sums, Order, Squeezing, Domination and Subsequences (viii), Limits of Sequences of Real Numbers: Uniqueness, Boundedness, Constants, Tails, Arithmetic, Quotients, Absolute Values, Finite Sums, Order, Squeezing, Domination and Subsequences (x)). The sequence $(f_{m}(x))_{m}$ is convergent with limit $f(x)$, so $f$ is the function $x\mapsto\lim_{m\to\infty}f_{m}(x)$, which is measurable by Suprema, Pointwise Limits and the Convergence Set of Measurable Real-Valued Maps (ii) (The Limit of a Convergent Sequence (i), Measurable Map, and the Set of Measurable Maps (ii)).

Step 2: integrability. Each $f_{m}$ is measurable with $|f_{m}(x)|\le g(x)$, and so is $f$ by Step 1; by Linearity and Monotonicity of the Lebesgue Integral, and the Integrability Criterion (v), $f_{m}\in\mathcal{L}^{1}(\mu)$ for every $m$ and $f\in\mathcal{L}^{1}(\mu)$. This proves (i).

Step 3: the functions $|f_{m}-f|$ are integrable. Let $G=g+g$; by Linearity and Monotonicity of the Lebesgue Integral, and the Integrability Criterion (vii), with coefficients $1,1$, $G\in\mathcal{L}^{1}(\mu)$. Let $m\in\mathbb{N}$. The function $|f_{m}-f|$ is measurable (Arithmetic of Measurable Real- and [0,∞]-Valued Maps (i), applied twice), and for every $x\in X$, by the triangle inequality and Step 1,

$$0\le|f_{m}(x)-f(x)|\le|f_{m}(x)|+|f(x)|\le g(x)+g(x)=G(x)$$

(Pointwise Operations on Real-Valued Maps (i), Rules of Arithmetic and Order in an Ordered Field (xi), Rules of Arithmetic and Order in an Ordered Field (x), Rules of Arithmetic and Order in an Ordered Field (iv)). As $|f_{m}-f|$ has values $\ge0$, it is its own absolute value (Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (iii)), so $|f_{m}-f|\in\mathcal{L}^{1}(\mu)$ by Linearity and Monotonicity of the Lebesgue Integral, and the Integrability Criterion (v). This proves the first assertion of (ii).

Step 4: the integrals in $\mathcal{M}^{+}$. $G$ is measurable with $G(x)\ge0$, so by Linearity and Monotonicity of the Lebesgue Integral, and the Integrability Criterion (vi) $G\in\mathcal{M}^{+}$ and $c=\int^{+}_{X}G\,d\mu=\int_{X}G\,d\mu$ is a real number $\ge0$; likewise $|f_{m}-f|\in\mathcal{M}^{+}$ and $a_{m}=\int^{+}_{X}|f_{m}-f|\,d\mu=\int_{X}|f_{m}-f|\,d\mu$ is a real number $\ge0$. Let $k_{m}=G-|f_{m}-f|$ (the sequence $(k_{m})$ exists by Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps (iv), applied to $(m,x)\mapsto G(x)-|f_{m}(x)-f(x)|$ on $\mathbb{N}\times X$, formed with Projection, Evaluation and Currying Maps (ii) and Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps (iii)). Each $k_{m}$ is measurable (Arithmetic of Measurable Real- and [0,∞]-Valued Maps (i)) with values $\ge0$ by Step 3 (Rules of Arithmetic and Order in an Ordered Field (iv)), so $(k_{m})$ is a sequence in $\mathcal{M}^{+}$ by Linearity and Monotonicity of the Lebesgue Integral, and the Integrability Criterion (vi). As $G=|f_{m}-f|+k_{m}$, also as functions into $[0,\infty]$ (Sums, Multiples and Products of Functions into [0,∞] (i)), Linearity and Monotonicity of the Lebesgue Integral, and the Integrability Criterion (i) gives

$$c=\int^{+}_{X}G\,d\mu=\int^{+}_{X}|f_{m}-f|\,d\mu+\int^{+}_{X}k_{m}\,d\mu=a_{m}+\int^{+}_{X}k_{m}\,d\mu .$$

As $c$ is real, so is $\int^{+}_{X}k_{m}\,d\mu$ (otherwise the sum would be $\infty$, by Addition and Multiplication on [0,∞] (i)), and

$$\int^{+}_{X}k_{m}\,d\mu=c-a_{m}\qquad(m\in\mathbb{N}).$$

Step 5: $\liminf_{m}k_{m}(x)=G(x)$. Let $x\in X$ and $\ell=\liminf_{m}k_{m}(x)=\sup_{j}\inf_{m\ge j}k_{m}(x)$ (Tail Extrema, Limit Inferior and Limit Superior of a Sequence in [−∞,∞] (ii), Tail Extrema, Limit Inferior and Limit Superior of a Sequence in [−∞,∞] (i)). We have $|f_{m}(x)-f(x)|\to|0|=0$ (Limits of Sequences of Real Numbers: Uniqueness, Boundedness, Constants, Tails, Arithmetic, Quotients, Absolute Values, Finite Sums, Order, Squeezing, Domination and Subsequences (i), Limits of Sequences of Real Numbers: Uniqueness, Boundedness, Constants, Tails, Arithmetic, Quotients, Absolute Values, Finite Sums, Order, Squeezing, Domination and Subsequences (vi), Limits of Sequences of Real Numbers: Uniqueness, Boundedness, Constants, Tails, Arithmetic, Quotients, Absolute Values, Finite Sums, Order, Squeezing, Domination and Subsequences (viii)). For every $j$, $\inf_{m\ge j}k_{m}(x)\le k_{j}(x)\le G(x)$, so $\ell\le G(x)$. For real $\varepsilon>0$ choose $N$ with $|f_{m}(x)-f(x)|<\varepsilon$ for $m\ge N$ (Convergent Sequences of Real Numbers (i)); then $k_{m}(x)>G(x)-\varepsilon$ for $m\ge N$, so $G(x)-\varepsilon\le\inf_{m\ge N}k_{m}(x)\le\ell$. Thus

$$G(x)-\varepsilon\le\ell\le G(x)\qquad\text{for every real }\varepsilon>0$$

(Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iv), Rules of Arithmetic and Order in an Ordered Field (iv)). With $\varepsilon=1$, $G(x)-1\le\ell\le G(x)$ for the reals $G(x)-1$ and $G(x)$, which differ from $-\infty$ and $\infty$; so $\ell\neq-\infty$ and $\ell\neq\infty$ (The Extended Real Line, Its Order, and [0,∞] (i), Order and Suprema in the Extended Real Line (ii)), and $\ell$, an element of $[-\infty,\infty]$ (Tail Extrema, Limit Inferior and Limit Superior of a Sequence in [−∞,∞] (ii)), is a real number (The Extended Real Line, Its Order, and [0,∞] (ii)). If $\ell<G(x)$, then $\varepsilon=(G(x)-\ell)/2>0$ would give $\ell\ge G(x)-\varepsilon=(G(x)+\ell)/2>\ell$ (Rules of Arithmetic and Order in an Ordered Field (ix), Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (ii)); hence $\ell=G(x)$.

Step 6: $\int_{X}|f_{m}-f|\,d\mu\to0$. By Step 5, $G$, read as a function into $[0,\infty]$, satisfies $G(x)=\liminf_{m}k_{m}(x)$ for every $x$, so by Fatou's Lemma (ii) and Step 4

$$c=\int^{+}_{X}G\,d\mu\le\liminf_{m}\int^{+}_{X}k_{m}\,d\mu=\sup_{j}\inf_{m\ge j}(c-a_{m}).$$

Let $\varepsilon>0$ be real. As $c-\varepsilon<c$, there is $j$ with $c-\varepsilon<\inf_{m\ge j}(c-a_{m})\le c-a_{m}$ for every $m\ge j$ (Order and Suprema in the Extended Real Line (x), Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iv)), that is, $0\le a_{m}<\varepsilon$ and so $|a_{m}-0|<\varepsilon$ (Rules of Arithmetic and Order in an Ordered Field (iv), Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (iii)). Hence $a_{m}=\int_{X}|f_{m}-f|\,d\mu\to0$ (Convergent Sequences of Real Numbers (i)), which with Step 3 proves (ii).

Step 7: convergence of the integrals. Let $m\in\mathbb{N}$. By Step 2 and Linearity and Monotonicity of the Lebesgue Integral, and the Integrability Criterion (vii), with coefficients $1,-1$, $f_{m}-f\in\mathcal{L}^{1}(\mu)$ with $\int_{X}(f_{m}-f)\,d\mu=\int_{X}f_{m}\,d\mu-\int_{X}f\,d\mu$, and by Linearity and Monotonicity of the Lebesgue Integral, and the Integrability Criterion (x)

$$\Bigl|\int_{X}f_{m}\,d\mu-\int_{X}f\,d\mu\Bigr|=\Bigl|\int_{X}(f_{m}-f)\,d\mu\Bigr|\le\int_{X}|f_{m}-f|\,d\mu .$$

The right-hand side is a null sequence by (ii), so $\int_{X}f_{m}\,d\mu\to\int_{X}f\,d\mu$ by Limits of Sequences of Real Numbers: Uniqueness, Boundedness, Constants, Tails, Arithmetic, Quotients, Absolute Values, Finite Sums, Order, Squeezing, Domination and Subsequences (xii). This proves (iii).