Fixed typos in the gluing lemma.

src/fa/lp/ui.tex

@@ -48,7 +48,7 @@
 
 \begin{theorem}[Vitali Convergence Theorem]
 \label{theorem:vitali-convergence}
-    Let $(X, \cm, \mu)$ be a measure space, $p \in [1, \infty)$, $E$ be a separable normed vector space over $K \in \RC$, and $\fF \subset 2^{L^p(X; E)}$ be a filter, then $\fF$ is Cauchy in $L^p(X; E)$ if and only if:
+    Let $(X, \cm, \mu)$ be a measure space, $p \in [1, \infty)$, $E$ be a normed vector space over $K \in \RC$, and $\fF \subset 2^{L^p(X; E)}$ be a filter, then $\fF$ is Cauchy in $L^p(X; E)$ if and only if:
     \begin{enumerate}
         \item[(M)] $\fF$ is locally Cauchy in measure. 
         \item[(UI)] For each $\eps > 0$, there exists $M \ge 0$ and $F \in \fF$ such that
@@ -142,7 +142,7 @@
 
 \begin{corollary}[Dominated Convergence Theorem (In Measure)]
 \label{corollary:dct-filter}
-    Let $(X, \cm, \mu)$ be a measure space, $p \in [1, \infty)$, $E$ be a separable normed vector space over $K \in \RC$, $\fF \subset 2^{L^p(X; E)}$ be a filter, and $g, h \in L^p(X; \real)$ such that:
+    Let $(X, \cm, \mu)$ be a measure space, $p \in [1, \infty)$, $E$ be a normed vector space over $K \in \RC$, $\fF \subset 2^{L^p(X; E)}$ be a filter, and $g, h \in L^p(X; \real)$ such that:
     \begin{enumerate}[label=(\alph*)]
         \item[(M)] $\fF \to g$ locally in measure.
         \item[(D)] There exists $F \in \fF$ such that $|f| \le h$ for all $f \in F$. 

src/measure/bochner-integral/strongly.tex

@@ -24,7 +24,7 @@
 
     By the separable case, $f$ is $(\cm, \cb_{F})$-measurable. Let $B \in \cb_E$, then $B \cap F \in \cb_F$ by \autoref{lemma:borel-induced}. Therefore $\bracs{f \in B} = \bracs{f \in B \cap F} \in \cm$, and $f$ is $(\cm, \cb_E)$-measurable. 
 
