Proof of Basic Properties of the Integral of Nonnegative Measurable Maps

For $f\in\mathcal{M}^{+}$, $\int_{X}f\,d\mu=\sup\Sigma_{f}$ with $\Sigma_{f}$ the nonempty subset of $[0,\infty]$ of Nonnegative Measurable Maps and Their Lebesgue Integral (ii). By Order and Suprema in the Extended Real Line (i), $\le$ is a total, hence partial, order on $[-\infty,\infty]$ that agrees with the order of $\mathbb{R}$ on real numbers; so for $s,t\in\mathcal{S}^{+}$ the relation $t\le s$ of Properties of Simple Functions and of the Simple Integral holds exactly when $t(x)\le s(x)$ in $[-\infty,\infty]$ for every $x\in X$.

Proof of (i). Let $s\in\mathcal{S}^{+}$. By Simple Functions, Nonnegative Simple Functions, and the Simple Integral (iii), Simple Functions, Nonnegative Simple Functions, and the Simple Integral (ii) and Simple Functions, Nonnegative Simple Functions, and the Simple Integral (i), $s$ is measurable as a map into $\mathbb{R}$, and $s(x)\ge0$ for every $x\in X$; so $s$ is measurable as a map into $[0,\infty]$ by Measurable Maps: Generators, Composition, Continuous Maps, Restrictions, and Criteria for Real- and [0,∞]-Valued Maps (vii), and $s\in\mathcal{M}^{+}$ by Nonnegative Measurable Maps and Their Lebesgue Integral (i). For every $t\in\mathcal{S}^{+}$ with $t(x)\le s(x)$ for every $x\in X$, $I_{\mu}(t)\le I_{\mu}(s)$ by Properties of Simple Functions and of the Simple Integral (vi); and $I_{\mu}(s)\in\Sigma_{s}$, as $s(x)\le s(x)$ for every $x$. So $I_{\mu}(s)$ is a greatest element of $\Sigma_{s}$, and $\sup\Sigma_{s}=I_{\mu}(s)$ by Greatest Elements as Suprema, Suprema and Infima of Nested Sets in [−∞,∞], and a Scaling Criterion for Order in [0,∞] (i), applied to the partial order $\le$ on $[-\infty,\infty]$. Hence $\int_{X}s\,d\mu=\sup\Sigma_{s}=I_{\mu}(s)$.

Proof of (ii). Let $A\in\mathcal{F}$. By Properties of Simple Functions and of the Simple Integral (i), $\mathbf{1}_{A}\in\mathcal{S}^{+}$ and $I_{\mu}(\mathbf{1}_{A})=\mu(A)$. By (i), $\mathbf{1}_{A}\in\mathcal{M}^{+}$ and $\int_{X}\mathbf{1}_{A}\,d\mu=I_{\mu}(\mathbf{1}_{A})=\mu(A)$.

Proof of (iii). Let $f,g\in\mathcal{M}^{+}$ with $f(x)\le g(x)$ for every $x\in X$. If $t\in\mathcal{S}^{+}$ and $t(x)\le f(x)$ for every $x$, then $t(x)\le g(x)$ for every $x$, by transitivity of $\le$ (Order and Suprema in the Extended Real Line (i)); so $\Sigma_{f}\subseteq\Sigma_{g}$, and $\sup\Sigma_{f}\le\sup\Sigma_{g}$ by Greatest Elements as Suprema, Suprema and Infima of Nested Sets in [−∞,∞], and a Scaling Criterion for Order in [0,∞] (ii). That is, $\int_{X}f\,d\mu\le\int_{X}g\,d\mu$.

Proof of (v). Let $z:X\to[0,\infty]$ satisfy $z(x)=0$ for every $x\in X$. The empty set $\emptyset$ belongs to $\mathcal{F}$ by Closure Properties of σ-Algebras, Intersections and Traces of σ-Algebras, and the Generated σ-Algebra (vi), and $\mathbf{1}_{\emptyset}(x)=0$ for every $x\in X$ by Indicator Function of a Subset (i), as no $x$ lies in $\emptyset$; so $z=\mathbf{1}_{\emptyset}$. By (ii), $z\in\mathcal{M}^{+}$ and $\int_{X}z\,d\mu=\mu(\emptyset)=0$, the last equality by Measure, Measure Space, and Probability Measure (i).

Proof of (iv). Let $c\in\mathbb{R}$ with $c\ge0$, let $f\in\mathcal{M}^{+}$, and let $h:X\to[0,\infty]$ satisfy $h(x)=c\cdot f(x)$ for every $x\in X$. By Addition and Multiplication on [0,∞] (ii), for $x\in X$: $h(x)$ is the real product $cf(x)$ if $f(x)\in\mathbb{R}$; $h(x)=0$ if $c=0$; and $h(x)=\infty$ if $c>0$ and $f(x)=\infty$.

