Added localisable order completeness.

src/measure/measure/localisable.tex

@@ -199,4 +199,42 @@
     \end{enumerate}
 \end{proof}
 
+\begin{corollary}
+\label{corollary:l-infty-dedekind-complete}
+    Let $(X, \cm, \mu)$ be a localisable measure space, then $L^\infty(X; \real)$ is order complete. 
+\end{corollary}
+\begin{proof}
+    Let $\seqi{f} \subset L^\infty(X; \real)$ and $M \in \real$ such that $f_i \le M$ almost everywhere for all $i \in I$. 
 
+    Fix $A \in \cm$ with $\mu(A) < \infty$, and let
+    \[
+    \mathcal{S}_A = \bracs{g \in L^\infty(A; \real)| f_i|_A \le g \text{ almost everywhere }\forall i \in I}
+    \]
+
+    then since $f_i \le M$ almost everywhere for all $i \in I$, $\mathcal{S}_A \ne \emptyset$, and $m_A = \inf_{g \in \mathcal{S}_A}\int g d\mu \in \real$.
+    
+    Let $\seq{g_{A, n}} \subset \mathcal{S}_A$ such that $\seq{g_{A, n}}$ is decreasing pointwise and $\limv{n}\int_A g_{A, n} d\mu \downto m_A$. Take $g_A = \limv{n}g_{A, n}$, then by the \hyperref[Dominated Convergence Theorem]{theorem:dct}, $\int g_A d\mu = m_A$. 
+
+    For each $i \in I$, since $g_{A, n} \ge f_i|_A$ almost everywhere for all $n \in \natp$, $g_A \ge f_i|_A$ almost everywhere as well. Thus $g_A \in \mathcal{S}_A$. For any $h \in \mathcal{S}_A$, $g_A \wedge h \in \mathcal{S}_A$ with
+    \[
+    m_A \le \int_A g_A \wedge h d\mu \le \int_A g_A d\mu = m_A 
+    \]
+
+    Thus $g_A \wedge h = g_A$ almost everywhere, so $g_A \le h$ almost everywhere, and $g_A$ is an essential supremum of $\bracsn{f_i|_A}_{i \in I}$. 
+
+    Now, let $A, B \in \cm$ with $\mu(A), \mu(B) < \infty$, then $\one_{A \cap B} g_B + \one_{A \setminus B}M \in \mathcal{S}_A$, and
+    \[
+    m_A \le \int_A g_A \wedge (\one_{A \cap B} g_B + \one_{A \setminus B}M)d\mu \le \int_A g_A d\mu = m_A
+    \]
+
+    Thus $g_A \wedge (\one_{A \cap B} g_B + \one_{A \setminus B}M) = g_A$ almost everywhere, so $g_A|_{A \cap B} \le g_B|_{A \cap B}$ almost everywhere. As the argument is symmetric, $g_A|_{A \cap B} = g_B|_{A \cap B}$ almost everywhere. 
+
+    By the \hyperref[gluing lemma for measurable functions]{lemma:gluing-measurable}, there exists a measurable function $g:X \to \real$ such that $g|_A = g_A$ for all $A \in \cm$ with $\mu(A) < \infty$. 
+
+    Let $h \in L^\infty(X; \real)$ with $h \ge f_i$ almost everywhere for all $i \in I$, then for any $A \in \cm$ with $\mu(A) < \infty$, 
+    \[
+    \mu(\bracs{h < g} \cap A) \le \mu(\bracs{h|_A < g_A} \cup \bracs{g|_A \ne g_A}) = 0
+    \]
+    
+    As $\mu$ is semifinite, $\mu(\bracs{h < g}) = 0$. Finally, since $g_A \le M$ almost everywhere for all $A \in \cm$ with $\mu(A) < \infty$, $g \le M$ almost everywhere. Therefore $g \in L^\infty(X; \real)$ is indeed the essential supremum of $\seqi{f}$. 
+\end{proof}

src/measure/measure/scaffold.tex

@@ -3,10 +3,12 @@
 
 \begin{definition}[Scaffold*]
 \label{definition:measure-scaffold}
-    Let $(X, \cm, \mu)$ be a measure space and $\cf \subset \bracs{A \in \cm|\mu(A) < \infty}$ be an ideal, then $\cf$ is a \textbf{scaffold} for $\mu$ if for all $E \in \cm$, 
-    \[
-    \mu(E) = \sup\bracs{\mu(E \cap A)|A \in \cf}
-    \]
+    Let $(X, \cm, \mu)$ be a measure space and $\cf \subset \cm$, then $\cf$ is a \textbf{scaffold} for $\mu$ if:
+    \begin{enumerate}[label=(S\arabic*)]
+        \item For each $A \in \cf$, $\mu(A) < \infty$. 
+        \item For all $E \in \cm$, $\mu(E) = \sup\bracs{\mu(E \cap A)|A \in \cf}$. 
+        \item For any $A, B \in \cf$, $A \cup B \in \cf$. 
+    \end{enumerate}
 
     and the quadruple $(X, \cm, \cf, \mu)$ is a \textbf{scaffolded measure space}. 
 
@@ -21,10 +23,11 @@
 
 \begin{lemma}[Gluing Lemma for Measures]
 \label{lemma:gluing-measure}
-    Let $(X, \cm)$ be a measurable space, $\cf \subset \cm$ be an ideal, and $\bracsn{\mu_A}_{A \in \cf}$ such that:
+    Let $(X, \cm)$ be a measurable space, $\cf \subset \cm$, and $\bracsn{\mu_A}_{A \in \cf}$ such that:
     \begin{enumerate}[label=(\alph*)]
         \item For each $A \in \cf$, $\mu_A$ is a finite measure on $A$.
         \item For each $A, B \in \cf$ and $E \in \cm$, $\mu_A(E \cap A \cap B) = \mu_B(E \cap A \cap B)$. 
+        \item For each $A, B \in \cf$, $A \cup B \in \cf$. 
     \end{enumerate}
 
     Let

src/measure/vector/rn-draft.tex

@@ -50,7 +50,7 @@
     &= \sup_{A \in \cf}\braks{\int_{A \cap E}f_A d\mu + \nu_s^A(A \cap E)}
     \end{align*}
 
-    As $\cf$ is an ideal, for any $A, B \in \cf$, $A \cup B \in \cf$, and
+    By (S3), for any $A, B \in \cf$, $A \cup B \in \cf$, and
     \begin{align*}
         \int_{A \cap E}f_A d\mu \vee \int_{B \cap E}f_B d\mu &\le \int_{(A \cup B) \cap E}f_{A \cup B} d\mu \\
         \nu_s^A(A \cap E) \vee \nu_s^B(B \cap E) &\le \nu_s^{A \cup B}((A \cup B) \cap E)