Fatou's lemma

Let $(X,\mathcal{A},\mu )$ be a measure space and let $f_n:X\to [0,+\mathrm{\infty }]$ be measurable. Then

${\int }_X{\mathrm{lim\hspace{0.17em}inf}}_{n\to \mathrm{\infty }}{f}_{n}d\mu \le {\mathrm{lim\hspace{0.17em}inf}}_{n\to \mathrm{\infty }}{\int }_X{f}_{n}d\mu \mathrm{.}$

The inequality can be strict. On $\mathbb{R}$ with Lebesgue measure, $f_n={\mathbf{1}}_{[n,n+1]}$ has ${\mathrm{lim\hspace{0.17em}inf}}_n{f}_n=0$ pointwise while $\int f_{n}d\lambda =1$ for every $n$, so the left side is $0$ and the right side is $1$: mass escapes to infinity. With $f_n=n{\mathbf{1}}_{(0,1\mathrm{/}n)}$ the same values arise with the mass escaping upward instead.

Not proved in this library. It is recorded with citations and used in no proof here.

What would prove it. One line from the monotone convergence theorem (Monotone convergence theorem (Beppo Levi) ‡): apply it to the increasing sequence $g_n:={\inf }_{k\ge n}{f}_k$, whose pointwise limit is ${\mathrm{lim\hspace{0.17em}inf}}_n{f}_n$, and use $g_n\le f_n$ to get $\int g_n\le \int f_n$. Fatou's lemma is thus not independent machinery; it is the convenient one-sided form of monotone convergence, and it is what the dominated convergence theorem is proved from.

Which page it serves. It is the tool that makes the limit theorems on the sequences and series pages usable for integrals, and it is the standard route to dominated convergence (Dominated convergence theorem ‡). Its two escaping mass examples are the sharpest available answer to the question "why is a dominating function needed", which the Riemann integral page can pose but not answer.