From 2e81d6f87a0cfc430ed1eacec6b49eec5831675d Mon Sep 17 00:00:00 2001
From: Bokuan Li <bokuan.li@mail.mcgill.ca>
Date: Thu, 22 Jan 2026 11:36:14 -0500
Subject: [PATCH] Added integration of simple functions.

---
 src/measure/lebesgue-integral/index.tex       |  2 +-
 .../lebesgue-integral/non-negative.tex        |  0
 src/measure/lebesgue-integral/simple.tex      | 64 +++++++++++++++++++
 src/measure/measurable-maps/simple.tex        |  2 +-
 4 files changed, 66 insertions(+), 2 deletions(-)
 create mode 100644 src/measure/lebesgue-integral/non-negative.tex
 create mode 100644 src/measure/lebesgue-integral/simple.tex

diff --git a/src/measure/lebesgue-integral/index.tex b/src/measure/lebesgue-integral/index.tex
index abacd27..e8e2c57 100644
--- a/src/measure/lebesgue-integral/index.tex
+++ b/src/measure/lebesgue-integral/index.tex
@@ -1,4 +1,4 @@
 \chapter{The Lebesgue Integral}
 \label{chap:lebesgue-integral}
 
-%\input{./src/measure/lebesgue-integral/simple.tex}
+\input{./src/measure/lebesgue-integral/simple.tex}
diff --git a/src/measure/lebesgue-integral/non-negative.tex b/src/measure/lebesgue-integral/non-negative.tex
new file mode 100644
index 0000000..e69de29
diff --git a/src/measure/lebesgue-integral/simple.tex b/src/measure/lebesgue-integral/simple.tex
new file mode 100644
index 0000000..5e1b508
--- /dev/null
+++ b/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}
diff --git a/src/measure/measurable-maps/simple.tex b/src/measure/measurable-maps/simple.tex
index fd81329..6da479b 100644
--- a/src/measure/measurable-maps/simple.tex
+++ b/src/measure/measurable-maps/simple.tex
@@ -30,5 +30,5 @@
     \]
     is the \textbf{standard form} of $f$.
 
-    The set $\Sigma(X, \cm, V)$ is the vector space of all simple functions from $X$ to $Y$.
+    The set $\Sigma(X, \cm; V)$ is the space of $V$-valued simple functions on $(X, \cm)$, which forms a vector space.
 \end{definition}