Integrable Functions and Their Lebesgue Integral

In the setting of Measure Spaces, Borel Sets and Lebesgue Measure on the Real Line: Standing Notation, let $(X,\mathcal{F},\mu)$ be a measure space. Let $\mathrm{Meas}(X,\mathcal{F};\mathbb{R},\mathcal{B}(\mathbb{R}))$ be the set of measurable functions $X\to\mathbb{R}$ of Measurable Map, and the Set of Measurable Maps (ii), let $\mathcal{M}^{+}=\mathcal{M}^{+}(X,\mathcal{F})$ be the set of measurable functions into $[0,\infty]$, and for $g\in\mathcal{M}^{+}$ let $\int_{X}g\,d\mu\in[0,\infty]$ be its integral. For $f:X\to\mathbb{R}$, $f^{+}$ and $f^{-}$ are its positive part and negative part.

(i) Integrable functions. A function $f\in\mathrm{Meas}(X,\mathcal{F};\mathbb{R},\mathcal{B}(\mathbb{R}))$ is integrable with respect to $\mu$ if

$$\int_{X}f^{+}\,d\mu<\infty\qquad\text{and}\qquad\int_{X}f^{-}\,d\mu<\infty$$

(here $f^{+},f^{-}\in\mathcal{M}^{+}$ by Arithmetic of Measurable Real- and [0,∞]-Valued Maps (i) and Measurable Maps: Generators, Composition, Continuous Maps, Restrictions, and Criteria for Real- and [0,∞]-Valued Maps (vii)).

(ii) The set $\mathcal{L}^{1}(\mu)$. $\mathcal{L}^{1}(X,\mathcal{F},\mu)$, also written $\mathcal{L}^{1}(\mu)$, is the set of those $f\in\mathrm{Meas}(X,\mathcal{F};\mathbb{R},\mathcal{B}(\mathbb{R}))$ that are integrable with respect to $\mu$ (a set by The Functions f ↦ f⁺ and f ↦ f⁻ on the Real-Valued Functions on a Set, and a Predicative Form of g = f⁺ and g = f⁻ (ii) and Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices (iv)).

(iii) The integral. For $f\in\mathcal{L}^{1}(\mu)$, the integrals $\int_{X}f^{+}\,d\mu$ and $\int_{X}f^{-}\,d\mu$ are finite, hence real numbers (Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros (ii)). The integral of $f$ with respect to $\mu$ is the real number

$$\int_{X}f\,d\mu=\int_{X}f^{+}\,d\mu-\int_{X}f^{-}\,d\mu,$$

also written $\int f\,d\mu$; the function $f\mapsto\int_{X}f\,d\mu$ from $\mathcal{L}^{1}(\mu)$ to $\mathbb{R}$ is the integral with respect to $\mu$ (it exists by The Functions f ↦ f⁺ and f ↦ f⁻ on the Real-Valued Functions on a Set, and a Predicative Form of g = f⁺ and g = f⁻ (iii)). A function in both $\mathcal{M}^{+}$ and $\mathcal{L}^{1}(\mu)$ thus has two integrals; where it matters, the text names which one is meant.