Positive function integral

Set

context $M \in \mathrm{MeasureSpace}(X)$
postulate $\int_X:\mathcal M^+\to \mathbb R_+$
$ f\uparrow u_n$ $u_n\in \mathcal T^+$
postulate $\int_X\ f\ \mathrm d\mu:=\mathrm{lim}_{n\to \infty}\int_X\ u_n\ \mathrm d\mu$

Notice that the integral on the right hand side here is that for positive real step functions.

Discussion

Monotone convergence theorem:

If $f_n$ is a growing sequence in $\mathcal M^+$, we have

$\int_X\left(\mathrm{lim}_{n\to\infty}f_n\right)\mathrm d\mu=\mathrm{lim}_{n\to\infty}\int_X f_n\mathrm d\mu$

Parents

Context

Growing sequence, Step function integral, Positive measurable numerical function