Updated Alaoglu's theorem.

src/fa/tvs/equicontinuous.tex

@@ -110,5 +110,20 @@
     Let $\seq{(x_n, y_n)} \subset E \times F$ and $\seq{\lambda_n} \subset \alg$ such that $(x_n, y_n) \to 0$ as $n \to \infty$. Since $\seq{y_n}$ is convergent, for each $n \in \natp$ and $x \in E$, $\bracsn{\lambda_n(x, y_n)|n \in \natp}$ is bounded by (E) and \autoref{proposition:equicontinuous-net}. By (B) or (B') and the \hyperref[Banach-Steinhaus Theorem]{theorem:banach-steinhaus}, $\bracsn{\lambda_n(\cdot, y_n)|n \in \natp}$ is equicontinuous, and $\lambda_n(x_n, y_n) \to 0$ as $n \to \infty$ by \autoref{proposition:equicontinuous-net}. By (M) and \autoref{proposition:equicontinuous-net}, $\alg$ is equicontinuous at $0$, and hence equicontinuous by \autoref{lemma:equicontinuous-bilinear}. 
 \end{proof}
 
+% TODO: Replace this with a more general version involving polars in the future. 
+\begin{theorem}[Banach-Alaoglu]
+\label{theorem:alaoglu}
+    Let $E$ be a locally convex space over $K \in \RC$ and $\alg \subset E^*$ be equicontinuous, then $\alg$ is precompact with respect to $\sigma(E^*, E)$.
+\end{theorem}
+\begin{proof}
+    For each $x \in E$, $\alg(x) = \bracsn{\dpn{x, \phi}{E}|\phi \in \alg}$ is precompact by \autoref{proposition:equicontinuous-bounded}. By the \hyperref[Arzelà-Ascoli Theorem]{theorem:arzela-ascoli}, 
+    \begin{enumerate}
+        \item[(C2)] The $\sigma(E^*, E)$-closure of $\alg$ in $\prod_{x \in E}K$ is equicontinuous. 
+        \item[(C3)] The $\sigma(E^*, E)$-closure of $\alg$ in $\prod_{x \in E}K$ is compact. 
+    \end{enumerate}
+
+    By \autoref{proposition:operator-space-completeness}, the $\sigma(E^*, E)$-closure of $\alg$ in $\prod_{x \in E}\ol{\alg(x)}$ is a subset of $\hom(E; K)$. Hence the $\sigma(E^*, E)$-closure of $\alg$ in $E^*$ is compact. 
+\end{proof}
+