Added mental gymnastics for lp direct sums.

src/fa/lp/definition.tex

@@ -176,25 +176,25 @@
     \begin{enumerate}
         \item For any $\alpha > 0$, 
         \[
-        \mu\bracs{|f| \ge \alpha} \le \frac{1}{\alpha}\norm{f}_{L^1(X; E)}
+        \mu\bracs{\norm{f}_E \ge \alpha} \le \frac{1}{\alpha}\norm{f}_{L^1(X; E)}
         \]
         \item For $\alpha > 0$ and strictly increasing function $\phi: [0, \infty) \to [0, \infty)$,
         \[
-        \mu\bracs{|f| \ge \alpha} \le \frac{1}{\phi(\alpha)}\norm{\phi \circ |f|}_{L^1(X; E)}
+        \mu\bracs{\norm{f}_E \ge \alpha} \le \frac{1}{\phi(\alpha)}\norm{\phi \circ |f|}_{L^1(X; E)}
         \]
         \item For any $\alpha > 0$,
         \[
-        \mu\bracs{|f| \ge \alpha} \le \frac{1}{\alpha^p}\norm{f}_{L^p(X; E)}^p
+        \mu\bracs{\norm{f}_E \ge \alpha} \le \frac{1}{\alpha^p}\norm{f}_{L^p(X; E)}^p
         \]
     \end{enumerate}
 \end{theorem}
 \begin{proof}
     (1): For any $\alpha > 0$, 
     \begin{align*}
-        \mu\bracs{|f| \ge \alpha} &= \int_{\bracs{f \ge \alpha}} d\mu \le \frac{1}{\alpha}\int |f|d\mu = \frac{\norm{f}_{L^1(X; E)}}{\alpha}
+        \mu\bracs{\norm{f}_E \ge \alpha} &= \int_{\bracs{\norm{f}_E \ge \alpha}} d\mu \le \frac{1}{\alpha}\int |\norm{f}_Ed\mu = \frac{\norm{f}_{L^1(X; E)}}{\alpha}
     \end{align*}
     
-    (2): By \autoref{lemma:monotone-measurable}, $\phi: [0, \infty) \to [0, \infty)$ is Borel measurable. Since $\phi$ is strictly increasing, $\bracs{|f| \ge \alpha} = \bracs{\phi \circ |f| \ge \phi(\alpha)}$, and the result holds by applying (1) to $\phi \circ |f|$. 
+    (2): By \autoref{lemma:monotone-measurable}, $\phi: [0, \infty) \to [0, \infty)$ is Borel measurable. Since $\phi$ is strictly increasing, $\bracs{\norm{f}_E \ge \alpha} = \bracs{\phi \circ \norm{f}_E \ge \phi(\alpha)}$, and the result holds by applying (1) to $\phi \circ \norm{f}_E$. 
 
     (3): Since $x \mapsto x^p$ is strictly increasing on $[0, \infty)$, applying (2) to $\phi(x) = x^p$ yields the desired result.
 \end{proof}
@@ -213,5 +213,34 @@
 \end{proof}
 
 
+% Move this to interpolation
 
+\begin{proposition}
+\label{proposition:lp-intersection-interpolation}
+    Let $(X, \cm, \mu)$ be a measure space, $E$ be a normed vector space, and $0 < p < q < r \le \infty$, then $L^p(X; E) \cap L^r(X; E) \subset L^q(X; E)$, where for each $f \in L^p(X; E) \cap L^r(X; E)$, 
+    \[
+    \norm{f}_{L^q(X; E)} \le \norm{f}_{L^p(X; E)}^\lambda\norm{f}_{L^q(X; E)}^{1 - \lambda}
+    \]
+
+    with
+    \[
+    \frac{1}{q} = \frac{\lambda}{p} + \frac{(1 - \lambda)}{r} \quad \lambda = \frac{q^{-1} - r^{-1}}{p^{-1} - r^{-1}}
+    \]
+\end{proposition}
+\begin{proof}[Proof, {{\cite[Proposition 6.10]{Folland}}}. ]
+    If $r = \infty$, then $\norm{f}_{E}^q \le \norm{f}_{L^\infty(X; E)}^{q - p}\norm{f}_E^p$ and $\lambda = p/q$, so
+    \[
+    \norm{f}_{L^q(X; E)} \le \norm{f}_{L^p(X; E)}^{p/q} \cdot \norm{f}_{L^\infty(X; E)}^{1 - p/q} = \norm{f}_{L^p(X; E)}^\lambda\norm{f}_{L^q(X; E)}^{1 - \lambda}
+    \]
+
+    If $r < \infty$, then by \hyperref[Hölder's inequality]{theorem:holder} applied to the pair $p/(\lambda q)$ and $r/[(1 - \lambda)q]$, 
+    \begin{align*}
+        \norm{f}_{L^q(X; E)}^q &= \int \norm{f}_{E}^{\lambda q}\norm{f}_E^{(1 - \lambda)q} d\mu \\
+        &= \norm{\norm{f}_E^{\lambda q}}_{L^{p/(\lambda q)}(X; \real)} \cdot 
+        \norm{\norm{f}_E^{(1 - \lambda) q}}_{L^{r/[(1 - \lambda)q]}(X; \real)} \\
+        &= \norm{f}_{L^p(X; E)}^{\lambda q}\norm{f}_{L^q(X; E)}^{(1 - \lambda)q} \\
+    \norm{f}_{L^q(X; E)} &\le \norm{f}_{L^p(X; E)}^\lambda\norm{f}_{L^q(X; E)}^{1 - \lambda}
+    \end{align*}
+    
+\end{proof}
 

src/fa/lp/seq.tex

@@ -27,6 +27,41 @@
     \]
 \end{definition}
 
