Added basic theory of Lp spaces, alongside some integral stuff.

src/measure/bochner-integral/strongly.tex

@@ -0,0 +1,27 @@
+\section{Strongly Measurable Functions}
+\label{section:strongly-measurable}
+
+\begin{definition}[Strongly Measurable Function]
+\label{definition:strongly-measurable}
+    Let $(X, \cm)$ be a measurable space, $E$ be a normed vector space over $K \in \RC$, and $f: X \to E$, then the following are equivalent:
+    \begin{enumerate}
+        \item For each $\phi \in E^*$, $\phi \circ f$ is $(\cm, \cb_K)$-measurable and $f(X) \subset E$ is separable.
+        \item $f$ is $(\cm, \cb_E)$ measurable and $f(X) \subset E$ is separable.
+        \item There exists a sequence $\seq{f_n} \subset \Sigma(X, \cm; E)$ such that
+        \begin{enumerate}
+            \item[(a)] For each $n \in \natp$, $\norm{f_n}_E \le \norm{f}_E$.
+            \item[(b)] $\norm{f_n(x) - f(x)}_E \to 0$ pointwise as $n \to \infty$.
+        \end{enumerate}
+    \end{enumerate}
+\end{definition}
+\begin{proof}
+    (1) $\Rightarrow$ (2): TODO
+
+    (2) $\Rightarrow$ (3): By \ref{proposition:measurable-simple-separable-norm}.
+
+    (3) $\Rightarrow$ (1): For each $\phi \in E^*$, $\phi \circ f = \limv{n}\phi \circ f_n$ is measurable by \ref{proposition:limit-measurable}. Since
+    \[
+    f(X) \subset \ol{\bigcup_{n \in \natp}f_n(X)}
+    \]
+    and each $f_n$ is finitely-valued, $f(X)$ is separable.
+\end{proof}