Added vector lattices.

src/measure/lebesgue-integral/complex.tex

@@ -28,7 +28,7 @@
 \label{definition:positive-negative-parts}
     Let $X$ be a set and $f: X \to \real$ be a function, then
     \[
-    f^+ = \max(f, 0) \quad f^- = -\min(f, 0)
+    f^+ = f \vee 0 \quad f^- = -(f \wedge 0)
     \]
 
     are the \textbf{positive} and \textbf{negative} parts of $f$, and $f = f^+ - f^-$.
@@ -56,27 +56,14 @@
     Let $(X, \cm, \mu)$ be a measure space, then the integral is a linear functional on $\mathcal{L}^1(X)$ such that for any $f \in \mathcal{L}^1(X)$, $\abs{\int f d\mu} \le \int \abs{f}d\mu$.
 \end{proposition}
 \begin{proof}
-    Let $f, g \in \mathcal{L}^1(X)$ and $\lambda \in \complex$. First suppose that $f, g$ are $\real$-valued and $\lambda \in \real$. In which case,
+    By \autoref{lemma:positive-functional-extension}, the mapping
     \[
-    \int \lambda f d\mu = \int (\lambda f)^+ d\mu - \int (\lambda f)^- d\mu
-    = \begin{cases}
-        \lambda\int f^+ d\mu - \lambda\int f^- d\mu &\lambda \ge 0 \\
-        -\lambda\int f^- d\mu + \lambda\int f^+ d\mu &\lambda < 0
-    \end{cases}
+    I: \mathcal{L}^1(X; \real) \to \real \quad f \mapsto \int f^+ d\mu - \int f^- d\mu
     \]
 
-    by \autoref{proposition:lebesgue-non-negative-properties}, so $\int \lambda f d\mu = \lambda \int f d\mu$.
+    is a $\real$-linear functional on $\mathcal{L}^1(X; \real)$. 
 
-    Let $h = f + g$, then $h = h^+ - h^- = f^+ + g^+ - f^- - g^-$, so
-    \begin{align*}
-        h^+ + f^- + g^- &= h^- + f^+ + g^+ \\
-        \int h^+d\mu + \int f^- d\mu + \int g^-d\mu &= \int h^- d\mu + \int f^+ d\mu + \int g^+ d\mu \\
-        \int h^+ d\mu - \int h^- d\mu &= \int f^+ d\mu - \int f^- d\mu + \int g^+ d\mu - \int g^- d\mu \\
-        &= \int f d\mu + \int g d\mu
-    \end{align*}
-    by \autoref{proposition:lebesgue-non-negative-properties}, so $\int f + g d\mu = \int f d\mu + \int g d\mu$.
-
-    Now suppose that $f, g$ are $\complex$-valued and $\lambda = \alpha + \beta i \in \complex$ with $\alpha, \beta \in \real$, then
+    Let $f, g \in L^1(X; \complex)$ and $\lambda = \alpha + \beta i \in \complex$ with $\alpha, \beta \in \real$, then
     \begin{align*}
         \int (\alpha f)d\mu &= \int \text{Re}(\lambda f)d\mu + i\int \text{Im}(\lambda f)d\mu \\
         &= \int \alpha \text{Re}(f) - \beta \text{Im}(f)d\mu + i\int \beta\text{Re}(f) + \alpha \text{Im}(f)d\mu \\