Updated the Lebesgue non-negative integral formula.

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*}