From 242c7ebea1e871c3a81232ead650183d31a25863 Mon Sep 17 00:00:00 2001
From: Bokuan Li <bokuan.li@mail.mcgill.ca>
Date: Sat, 20 Jun 2026 09:48:01 -0400
Subject: [PATCH] Updated the Lebesgue non-negative integral formula.

---
 .../lebesgue-integral/non-negative.tex        | 35 ++++++++++++++-----
 src/measure/lebesgue-integral/simple.tex      |  4 +--
 2 files changed, 28 insertions(+), 11 deletions(-)

diff --git a/src/measure/lebesgue-integral/non-negative.tex b/src/measure/lebesgue-integral/non-negative.tex
index aed2bb5..445e1b3 100644
--- a/src/measure/lebesgue-integral/non-negative.tex
+++ b/src/measure/lebesgue-integral/non-negative.tex
@@ -5,10 +5,10 @@
 \label{definition:measurable-non-negative}
     Let $(X, \cm)$ be a measure space, then
     \[
-    \mathcal{L}^+(X, \cm) = \bracs{f: X \to \real| f \ge 0, f \text{ is } (\cm, \cb_\real) \text{-measurable}}
+    \mathcal{L}^+(X, \cm) = \bracs{f: X \to [0, \infty]| f \ge 0, f \text{ is } (\cm, \cb_\real) \text{-measurable}}
     \]
 
-    is the space of non-negative $\real$-valued measurable functions on $(X, \cm)$.
+    is the space of non-negative $\ol \real$-valued measurable functions on $(X, \cm)$.
 \end{definition}
 
 \begin{definition}[Integral of Non-Negative Function]
@@ -23,19 +23,36 @@
 
 \begin{lemma}
 \label{lemma:lebesgue-non-negative-strict}
-    Let $(X, \cm, \mu)$ be a measure space and $f \in \mathcal{L}^+(X, \cm)$, then
-    \[
-    \int f d\mu = \sup\bracs{\int \phi d\mu \bigg | \phi \in \Sigma^+(X, \cm), \phi|_{\bracs{f > 0}} < f|_{\bracs{f > 0}}, \phi \le f}
-    \]
+    Let $(X, \cm, \mu)$ be a measure space and $f \in \mathcal{L}^+(X, \cm)$. 
+    \begin{enumerate}
+        \item For each $\phi \in \Sigma^+(X, \cm)$, denote $\phi \le_u f$ if there exists $\delta > 0$ such that $\phi + \delta \ge f$ on $\bracs{\phi > 0}$, then
+        \[
+        \int f d\mu = \sup\bracs{\int \phi d\mu \bigg | \phi \in \Sigma^+(X, \cm), \phi \le_u f}
+        \]
 
+        \item If $\mu$ is semifinite, then
+        \[
+        \int f d\mu = \sup\bracs{\int \phi d\mu \bigg | \phi \in \Sigma^+(X, \cm) \cap L^1(X; \real), \phi \le_u f}
+        \]
+    \end{enumerate}
 \end{lemma}
 \begin{proof}
-    Let $\phi \in \Sigma^+(X, \cm)$ with $\phi \le f$, then for any $\alpha \in (0, 1)$, $\alpha \phi|_{\bracs{f > 0}} < f|_{\bracs{f > 0}}$. Since
+    (1): Let $\phi \in \Sigma^+(X, \cm)$ with $\phi \le f$ and $\alpha \in (0, 1)$. Since $\phi(X) \setminus \bracs{0} \subset (0, \infty)$ is finite, $\delta = \min_{y \in \phi(X) \setminus \bracs{0}}(1 - \alpha)y > 0$. Thus $\alpha \phi + \delta \le \phi \le f$ on $\bracs{\phi > 0} = \bracs{\alpha \phi > 0}$, and $\alpha \phi \le_u f$. 
+    
+    By \hyperref[linearity on simple functions]{proposition:lebesgue-simple-properties}, 
     \[
     \int \phi d\mu = \sup_{\alpha \in (0, 1)}\alpha \int \phi d\mu = \sup_{\alpha \in (0, 1)}\int \alpha \phi d\mu
     \]
 
-    the two sides are equal.
+    Thus
+    \[
+    \int \phi d\mu \le \sup\bracs{\int \psi d\mu \bigg | \psi \in \Sigma^+(X, \cm), \psi \le_u f}
+    \]
+
+    As the above holds for all $\phi \in \Sigma^+(X, \cm)$, 
+    \[
+    \int f d\mu = \sup\bracs{\int \psi d\mu \bigg | \psi \in \Sigma^+(X, \cm), \psi \le_u f}
+    \]
 \end{proof}
 
 \begin{theorem}[Monotone Convergence Theorem]
@@ -98,7 +115,7 @@
 \begin{proof}
     (1): By \autoref{lemma:lebesgue-simple-monotone}, there exists $\seq{f_n}, \seq{g_n} \subset \Sigma^+(X, \cm)$ with $0 \le f_n \le f$ and $0 \le g_n \le g$ for each $n \in \natp$, $f_n \upto f$, and $g_n \upto g$. By \autoref{proposition:lebesgue-simple-properties} and the \hyperref[Monotone Convergence Theorem]{theorem:mct},
     \begin{align*}
-    \int \alpha f + g d\mu = \limv{n}\int \alpha f_n + g_n d\mu = \alpha\limv{n}\int f_n d\mu + \limv{n}\int g_n d\mu \\
+    \int \alpha f + g d\mu &= \limv{n}\int \alpha f_n + g_n d\mu = \alpha\limv{n}\int f_n d\mu + \limv{n}\int g_n d\mu \\
     &= \alpha \int f d\mu + \int g d\mu
     \end{align*}
 
diff --git a/src/measure/lebesgue-integral/simple.tex b/src/measure/lebesgue-integral/simple.tex
index 53c8769..bbae250 100644
--- a/src/measure/lebesgue-integral/simple.tex
+++ b/src/measure/lebesgue-integral/simple.tex
@@ -16,7 +16,7 @@
     is the \textbf{Lebesgue integral} of $f$.
 \end{definition}
 
-\begin{proposition}[{{\cite[Proposition 2.13]{Folland}}}]
+\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}
@@ -26,7 +26,7 @@
         \item The mapping $A \mapsto \int \one_A \cdot f d\mu$ is a measure on $(X, \cm)$.
     \end{enumerate}
 \end{proposition}
-\begin{proof}
+\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}}