-    (2) $\Rightarrow$ (3): By \autoref{proposition:measurable-simple-separable-norm}.
+    (2) $\Rightarrow$ (3): By \autoref{corollary:measurable-simple-separable-norm}.
 
     (3) $\Rightarrow$ (1): For each $\phi \in E^*$, $\phi \circ f = \limv{n}\phi \circ f_n$ is measurable by \autoref{proposition:limit-measurable}. Since
     \[

src/measure/lebesgue-integral/non-negative.tex

@@ -96,7 +96,7 @@
     Let $(X, \cm)$ be a measurable space and $f \in \mathcal{L}^+(X, \cm)$, then there exists $\seq{f_n} \subset \Sigma^+(X, \cm)$ such that $f_n \upto f$ pointwise.
 \end{lemma}
 \begin{proof}
-    By \autoref{proposition:measurable-simple-separable-norm}, there exists $\seq{g_n} \subset \Sigma^+(X, \cm)$ such that $0 \le g_n \le f$ for each $n \in \natp$, and $g_n \to f$ pointwise. For each $n \in \natp$, let $f_n = \max_{1 \le k \le n}g_k$, then $f_n \in \Sigma^+(X, \cm)$, $0 \le f_n \le f$, and $f_n \upto f$ pointwise.
+    By \autoref{corollary:measurable-simple-separable-norm}, there exists $\seq{g_n} \subset \Sigma^+(X, \cm)$ such that $0 \le g_n \le f$ for each $n \in \natp$, and $g_n \to f$ pointwise. For each $n \in \natp$, let $f_n = \max_{1 \le k \le n}g_k$, then $f_n \in \Sigma^+(X, \cm)$, $0 \le f_n \le f$, and $f_n \upto f$ pointwise.
 \end{proof}
 
 

src/measure/measurable-maps/approx.tex

@@ -0,0 +1,163 @@
+\section{Approximations with Simple Functions}
+\label{section:simple-approx}
+
+\begin{definition}[Admissible Approximant Function]
+\label{definition:admissible-approximant-function}
+    Let $X$ be a topological space and $\mathcal{A}: X \to 2^X$, then $\mathcal{A}$ is an \textbf{admissible approximant function} on $X$ if:
+    \begin{enumerate}[label=(AA\arabic*)]
+        \item For each $x \in X$, $x \in \overline{\mathcal{A}(x)^o}$. 
+        \item $\bigcap_{x \in X}\mathcal{A}(x) \ne \emptyset$. 
+    \end{enumerate}
+
+    and $\mathcal{A}$ is \textbf{Borel measurable} if:
+    \begin{enumerate}[label=(AA\arabic*), start=2]
+        \item[(B)] For any $x_0 \in X$, $\bracs{x \in X|x_0 \in \mathcal{A}(x)} \in \cb_X$.
+    \end{enumerate}
+\end{definition}
+
+\begin{lemma}
+\label{lemma:admissible-approximant-existence}
+    Let $X$ be a topological space, and $\mathcal{A}: X \to 2^X$ be defined by $x \mapsto X$, then $\mathcal{A}$ is an \hyperref[admissible approximant function]{definition:admissible-approximant-function}. 
+\end{lemma}
+
+
+\begin{definition}[Approximation of the Identity]
+\label{definition:approximation-id-measure}
+    Let $X$ be a topological space, $\mathcal{A}: X \to 2^X$ be an \hyperref[admissible approximant function]{definition:admissible-approximant-function} and $\net{I} \subset X^X$ be a net, then $\net{I}$ is an \textbf{$\mathcal{A}$-admissible approximation of the identity} if:
+    \begin{enumerate}[label=(AI\arabic*)]
+        \item For each $x \in X$, $I_\alpha(x) \to x$. 
+        \item For each $x \in X$ and $\alpha \in A$, $I_\alpha(x) \in \mathcal{A}(x)$. 
+    \end{enumerate}
+
+    The approximation $\net{I}$ is \textbf{simple} if $I_\alpha$ is finitely-valued for all $\alpha \in A$, and \textbf{Borel measurable} if $I_\alpha$ is Borel measurable for all $\alpha \in A$. 
+\end{definition}
+
+\begin{lemma}[Existence of Simple Approximations of the Identity]
+\label{lemma:separable-metric-space-approx-identity}
+    Let $X$ be a separable and metrisable topological space, $\mathcal{A}: X \to 2^X$ be a Borel measurable \hyperref[admissible approximant function]{definition:admissible-approximant-function}, and $\seq{x_n} \subset X$ be a dense subset with $x_1 \in \bigcap_{x \in X}\mathcal{A}(x)$, then there exists $\seq{I_n} \subset X^X$ such that:
+    \begin{enumerate}
+        \item $\seq{I_n}$ is an $\mathcal{A}$-admissible \hyperref[approximation of the identity]{definition:approximation-id-measure}. 
+        \item For each $N \in \natp$, $I_N$ is Borel measurable with $I_N(X) \subset \bracsn{x_n|1 \le n \le N}$. 
+        \item For each $n \in \natp$ and $x \in X$, $d(x, I_{n+1}(x)) \le d(x, I_n(x))$. 
+    \end{enumerate}
+\end{lemma}
+\begin{proof}
+    By removing duplicate elements from the sequence, assume without loss of generality that for each $m, n \in \natp$ with $m \ne n$, $x_m \ne x_n$. 
+
+    Let $N \in \natp$. For each $x \in X$, let
+    \[
+    C_N(x) = \bracs{1 \le n \le N| x_n \in \mathcal{A}(x)}
+    \]
+
+    Since $x_1 \in \bigcap_{y \in X}\mathcal{A}(y)$, $1 \in C_N(x)$ and $C_N(x) \ne \emptyset$. 
+    
+    Fix a metric $d: Y \times Y \to [0, \infty)$ and let
+    \[
+    k_N(x) = \min\bracs{n \in C_N(x) \bigg | d(x, x_n) = \min_{m \in C_N(x)}d(x, x_m)}
+    \]
+
+    be the minimum $n \in C_N(x)$ on which the minimal distance from $x$ to $\bracs{x_m|m \in C_N(x)}$ is achieved. Then, for each $n \in \natp$, 
+    \begin{align*}
+        \bracs{k_N \le n} &= \bigcup_{j = 1}^n \bracs{x \in X \bigg | j \in C_N(x), d(x, x_j) = \min_{m \in C_N(x)}d(x, x_m)} \\
+        &= \bigcup_{j = 1}^n \bracs{j \in C_N} \cap \bracs{x \in X \bigg | d(x, x_j) = \min_{m \in C_N(x)}d(x, x_m)} \\
+        &= \bigcup_{j = 1}^n\bigcup_{J \subset [N]} \bracs{j \in C_N, J = C_N} \cap \bracs{x \in X \bigg | d(x, x_j) = \min_{m \in J}d(x, x_m)} 
+    \end{align*}
+
+    Given that $\mathcal{A}$ is Borel measurable, $\bracs{n \in C_N} = \bracs{x_n \in \mathcal{A}(x)}$ is a Borel set for each $1 \le n \le N$. As a result, $\bracs{J = C_N}$ is Borel for each $J \subset [N]$. Thus $\bracs{j \in C_N, J = C_N}$ is Borel for each $1 \le j \le n$ and $J \subset [N]$. 
+
+    On the other hand, for each $1 \le n \le N$, the function $x \mapsto d(x, x_n)$ is continuous and hence Borel measurable. Similarly, for each $J \subset [N]$, the mapping $\real^J \to \real$ with $\alpha \mapsto \min_{j \in J}\alpha_j$ is also Borel measurable. 
+    
+    
+    The above facts combined show that $\bracs{k_N \le n}$ is a Borel set, and $k_N: X \to [N]$ is a Borel measurable function. Now, let
+    \[
+    I_N: X \to \bracsn{x_n|1 \le n \le N} \quad x \mapsto x_{k_N(x)}
+    \]
+
+    then for each $1 \le n \le N$, $\bracs{I_N = x_n} = \bracs{k_N = n}$ is a Borel set. Thus $I_N$ is Borel measurable. 
+
+    In addition, for each $x \in X$, $k_N(x) \in C_N(x)$, so
+    \[
+    I_N(x) = x_{k_N(x)} \in \bracs{x_n|n \in C_N(x)} \subset \mathcal{A}(x)
+    \]
+
+    and $\seq{I_N}$ satisfies (AI2).
+
+    Finally, for each $x \in X$ and $\eps > 0$, since $x \in \ol{\mathcal{A}(x)^o}$, there exists $N_0 \in \natp$ such that $x_{N_0} \in \mathcal{A}(x)$ and $d(x, x_{N_0}) < \eps$. In which case, for any $N \ge N_0$, $N_0 \in C_N(x)$ and $d(x, I_N(x)) \le d(x, x_{N_0}) < \eps$. Thus $I_N(x) \to x$ as $N \to \infty$, and $\seq{I_N}$ satisfies (AI1). 
+    
+    Therefore $\seq{I_N}$ is an approximation of the identity satisfying (1)-(3). 
+\end{proof}
+
+
+
+\begin{corollary}
+\label{corollary:measurable-simple-separable}
+    Let $(X, \cm)$ be a measurable space, $Y$ be a separable and metrisable topological space, and $\mathcal{A}: Y \to 2^Y$ be a Borel measurable \hyperref[admissible approximant function]{definition:admissible-approximant-function}, then for any $f: X \to Y$, the following are equivalent:
+    \begin{enumerate}
+        \item $f$ is $(\cm, \cb_Y)$-measurable.
+        \item For any dense subset $\seq{y_n} \subset Y$ with $y_1 \in \bigcap_{y \in Y}\mathcal{A}(y)$, there exists a sequence $\seq{f_n}$ of $(\cm, \cb_Y)$-measurable simple functions such that
+        \begin{enumerate}
+            \item[(i)] For each $x \in X$ and $N \in \natp$,
+            \[
+            f_N(x) \in \mathcal{A}(f(x)) \cap \bracsn{y_n|1 \le n \le N}
+            \]
+            \item[(ii)] $f_n \to f$ pointwise as $n \to \infty$.
+        \end{enumerate}
+
+        \item There exists a sequence $\seq{f_n}$ of $(\cm, \cb_Y)$-measurable simple functions such that $f_n \to f$ pointwise.
+    \end{enumerate}
+\end{corollary}
+\begin{proof}
+    (1) $\Rightarrow$ (2): Let $\seq{y_n} \subset Y$ be a dense subset with $y_1 \in \bigcap_{y \in Y}\mathcal{A}(y)$. By \autoref{lemma:separable-metric-space-approx-identity}, there exists $\seq{I_n} \subset Y^Y$ such that:
+    \begin{enumerate}
+        \item $\seq{I_n}$ is an $\mathcal{A}$-admissible \hyperref[approximation of the identity]{definition:approximation-id-measure}. 
+        \item For each $N \in \natp$, $I_N$ is Borel measurable with $I_N(Y) \subset \bracsn{y_n|1 \le n \le N}$. 
+    \end{enumerate}
+
+    For each $n \in \natp$, let $f_n = I_N \circ f_n$, then:
+    \begin{enumerate}
+        \item[(i)] For each $x \in X$ and $N \in \natp$,
+        \[
+        f_N(x) = I_N(f(x)) \in \mathcal{A}(f(x)) \cap \bracsn{y_n|1 \le n \le N}
+        \]
+        \item[(ii)] Since $I_n \to \text{Id}$ pointwise as $n \to \infty$, $f_n \to f$ pointwise as $n \to \infty$. 
+    \end{enumerate}
+
+    (3) $\Rightarrow$ (1): By \autoref{proposition:metric-measurable-limit}.
+\end{proof}
+
+\begin{corollary}
+\label{corollary:measurable-simple-separable-norm}
+    Let $(X, \cm)$ be a measurable space, $(E, \norm{\cdot}_E)$ be a separable normed vector space, and $f: X \to E$, then the following are equivalent:
+    \begin{enumerate}
+        \item $f$ is $(\cm, \cb_E)$-measurable.
+        \item There exists simple functions $\seq{f_n}$ such that $\abs{f_n} \le \abs{f}$ for all $n \in \natp$, and $f_n \to f$ pointwise.
+    \end{enumerate}
+\end{corollary}
+\begin{proof}
+    (1) $\Rightarrow$ (2): Let
+    \[
+    \mathcal{A}: E \to 2^E \quad y \mapsto \begin{cases}
+        B_E(0, \norm{y}_E) & y \ne 0 \\ 
+        E & y = 0
+    \end{cases}
+    \]
+
+    then
+    \begin{enumerate}
+        \item[(AA1)] For each $y \in E$, $y \in \ol{\mathcal{A}(y)^o}$.
+        \item[(AA2)] $0 \in \bigcap_{y \in E}\mathcal{A}(y)$.
+        \item[(B)] For any fixed $y_0 \in E \setminus \bracs{0}$,
+        \[
+        \bracs{y \in E|y_0 \in \mathcal{A}(y)} = \bracs{y \in E|\norm{y_0}_E < \norm{y}_E} \cup \bracs{0} \in \cb_E
+        \]
+
+        and $\bracs{y \in E|0 \in \mathcal{A}(y)} = E$. 
+    \end{enumerate}
+
+    so $\mathcal{A}$ is a Borel measurable \hyperref[admissible approximant function]{definition:admissible-approximant-function}. 
+
+    By (2) of \autoref{corollary:measurable-simple-separable}, there exists simple functions $\seq{f_n}$ such that $|f_n| \le |f|$ on $\bracs{f \ne 0}$ for all $n \in \natp$ and $f_n \to f$ pointwise. In which case, $|\one_{\bracs{f \ne 0}}f_n| \le |f|$ globally for all $n \in \natp$ and $\one_{\bracs{f \ne 0}}f_n \to f$ pointwise as $n \to \infty$. 
+
+    (2) $\Rightarrow$ (1): By \autoref{proposition:metric-measurable-limit}.
+\end{proof}
+

src/measure/measurable-maps/index.tex

@@ -6,4 +6,5 @@
 \input{./real-valued.tex}
 \input{./simple.tex}
 \input{./metric.tex}
+\input{./approx.tex}
 \input{./in-measure.tex}

src/measure/measurable-maps/metric.tex

@@ -21,7 +21,7 @@
 
 \begin{proposition}
 \label{proposition:metric-measurables}
-    Let $(X, \cm)$ be a measurable space, $Y$ be a metrisable topological space, $f, g: X \to Y$ be $(\cm, \cb_Y)$-measurable functions, then the following functions are measurable:
+    Let $(X, \cm)$ be a measurable space, $Y$ be a separable and metrisable topological space, $f, g: X \to Y$ be $(\cm, \cb_Y)$-measurable functions, then the following functions are measurable:
     \begin{enumerate}
         \item For any metric $d$ on $Y$, $x \mapsto d(f(x), f(y))$.
         \item If $Y$ is a TVS over $K \in \RC$ and $\lambda \in K$, $\lambda f + g$. In particular, $\bracs{f = g} \in \cm$.
@@ -53,7 +53,7 @@
 \label{proposition:metric-measurable-limit}
     Let $(X, \cm)$ be a measurable space, $Y$ be a metrisable topological space, and $\seq{f_n}$ be $(\cm, \cb_Y)$-measurable functions, then:
     \begin{enumerate}
-        \item If $Y$ is completely metrisable, then $\bracsn{\limv{n}f_n \text{ exists}} \in \cm$.
+        \item If $Y$ is Polish, then $\bracsn{\limv{n}f_n \text{ exists}} \in \cm$.
         \item If $f = \limv{n}f_n$ exists, then it is $(\cm, \cb_Y)$-measurable.
     \end{enumerate}
 \end{proposition}
@@ -69,86 +69,3 @@
 \end{proof}
 
 
-\begin{proposition}
-\label{proposition:measurable-simple-separable}
-    Let $(X, \cm)$ be a measurable space, $Y$ be a separable metric space, and $N: Y \to 2^Y$ such that
-    \begin{enumerate}
-        \item[(a)] For each $y \in Y$, $y \in \ol{N(y)^o}$.
-        \item[(b)] $\bigcap_{y \in Y}N(y) \ne \emptyset$.
-        \item[(c)] For any $y_0 \in Y$, $\bracs{y \in Y|y_0 \in N(y)} \in \cb_Y$.
-    \end{enumerate}
-
-    Then, for any $f: X \to Y$, the following are equivalent:
-    \begin{enumerate}
-        \item $f$ is $(\cm, \cb_Y)$-measurable.
-        \item There exists a sequence $\seq{f_n}$ of $(\cm, \cb_Y)$-measurable simple functions such that
-        \begin{enumerate}
-            \item[(i)] For each $x \in X$ and $n \in \natp$, $f_n(x) \in N(f(x))$.
-            \item[(ii)] $f_n \to f$ pointwise.
-        \end{enumerate}
-
-        \item There exists a sequence $\seq{f_n}$ of $(\cm, \cb_Y)$-measurable simple functions such that $f_n \to f$ pointwise.
-    \end{enumerate}
-\end{proposition}
-\begin{proof}
-    (1) $\Rightarrow$ (2): Let $\seq{y_n} \subset Y$ be a dense subset of $Y$. Assume without loss of generality that $y_1 \in \bigcap_{y \in Y}N(y)$. For each $N \in \nat$ and $x \in X$, let
-    \[
-    C(N, x) = \bracs{1 \le n \le N|y_n \in N(f(x))}
-    \]
-
-    By assumption (b), $1 \in C(N, x) \ne \emptyset$. Let
-    \[
-    k(N, x) = \min\bracs{n \in C(N, x) \bigg | d(f(x), y_n) = \min_{m \in C(N, x)}d(f(x), y_m)}
-    \]
-
-    then for any $k \in \natp$, $\bracs{x \in X|k(n, x) \le k}$ is equal to
-    \[
-     \bigcup_{j = 1}^k\bracs{x \in X \bigg |y_j \in C(n, x), d(f(x), y_j) = \min_{m \in C(N, x)}d(f(x), y_m)}
-    \]
-
-    For each $1 \le m \le N$, $y \mapsto d(y, y_m)$ is continuous. Thus $x \mapsto d(f(x), y_m)$ and $x \mapsto \min_{m \in C(N, x)}d(f(x), y_m)$ are $(\cm, \cb_\real)$-measurable by \autoref{proposition:limit-measurable} and assumption (c). By \autoref{proposition:metric-measurables},
-    \[
-    \bracs{x \in X \bigg | d(f(x), y_j) = \min_{m \in C(N, x)}d(f(x), y_m)} \in \cm
-    \]
-
-    for each $1 \le j \le k$. Combining this with assumption (c) shows that $\bracs{x \in X|k(n, x) \le k} \in \cm$.
-
-    Let $f_N(x) = y_{k(N, x)}$, then for each $N \in \natp$, $f_N(x) \subset \bracs{y_n|1 \le n \le N}$, so $f_N(x)$ is finitely valued. Since $x \mapsto k{(N, x)}$ is $(\cm, 2^\nat)$-measurable, $f_N$ is $(\cm, \cb_Y)$-measurable.
-
-    Fix $x \in X$, then
-    \[
-    f(x) \in \ol{N^o(f(x))} = \ol{\bracs{y_n| n \in \natp, y_n \in N^o(f(x))}}
-    \]
-
-    by assumption (a) and \autoref{definition:dense}. Thus for any $\eps > 0$, there exists $N \in \nat$ such that $y_N \in N^o(f(x))$ and $d(f(x), y_N) < \eps$. In which case, $d(f(x), f_n(x)) < \eps$ for all $n \ge N$. Therefore $f_n \to f$ pointwise.
-
-    (3) $\Rightarrow$ (1): By \autoref{proposition:metric-measurable-limit}.
-\end{proof}
-
-\begin{proposition}
-\label{proposition:measurable-simple-separable-norm}
-    Let $(X, \cm)$ be a measurable space, $(E, \norm{\cdot}_E)$ be a separable normed vector space, and $f: X \to E$, then the following are equivalent:
-    \begin{enumerate}
-        \item $f$ is $(\cm, \cb_E)$-measurable.
-        \item There exists simple functions $\seq{f_n}$ such that $\abs{f_n} \le \abs{f}$ for all $n \in \natp$, and $f_n \to f$ pointwise.
-    \end{enumerate}
-\end{proposition}
-\begin{proof}
-    Let
-    \[
-    N: E \to 2^E \quad y \mapsto B_E(0, \norm{y}_E)
-    \]
-
-    then
-    \begin{enumerate}
-        \item[(a)] $y \in \ol{B_E(0, \norm{y}_E)}$.
-        \item[(b)] $0 \in \bigcap_{y \in E}N(y)$.
-        \item[(c)] For any fixed $y_0 \in E$,
-        \[
-        \bracs{y \in E|y_0 \in N(y)} = \bracs{y \in E|\norm{y_0}_E \le \norm{y}_E} \in \cb_E
-        \]
-
-    \end{enumerate}
-
-    By \autoref{proposition:measurable-simple-separable}, (1) and (2) are equivalent.
-\end{proof}

src/measure/measure/localisable.tex

@@ -103,3 +103,96 @@
 \end{proof}
 
 
+\begin{lemma}
+\label{lemma:gluing-measurable-sets}
+    Let $(X, \cm, \mu)$ be a localisable measure space, $\cf = \bracs{A \in \cm|\mu(A) < \infty}$, $\bracs{(E_A, F_A)}_{A \in \cf}$ such that:
+    \begin{enumerate}[label=(\alph*)]
+        \item For each $A \in \cf$, $E_A, F_A \in \cm$, $E_A, F_A \subset A$, and $E_A \cap F_A = \emptyset$. 
+        \item For each $A, B \in \cf$, $\mu((E_A \cap B) \Delta (E_B \cap A)) = 0$ and $\mu((F_A \cap B) \Delta (F_B \cap A)) = 0$.
+    \end{enumerate}
+
+    Let $E$ and $F$ be essential suprema of $\bracsn{E_A}_{A \in \cf}$ and $\bracsn{F_A}_{A \in \cf}$, respectively, then
+    \begin{enumerate}
+        \item For each $B \in \cf$, $\mu(E \cap F_B) = 0$. 
+        \item $\mu(E \cap F) = 0$.
+    \end{enumerate}
+\end{lemma}
+\begin{proof}
+    (1): Let $A, B \in \cf$, then
+    \begin{align*}
+        \mu(E_A \setminus F_B^c) &= \mu(E_A \cap F_B) = \mu(E_A \cap F_B \cap A \cap B) \\
+        &\le \mu(E_A \cap F_A) + \mu((F_A \cap B) \Delta (F_B \cap A)) = 0
+    \end{align*}
+
+    so $F_B^c$ is an essential upper bound of $\bracs{E_A}_{A \in \cf}$. Since $E$ is an essential supremum of $\bracs{E_A}_{A \in \cf}$, $\mu(E \setminus F_B^c) = \mu(E \cap F_B) = 0$. 
+    
+    (2): For any $B \in \cf$, $\mu(F_B \setminus E^c) = \mu(F_B \cap E) = \mu(E \cap F_B) =0$. Thus $E^c$ is an essential upper bound of $\bracs{F_B}_{B \in \cf}$. Given that $F$ is an essential supremum of $\bracsn{F_B}_{B \in \cf}$, $\mu(F \cap E) = \mu(F \setminus E^c) = 0$. 
+\end{proof}
+
+
+\begin{lemma}[Gluing Lemma for Measurable Functions]
+\label{lemma:gluing-measurable}
+    Let $(X, \cm, \mu)$ be a localisable measure space, $\cf = \bracs{A \in \cm|\mu(A) < \infty}$, $Y$ be a Polish space, and $\bracsn{f_A: A \to Y|A \in \cf}$ such that:
+    \begin{enumerate}[label=(\alph*)]
+        \item For each $A \in \cf$, $f_A \in \mathcal{L}^0(A; Y)$. 
+        \item For each $A, B \in \cf$, $f_A|_{A \cap B} = f_B|_{A \cap B}$ almost everywhere.  
+    \end{enumerate}
+    
+    then there exists $f: X \to Y$ such that:
+    \begin{enumerate}
+        \item $f \in \mathcal{L}^0(X; Y)$. 
+        \item For each $A \in \cf$, $f|_A = f_A$ almost everywhere. 
+        \item[(U)] For any $g: X \to Y$ satisfying (1) and (2), $f = g$ almost everywhere. 
+    \end{enumerate}
+\end{lemma}
+\begin{proof}
+    First suppose that $Y$ is finite. For each $y \in Y$, let $P(y)$ be an essential supremum of $\bracs{f_A^{-1}(y)|A \in \cf}$. By \autoref{lemma:gluing-measurable-sets}, for any $x, y \in Y$ with $x \ne y$, $\mu(P(x) \cap P(y)) = 0$. After modification by null sets, assume without loss of generality that $X = \bigsqcup_{y \in Y}P(y)$. 
+
+    For each $x \in X$, let $f(x) \in Y$ be the unique element of $Y$ such that $x \in P(f(x))$, then:
+    \begin{enumerate}
+        \item For each $y \in Y$, $f^{-1}(y) = P(y)$, so $f \in \mathcal{L}^0(X; Y)$ is measurable. 
+        \item Let $A \in \cf$, then for each $y \in Y$, $\mu(f_A^{-1}(y) \setminus P(y)) = 0$. On the other hand, 
+        \begin{align*}
+         (P(y) \cap A) \setminus f_A^{-1}(y) &= P(y) \cap \bigcup_{z \in Y \setminus \bracs{y}}f_A^{-1}(z) \\
+         &\subset \braks{P(y) \cap \bigcup_{z \in Y \setminus \bracs{y}}P(z)} \cup \bigcup_{z \in Y \setminus \bracs{y}}f_A^{-1}(z) \setminus P(z)
+        \end{align*}
+
+        is a null set. Therefore $f|_A = f_A$ almost everywhere. 
+        \item[(U)] For all $A \in \cf$, $f|_A = g|_A$ almost everywhere. Since $\mu$ is semifinite, $f = g$ almost everywhere. 
+    \end{enumerate}
+    
+    Therefore $f$ is the desired function. 
+
+    Now suppose that $Y$ is an arbitrary separable metrisable space. By \autoref{lemma:admissible-approximant-existence}, there exists $\seq{I_n} \subset Y^Y$ such that:
+    \begin{enumerate}[label=(\roman*)]
+        \item $I_n \to \text{Id}$ pointwise as $n \to \infty$. 
+        \item For each $n \in \natp$, $I_n(Y)$ is finite and Borel measurable. 
+    \end{enumerate}
+
+    For each $n \in \natp$, let $f_{A, n} = I_n \circ f_A$, then 
+    \begin{enumerate}[label=(\alph*)]
+        \item For each $A \in \cf$, $f_{A, n} \in \mathcal{L}^0(A; Y)$. 
+        \item For each $A, B \in \cf$, $f_{A, n}|_{A \cap B} = f_{B, n}|_{A \cap B}$ almost everywhere. 
+        \item For each $A \in \cf$, $f_{A, n}(A) \subset I_n(Y)$. 
+    \end{enumerate}
+
+    By the finite case, there exists $f_n: X \to Y$ such that:
+    \begin{enumerate}
+        \item $f_n \in \mathcal{L}^0(X; Y)$. 
+        \item For each $A \in \cf$, $f_n|_A = f_{A, n}$ almost everywhere. 
+    \end{enumerate}
+    
+    Since $Y$ is Polish, \autoref{proposition:metric-measurable-limit} implies that $\bracsn{\limv{n}f_n \text{ exists}} \in \cm$. For each $A \in \cf$, since $\limv{n}f_{A, n}$ and $\limv{n}f_{n}|_A$ exist and are equal almost everywhere on $A$, 
+    \[
+    \mu\paren{\bracs{\limv{n}f_n \text{ does not exist}} \cap A} \le \mu\bracs{\limv{n}f_{A, n} \text{ does not exist}} = 0
+    \]
+
+    As $\mu$ is semifinite, $\mu\bracsn{\limv{n}f_n \text{ does not exist}} = 0$, so there exists $f \in \mathcal{L}^0(X; Y)$ such that $f = \limv{n}f_n$ almost everywhere. In which case, 
+    \begin{enumerate}
+        \item $f \in \mathcal{L}^0(X; Y)$. 
+        \item For each $A \in \cf$, $f|_A = \limv{n}f_n|_A = \limv{n}f_{A, n} = f_A$ almost everywhere. 
+        \item[(U)] For all $A \in \cf$, $f|_A = g|_A$ almost everywhere. Since $\mu$ is semifinite, $f = g$ almost everywhere. 
+    \end{enumerate}
+\end{proof}
+
+

src/measure/measure/product.tex

@@ -127,7 +127,7 @@
 
     Therefore $\alg = \cm \otimes \cn$. 
 
-    Now let $F \subset L^+(X \times Y)$ be the set of functions satisfying (1), then $F \supset \Sigma^+(X, \cm)$ by linearity. Let $f \in L^+(X \times Y)$, then by \autoref{proposition:measurable-simple-separable}, there exists $\seq{\phi_n} \subset \Sigma^+(X \times Y)$ such that $\phi_n \upto f$. In which case, by the Monotone Convergence Theorem, (1) also holds for $f$. 
+    Now let $F \subset L^+(X \times Y)$ be the set of functions satisfying (1), then $F \supset \Sigma^+(X, \cm)$ by linearity. Let $f \in L^+(X \times Y)$, then by \autoref{corollary:measurable-simple-separable}, there exists $\seq{\phi_n} \subset \Sigma^+(X \times Y)$ such that $\phi_n \upto f$. In which case, by the Monotone Convergence Theorem, (1) also holds for $f$. 
 \end{proof}
 
 

src/process/markov/definition.tex

@@ -41,7 +41,7 @@
     (\bp_{s+t}\one_A)(x) = \int \one_A(y)P_{s+t}(x, dy) = \int P_t(y, A)P_s(x, dy) = \int \int \one_A(z)P_t(y, dz)P_s(x, dy)
     \]
 
-    Let $f: X \to \complex$ bounded and $(\cm, \cb_\complex)$-measurable. By \autoref{proposition:measurable-simple-separable-norm}, there exists $\seq{f_n} \subset \Sigma(X; \complex)$ such that $\abs{f_n} \le \abs{f}$ for all $n \in\nat$, and $f_n \to f$ pointwise. By the \hyperref[Dominated Convergence Theorem]{theorem:dct},
+    Let $f: X \to \complex$ bounded and $(\cm, \cb_\complex)$-measurable. By \autoref{corollary:measurable-simple-separable-norm}, there exists $\seq{f_n} \subset \Sigma(X; \complex)$ such that $\abs{f_n} \le \abs{f}$ for all $n \in\nat$, and $f_n \to f$ pointwise. By the \hyperref[Dominated Convergence Theorem]{theorem:dct},
     \begin{align*}
     (\bp_{s+t}f)(x) &= \limv{n}\int f_n(y)P_{s+t}(x, dy) = \limv{n}\iint f_n(z)P_t(y, dz)P_s(x, dy) \\
     &= \int \int f_n(z)P_t(y, dz)P_s(x, dy) = (\bp_s\bp_t) f(x)