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