Housekeeping.

src/fa/norm/normed.tex

@@ -122,7 +122,7 @@
 
 \begin{proposition}
 \label{proposition:dual-norm}
-    Let $E$ be a normed vector space, then for any $x \in E$, 
+    Let $E$ be a normed vector space over $K \in \RC$, then for any $x \in E$, 
     \[
     \norm{x}_E = \sup_{\substack{\phi \in E^* \\ \norm{\phi}_{E^*} = 1}}\dpn{x, \phi}{E}
     \]
@@ -132,3 +132,19 @@
 \end{proof}
 
 
+\begin{lemma}[Riesz]
+\label{lemma:riesz-almost-orthogonal}
+    Let $E$ be an infinite-dimensional normed vector space over $K \in \RC$ and $\seq{\alpha_n} \subset (0, 1)$, then there exists $\seq{x_n} \subset \partial B_E(0, 1)$ such that
+    \[
+    d(x_n, \text{span}\bracsn{x_j|1 \le j < n}) > \alpha_n \quad \forall n \in \natp
+    \]
+\end{lemma}
+\begin{proof}
+    Let $N \in \natp$ and suppose inductively that $\bracsn{x_n|1 \le n < N}$ have been constructed to satisfy the lemma for all $1 \le n < N$. Let $F_N = \text{span}\bracsn{x_n|1 \le n < N}$, then $F_N$ is finite-dimensional, and closed by \autoref{proposition:closed-subspace-induction}. As $E$ is infinite-dimensional, $E/F_N$ is non-trivial, and there exists $y_N \in E$ such that $\norm{y_N + F_N}_{E/F_N} > \alpha_N$. By \autoref{lemma:quotient-norm-optimiser}, there exists $z_N \in B_E(0, 1)$ such that $z_N + F_N = y_N + F_N$. As $z_N + F_N \ne 0$, $z_N \ne 0$ as well. Let $x_N = z_N/\norm{z_N}_{E} \in \partial B_E(0, 1)$, then
+    \[
+        \norm{x_N + F_N}_{E/F} > \norm{z_N + F_N}_{E/F} = \norm{y_N + F_N}_{E/F} > \alpha_N
+    \]
+
+    Thus $d(x_N, \text{span}\bracsn{x_n|1 \le n < N}) = \norm{x_N + F_N}_{E/F} > \alpha_N$.
+\end{proof}
+