Added first darft of gluing lemma for measurable functions.

src/measure/measurable-maps/approx.tex

@@ -34,7 +34,7 @@
 
 \begin{lemma}[Existence of Simple Approximations of the Identity]
 \label{lemma:separable-metric-space-approx-identity}
-    Let $X$ be a separable metric 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:
+    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}$. 
@@ -50,7 +50,7 @@
 
     Since $x_1 \in \bigcap_{y \in X}\mathcal{A}(y)$, $1 \in C_N(x)$ and $C_N(x) \ne \emptyset$. 
     
-    From here, let
+    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)}
     \]
@@ -90,7 +90,7 @@
 
 \begin{corollary}
 \label{corollary:measurable-simple-separable}
-    Let $(X, \cm)$ be a measurable space, $Y$ be a separable metric 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:
+    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

src/measure/measure/localisable.tex

@@ -158,12 +158,41 @@
         \end{align*}
 
         is a null set. Therefore $f|_A = f_A$ almost everywhere. 
-        \item For all $A \in \cf$, $f|_A = g|_A$ almost everywhere. Since $\mu$ is semifinite, $f = g$ 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 arbitrary. Let $\seq{y_n} \subset Y$ be a dense subset of $Y$. By \autoref{corollary:measurable-simple-separable}, for each
+    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$, 
+    \[
+    \mu\paren{\bracs{\limv{n}f_n \text{ does not exist}} \cap A} = \mu\bracs{\limv{n}f_{A, n} \ne f_A} = 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}