Case $c=0$. Then $h(x)=0$ for every $x\in X$, so by (v), $h\in\mathcal{M}^{+}$ and $\int_{X}h\,d\mu=0=0\cdot\int_{X}f\,d\mu$, the last equality by Addition and Multiplication on [0,∞] (ii).

Case $c>0$. Measurability. Let $a\in\mathbb{R}$; we show $\{x\in X:h(x)>a\}=\{x\in X:f(x)>a/c\}$. If $f(x)\in\mathbb{R}$, then $h(x)=cf(x)$ is real, and $cf(x)>a$ if and only if $f(x)>a/c$ (by the order and arithmetic of $\mathrm{Real}$, The Real Numbers as a Type (vi) and The Real Numbers as a Type (v), with $q=a/c$ the real number with $q\cdot c=a$, Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (ii)), in $\mathbb{R}$ and hence in $[-\infty,\infty]$ by Order and Suprema in the Extended Real Line (i). If $f(x)=\infty$, then $h(x)=\infty$, and both $h(x)>a$ and $f(x)>a/c$ hold, since $\infty$ is the greatest element of $[-\infty,\infty]$ (Order and Suprema in the Extended Real Line (ii)) and $\infty\notin\mathbb{R}$ (The Extended Real Line, Its Order, and [0,∞] (i)). As $f$ is measurable as a map into $[0,\infty]$ (Nonnegative Measurable Maps and Their Lebesgue Integral (i)), the set $\{x\in X:f(x)>a/c\}$ belongs to $\mathcal{F}$ by Measurable Maps: Generators, Composition, Continuous Maps, Restrictions, and Criteria for Real- and [0,∞]-Valued Maps (vi). So $\{x\in X:h(x)>a\}\in\mathcal{F}$ for every $a\in\mathbb{R}$, $h$ is measurable as a map into $[0,\infty]$ by Measurable Maps: Generators, Composition, Continuous Maps, Restrictions, and Criteria for Real- and [0,∞]-Valued Maps (vi), and $h\in\mathcal{M}^{+}$ by Nonnegative Measurable Maps and Their Lebesgue Integral (i).

The integral. We show $\Sigma_{h}=\{c\cdot u:u\in\Sigma_{f}\}$. Let $t\in\mathcal{S}^{+}$ with $t(x)\le f(x)$ for every $x$. Then $ct\in\mathcal{S}^{+}$ by Properties of Simple Functions and of the Simple Integral (ii); for every $x$, $(ct)(x)=ct(x)$ (Pointwise Operations on Real-Valued Maps (i)) is the product $c\cdot t(x)$ of Addition and Multiplication on [0,∞] (ii), both factors being real, and $c\cdot t(x)\le c\cdot f(x)=h(x)$ by Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (iv) and Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (ii). So $I_{\mu}(ct)\in\Sigma_{h}$, and $I_{\mu}(ct)=c\cdot I_{\mu}(t)$ by Properties of Simple Functions and of the Simple Integral (v). Conversely, let $t'\in\mathcal{S}^{+}$ with $t'(x)\le h(x)$ for every $x$, and let $t=(1/c)t'$, with $r=1/c$ the real number with $r\cdot c=1$ (Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (ii)) and $r>0$ (Rules of Arithmetic and Order in an Ordered Field (viii)), which belongs to $\mathcal{S}^{+}$ by Properties of Simple Functions and of the Simple Integral (ii). For $x\in X$: if $f(x)=\infty$, then $t(x)\le f(x)$ by Order and Suprema in the Extended Real Line (ii); if $f(x)\in\mathbb{R}$, then $t'(x)\le cf(x)$ in $\mathbb{R}$ by Order and Suprema in the Extended Real Line (i), so $t(x)=t'(x)/c\le f(x)$. Thus $I_{\mu}(t)\in\Sigma_{f}$; and $ct=t'$, as $(ct)(x)=c\cdot(r\cdot t'(x))=t'(x)$ for every $x\in X$ (Pointwise Operations on Real-Valued Maps (i)) and maps with equal values are equal (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv)), so $I_{\mu}(t')=I_{\mu}(ct)=c\cdot I_{\mu}(t)$ by Properties of Simple Functions and of the Simple Integral (v). This proves $\Sigma_{h}=\{c\cdot u:u\in\Sigma_{f}\}$. Since $\Sigma_{f}$ is a nonempty subset of $[0,\infty]$ and $c\in[0,\infty]$, Suprema and Finite Sums in [0,∞] (ii) gives

$$\int_{X}h\,d\mu=\sup\Sigma_{h}=\sup\{c\cdot u:u\in\Sigma_{f}\}=c\cdot\sup\Sigma_{f}=c\cdot\int_{X}f\,d\mu.$$