Added integration of simple functions.

src/measure/lebesgue-integral/simple.tex

@@ -0,0 +1,64 @@
+\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\footnote{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}[{{\cite[Proposition 2.13]{Folland}}}]
+\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}
+    (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}