\section{Integration of Simple Functions}
\label{section:lebesgue-simple}

\begin{definition}[Space of Simple Functions]
\label{definition:simple-function-scalar}
    Let $(X, \cm)$ be a measurable space, then $\Sigma(X, \cm) = \Sigma(X, \cm; \complex)$ is the space of $\complex$-valued simple functions on $(X, \cm)$, and $\Sigma^+(X, \cm)$ is the space of non-negative simple functions.
\end{definition}

\begin{definition}[Integral of Non-Negative Simple Functions]
\label{definition:lebesgue-simple}
    Let $(X, \cm, \mu)$ be a measure space and $f = \sum_{y \in f(X)}y \cdot \one_{\bracs{f = y}} \in \Sigma^+(X, \cm)$ be a non-negative simple function in standard form, then (with the convention that $0 \cdot \infty = 0$)
    \[
    \int f d\mu = \int f(x) \mu(dx) = \sum_{y \in f(X)}y \cdot \mu(\bracs{f = y})
    \]

    is the \textbf{Lebesgue integral} of $f$.
\end{definition}

\begin{proposition}
\label{proposition:lebesgue-simple-properties}
    Let $(X, \cm, \mu)$ be a measure space and $f, g \in \Sigma^+(X, \cm)$, then:
    \begin{enumerate}
        \item For any $\alpha \ge 0$, $\int \alpha f d\mu = \alpha \int f d\mu$.
        \item $\int f + g d\mu = \int f d\mu + \int g d\mu$.
        \item If $f \le g$, then $\int f \le \int g$.
        \item The mapping $A \mapsto \int \one_A \cdot f d\mu$ is a measure on $(X, \cm)$.
    \end{enumerate}
\end{proposition}
\begin{proof}[Proof, {{\cite[Proposition 2.13]{Folland}}}. ]
    (1): If $\alpha = 0$, then $\int \alpha f d\mu = \int 0 d\mu = 0 = 0 \cdot \int f d\mu$. Otherwise, the mapping $y \mapsto \alpha y$ is a bijection. Hence
    \[
    \alpha f = \sum_{y \in f(X)} (\alpha y) \cdot \one_{\bracs{f = y}}
    \]

    is the standard form of $\alpha f$. Therefore
    \[
    \int \alpha f d\mu = \sum_{y \in f(X)}(\alpha y) \cdot \mu({\bracs{f = y}}) = \alpha \int f d\mu
    \]


    (2): Since $\mu$ is finitely additive,
    \begin{align*}
        \int f d\mu + \int g d\mu &= \sum_{y \in f(X)}y \cdot \mu(\bracs{f = y}) + \sum_{y \in g(X)}y \cdot \mu(\bracs{g = y}) \\
        &= \sum_{y \in f(X)}\sum_{z \in g(X)}(y + z) \cdot \mu(\bracs{f = y, g = z}) \\
        &= \sum_{y \in (f + g)(X)}\sum_{{z \in f(X) \atop {z' \in g(X) \atop z + z' = y}}}(z + z') \cdot \mu(\bracs{f = z, g = z'}) \\
        &= \sum_{y \in (f + g)(X)}y \cdot \mu(\bracs{f + g = y}) = \int f + g d\mu
    \end{align*}

    (3): Since $\mu$ is finitely additive,
    \begin{align*}
        \int f d\mu &= \sum_{y \in f(X)}y \cdot \mu(\bracs{f = y}) = \sum_{y \in f(X)}\sum_{z \in g(X)}y \cdot \mu(\bracs{f = y, g = z}) \\
        &\le \sum_{y \in f(X)}\sum_{z \in g(X)}z \cdot \mu(\bracs{f = y, g = z}) = \sum_{z \in g(X)}z \cdot \mu\paren{\bracs{g = z}} = \int g d\mu
    \end{align*}

    (4): Firstly, for any $A \in \cm$,
    \[
    \one_A \cdot f = \sum_{y \in f(X)}y \cdot \one_{A \cap \bracs{f = y}}
    \]

    so by (1),
    \[
    \int \one_A \cdot f d\mu = \sum_{y \in f(X)}y \cdot \mu(A \cap \bracs{f = y})
    \]

    Since $\mu$ is countably additive, for any $\seq{E_n} \subset \cm$ pairwise disjoint with $E = \bigcup_{n \in \natp}E_n$,
    \[
    \int \one_E \cdot f d\mu = \sum_{y \in f(X)}y \cdot \one_{E \cap \bracs{f = y}} = \sum_{y \in f(X)}\sum_{n \in \natp}y \cdot \one_{E_n \cap \bracs{f = y}} = \sum_{n \in \natp}\int \one_{E_n} \cdot f d\mu
    \]

\end{proof}