+\begin{proposition}
+\label{proposition:lp-direct-sum-gymnastics}
+    Let $\seqi{X}$ be normed vector spaces over $K \in \RC$ and $p \in [1, \infty]$. 
+    \begin{enumerate}
+        \item (\textbf{Hölder's Inequality}) Let $q \in [1, \infty]$ be the Hölder conjugate of $p$, $\seqi{Y}, \seqi{Z}$ be normed spaces, and $\seqi{\lambda}$ such that for each $i \in I$, $\lambda \in L^2(X_i, Y_i; Z)$.
+        
+        For each $x \in [l^p(I); X_i]$ and $y \in [l^q(I); Y_i]$, let $\lambda(x, y)_i = \lambda_i(x_i, y_i)$, then
+        \[
+        \norm{\lambda(x, y)}_{[l^1(I); Z_i]} \le \norm{x}_{[l^p(I); X_i]} \cdot \norm{y}_{[l^q(I); X_i]} \cdot \sup_{i \in I}\norm{\lambda_i}_{L^2(X_i, Y_i; Z_i)}
+        \]
+        \item (\textbf{Minkowski's Inequality}) For each $x, y \in [l^p(I); X_i]$,
+        \[
+        \norm{x + y}_{[l^p(I); X_i]} \le \norm{x}_{[l^p(I); X_i]} + \norm{y}_{[l^p(I); X_i]}
+        \]
+
+        \item (\textbf{Markov's Inequality}) If $p < \infty$, then for each $\alpha > 0$ and $x \in [l^p(I); X_i]$, 
+        \[
+        |\bracsn{i \in I|\ \norm{x}_{X_i} \ge \alpha}| \le \frac{1}{\alpha^p}\norm{f}_{[l^p(I); X_i]}^p
+        \]
+
+        In particular, $\bracs{i \in I|x_i \ne 0}$ is countable. 
+        \item For any $q \in [p, \infty]$, $[l^p(I); X_i] \subset [l^q(I); X_i]$, where for any $x \in [l^p(I); X_i]$, $\norm{x}_{[l^q(I); X_i]} \le \norm{x}_{[l^p(I); X_i]}$. 
+        \item If $X_i$ is a Banach space for all $i \in I$, then so is $[l^p(I); X_i]$. 
+    \end{enumerate}
+\end{proposition}
+\begin{proof}
+    (1), (2), (3): By the classical \hyperref[Hölder's inequality]{theorem:holder}, \hyperref[Minkowski's inequality]{theorem:minkowski}, and \hyperref[Markov's inequality]{theorem:markov-inequality}.
+    
+    (4): For each $i \in I$, $\norm{x_i}_{X_i} \le \norm{x}_{[l^p(I); X_i]}$, so the result holds when $q = \infty$. 
+
+    If $q < \infty$, then by \autoref{proposition:lp-intersection-interpolation}, there exists $\lambda \in [p, q]$ such that 
+    \[
+    \norm{x}_{[l^p(I); X_i]} \le \norm{x}_{[l^p(I); X_i]}^{\lambda}\norm{x}_{[l^\infty(I); X_i]}^{1 - \lambda} \le \norm{x}_{[l^p(I); X_i]}
+    \]
+\end{proof}