Added complexification.

src/dg/complex/derivative.tex

@@ -221,7 +221,7 @@
 \end{proof}
 
 
-\begin{definition}[Complex Analytic]
+\begin{definition}[Holomorphic]
 \label{definition:complex-analytic}
     Let $E$ be a complete separated locally convex space over $\complex$, $U \subset \complex$ be open, and $f \in C(U; E)$, then the following are equivalent:
     \begin{enumerate}
@@ -234,16 +234,16 @@
         \[
         f(z_0) = \frac{1}{2\pi i} \int_\gamma \frac{f(z)}{z - z_0}dz
         \]
-        \item (\textbf{Analyticity}) For each $z_0 \in U$ and $r > 0$ such that $\ol{B(z_0, r)} \subset U$, there exists $\seq{a_n} \subset E$ such that $f$ may be expressed as a power series
+        \item (\textbf{Analyticity}) For each $z_0 \in U$ and $r > 0$ with $\ol{B(0, r)} \subset U$, there exists $\seq{a_n} \subset E$ such that for each $z \in B(z_0, r/2)$, 
         \[
         f(z) = \sum_{n = 0}^\infty a_n(z - z_0)^n
         \]
 
-        with radius of convergence at least $r$.
+        where the radius of convergence of the series is at least $r$. 
         \item (\textbf{Weak Holomorphy}) For each $\phi \in E^*$, $\phi \circ f$ satisfies the above. 
     \end{enumerate}
 
-    If the above holds, then $f$ is \textbf{complex analytic}. 
+    If the above holds, then $f$ is \textbf{holomorphic/complex analytic} on $U$. 
 \end{definition}
 \begin{proof}
     (1) $\Leftrightarrow$ (2): \autoref{lemma:complex-analytic}. 
@@ -257,7 +257,7 @@
     
     Let
     \[
-    g(z) = \sum_{k = 0}^\infty \frac{1}{k!} D^kf(z_0)(z - z_0)^n
+    g(z) = \sum_{k = 0}^\infty \frac{1}{k!} D^kf(z_0)(z - z_0)^k
     \]
 
     then by \hyperref[Cauchy's Estimate]{corollary:cauchy-estimate}, for any $k \in \natz$ and continuous seminorm $[\cdot]_E: E \to [0, \infty)$, 
@@ -267,7 +267,7 @@
 
     Thus $[D^kf(z_0)/k!]_E \le C/r^k$ for all $k \in \natz$, and the radius of convergence of $g$ is at least $r$. 
     
-    Let $z \in B(z_0, r/2)$, $s = |z - z_0|$, and $n \in \natp$, then by \hyperref[Taylor's Formula]{theorem:taylor-lagrange} and \hyperref[Cauchy's Estimate]{corollary:cauchy-estimate}, 
+    Let $z \in B(z_0, r/2)$, $s = |z - z_0|$, and $n \in \natp$, then by \hyperref[Taylor's Formula]{theorem:taylor-integral} and \hyperref[Cauchy's Estimate]{corollary:cauchy-estimate}, 
     \begin{align*}
         \braks{f(z) - \sum_{k = 0}^n \frac{1}{k!} D^kf(z_0)(z - z_0)^n}_E &\le s^{n+1} \cdot \sup_{z' \in \ol{B(z_0, s)}} [D^{n+1}f(z')]_E \\
         &\le \frac{Cs^{n+1}}{(r-s)^{n+1}}
@@ -281,3 +281,4 @@
 \end{proof}
 
 
+

src/dg/complex/entire.tex

@@ -0,0 +1,44 @@
+\section{Entire Functions}
+\label{section:entire-holomorphic}
+
+\begin{definition}[Entire Function]
+\label{definition:entire-function}
+    Let $E$ be a complete separated locally convex space over $\complex$, then an \textbf{entire $E$-valued function} is an $E$-valued holomorphic function on $\complex$.
+\end{definition}
+
+\begin{proposition}
+\label{proposition:entire-power-series}
+    Let $E$ be a complete separated locally convex space over $\complex$, and $f \in H(\complex; E)$, then for any $z_0 \in \complex$ and $z \in \complex$,
+    \[
+    f(z) = \sum_{k = 0}^\infty \frac{1}{k!} D^kf(z_0)(z - z_0)^k
+    \]
+
+    where the radius of convergence of the series is infinite. 
+\end{proposition}
+\begin{proof}
+    See (4) of \autoref{definition:complex-analytic}. 
+\end{proof}
+
+\begin{theorem}[Liouville]
+\label{theorem:liouville}
+    Let $E$ be a complete separated locally convex space over $\complex$ and $f \in H(\complex; E)$. If $f$ is bounded, then $f$ is constant. 
+\end{theorem}
+\begin{proof}
+    Let $x_0 \in \complex$ and $[\cdot]_E: [E, \infty)$ be a continuous seminorm on $E$, then by \hyperref[Cauchy's Estimate]{corollary:cauchy-estimate},
+    \[
+    [Df(z_0)]_E \le \frac{1}{r} \sup_{z \in \ol{B(z_0, r)}}[f(z)]_E
+    \]
+
+    for all $r > 0$. Therefore $Df = 0$, and $f$ is constant. 
+\end{proof}
+
+\begin{theorem}[Fundamental Theorem of Algebra]
+\label{theorem:fundamental-theorem-of-algebra}
+    Let $p \in \complex[z]$ be a non-constant polynomial, then there exists $z \in \complex$ such that $f(z) = 0$. 
+\end{theorem}
+\begin{proof}
+    Let $p \in \complex[z]$ such that $p(z) \ne 0$ for all $z \in \complex$. Let $f = 1/p$, then $f \in H(\complex; \complex) \cap C_0(\complex; \complex)$, so $f$ is bounded. By \hyperref[Liouville's Theorem]{theorem:liouville}, $f$ and thus $p$ is constant. 
+\end{proof}
+
+
+

src/dg/complex/index.tex

@@ -3,6 +3,8 @@
 
 
 \input{./derivative.tex}
+\input{./space.tex}
 \input{./log.tex}
+\input{./entire.tex}
 
 

src/dg/complex/space.tex

@@ -0,0 +1,40 @@
+\section{Spaces of Holomorphic Functions}
+\label{section:holomorphic-function-space}
+
+\begin{definition}[Space of Holomorphic Functions]
+\label{definition:holomorphic-function-space}
+    Let $E$ be a complete separated locally convex space over $\complex$ and $U \subset \complex$ be open, then $H(U; E)$ is the \textbf{space of $E$-valued holomorphic functions on $U$}, equipped with the topology of uniform convergence on compact sets. 
+\end{definition}
+
+\begin{proposition}
+\label{proposition:holomorphic-complete}
+    Let $E$ be a complete separated locally convex space over $\complex$ and $U \subset \complex$ be open, then $H(U; E)$ is complete. 
+\end{proposition}
+\begin{proof}
+    By \hyperref[corollary:cauchy-estimate]{Cauchy's estimate}, uniform convergence on compact sets is equivalent to uniform convergence of derivatives of all orders on compact sets. Since $U$ is locally compact, uniform limits of holomorphic functions are holomorphic by \autoref{theorem:differentiable-uniform-limit}.
+\end{proof}
+
+\begin{theorem}[Montel]
+\label{theorem:montel}
+    Let $E$ be a complete separated locally convex space over $\complex$, $U \subset \complex$ be open, and $\cf \subset H(U; E)$, then the following are equivalent:
+    \begin{enumerate}[label=(B\arabic*)]
+        \item $\cf$ is equicontinuous, and for each $x \in U$, $\cf(x) = \bracs{f(x)|f \in \cf}$ is bounded.
+        \item $\cf$ is bounded in $H(U; E)$.
+    \end{enumerate}
+
+    and the following are equivalent:
+    \begin{enumerate}[label=(C\arabic*)]
+        \item $\cf$ is precompact in $H(U; E)$. 
+        \item $\cf$ is bounded in $H(U; E)$, and for each $x \in U$, $\cf(x) = \bracs{f(x)|f \in \cf}$ is precompact.  
+    \end{enumerate}
+\end{theorem}
+\begin{proof}
+    (B1) $\Rightarrow$ (B2): Let $K \subset U$ be compact and $V \in \cn_E(0)$ be circled. Since $\cf$ is equicontinuous, for each $x \in K$, there exists $U_x \in \cn_U(x)$ such that $f(y) - f(x) \in V$ for all $y \in U_x$ and $f \in \cf$. By compactness of $K$, there exists $\seqf{x_j} \subset K$ such that $K \subset \bigcup_{j = 1}^n U_{x_j}$. Since $B = \bigcup_{j = 1}^n \cf(x_j)$ is bounded, there exists $\lambda > 0$ such that $\lambda V \supset B$. In which case, 
+    \[
+    (\lambda + 1)V \supset B + V \supset \bigcup_{x \in K}^n \cf(x)
+    \]
+
+    (B2) $\Rightarrow$ (B1): By \hyperref[Cauchy's Estimate]{corollary:cauchy-estimate}, $\bracsn{Df|f \in \cf}$ is also uniformly bounded on every compact set. Thus $\cf$ is equicontinuous. 
+
+    (C1) $\Leftrightarrow$ (C2): By the \hyperref[Arzelà-Ascoli Theorem]{theorem:arzela-ascoli}.
+\end{proof}

src/dg/derivative/taylor.tex

@@ -62,16 +62,17 @@
 
 \begin{theorem}[Taylor's Formula, Peano Remainder]
 \label{theorem:taylor-peano}
-    Let $E$ be a topological vector space, $\sigma \subset \mathfrak{B}(E)$ be an ideal that includes bounded sets contained in finite-dimensional subspaces, $F$ be a separated locally convex space, $U \subset E$ be open, and $f: U \to F$ be $n$-fold $\tilde \sigma$-differentiable at $x_0 \in U$, then there exists $r \in \mathcal{R}_\sigma^n(E; F)$ such that
+    Let $E$ be a topological vector space, $\sigma \subset \mathfrak{B}(E)$ be an ideal containing bounded subsets in finite-dimensional subspaces, $F$ be a separated locally convex space, $U \subset E$ be open, and $f: U \to F$ be $n$-fold $\tilde \sigma$-differentiable at $x_0 \in U$, then there exists $r \in \mathcal{R}_\sigma^n(E; F)$ such that
     \[
-    g(x_0 + h) = g(x_0) + \sum_{k = 1}^n \frac{1}{k!}D^k_\sigma f(x_0)(h^{(k)}) + r(h)
+    f(x_0 + h) = f(x_0) + \sum_{k = 1}^n \frac{1}{k!}D^k_\sigma f(x_0)(h^{(k)}) + r(h)
     \]
 
+    for sufficiently small $h$. 
 \end{theorem}
 \begin{proof}[Proof {{\cite[Theorem 4.7.3]{Bogachev}}}. ]
     Let
     \[
-    r(h) = g(x_0 + h) - g(x) - \sum_{k = 1}^n \frac{1}{k!}D^k_\sigma f(x_0)(h^{(k)})
+    r(h) = f(x_0 + h) - f(x) - \sum_{k = 1}^n \frac{1}{k!}D^k_\sigma f(x_0)(h^{(k)})
     \]
 
     For any $1 \le k \le n$, $D^k_\sigma(x_0) \in B^k_\sigma(E; F)$ is symmetric by \autoref{theorem:derivative-symmetric}. Let $T_k(h) = \frac{1}{k!}D^k_\sigma f(x_0)(h^{(k)})$, then by \autoref{theorem:power-rule}, for any $\bracs{t_j}_1^\ell \in E$,
@@ -85,7 +86,7 @@
 
     so
     \[
-    D^k_\sigma r(0) = D^k_\sigma g(x_0) - D^k_\sigma(x_0) = 0
+    D^k_\sigma r(0) = D^k_\sigma g(x_0) - D^k_\sigma f(x_0) = 0
     \]
 
 
@@ -121,3 +122,41 @@
 
     Therefore $r \in \mathcal{R}_\sigma^{n+1}(E; F)$.
 \end{proof}
+
+
+\begin{theorem}[Taylor's Formula, Integral Remainder]
+\label{theorem:taylor-integral}
+    Let $E$ be a topological vector space, $\sigma \subset \mathfrak{B}(E)$ be a covering ideal, $F$ be a separated locally convex space, $U \subset E$ be open, and $f \in C^{n+1}_\sigma(E; F)$, then for any $x_0 \in U$ and $h \in E$ such that $[x_0, x_0 + h] \subset U$, then
+    \[
+    f(x_0 + h) = f(x_0) + \sum_{k = 1}^n \frac{1}{k!}D^k_\sigma f(x_0)(h^{(k)}) + r(h)
+    \]
+
+    where
+    \[
+    r(h) = \int_0^1 \frac{(1 - t)^{n}}{n!}D^{n+1}_\sigma f(x_0 + th)(h^{(n+1)}) dt
+    \]
+
+    In particular, for any continuous seminorm $[\cdot]_F: F \to [0, \infty)$, 
+    \[
+    [r(h)]_F \le \frac{1}{(n+1)!} \cdot \sup_{t \in [0, 1]}[D^{n+1}_\sigma f(x_0 + th)(h^{n+1})]
+    \]
+\end{theorem}
+\begin{proof}{Proof, {{\cite[Section XIII.6]{Lang}}}. }
+    Firstly, if $n = 0$, then by the \hyperref[Fundamental Theorem of Calculus]{theorem:ftc-riemann}, 
+    \[
+    f(x_0 + h) - f(x_0) = \int_0^1 D_\sigma f(x_0 + th)(h) dt
+    \]
+
+    Assume inductively that the theorem holds for $n \in \natz$. Let
+    \[
+    u(t) =  D^{n+1}_\sigma f(x + ty)(h^{(n+1)}) \quad v(t) = -\frac{(1 - t)^{n+1}}{(n+1)!}
+    \]
+
+    then $Dv(t) = (1 - t)^n/n!$, and using the \hyperref[change of variables formula]{theorem:rs-change-of-variables} and \hyperref[integration by parts]{theorem:rs-ibp},
+    \begin{align*}
+        r(h) &= \frac{1}{n!}\int_0^1 (1 - t)^{n}D^{n+1}_\sigma f(x_0 + th)(h^{(n+1)}) dt \\
+        &= \int_0^1 udv = u(1)v(1) - u(0)v(0) - \int_0^1 vdu \\
+        &= D_\sigma^{n+1}(x_0)(h^{(n+1)}) \\
+        &+ \int_0^1 \frac{(1 - t)^{n+1}}{(n+1)!}D^{n+2}_\sigma f(x_0 + th)(h^{(n+2)}) dt
+    \end{align*}
+\end{proof}

src/fa/lc/inductive.tex

@@ -54,8 +54,8 @@
         \item[(U)] For each $(F, \seqi{T})$ satisfying (1) and (2), there exists a unique $T \in L(E; F)$ such that the following diagram commutes:
         \[
         \xymatrix{
-        A \ar@{->}[r]^{T} & B \\
-        A_i \ar@{->}[u]^{\iota_i} \ar@{->}[ru]_{T_i} & 
+        E \ar@{->}[r]^{T} & F \\
+        E_i \ar@{->}[u]^{\iota_i} \ar@{->}[ru]_{T_i} & 
         }
         \]
         
@@ -71,13 +71,45 @@
     The space $E = \bigoplus_{i \in I}E_i$ is the \textbf{locally convex direct sum} of $\seqi{E}$. 
 \end{definition}
 \begin{proof}
-    Let $(E, \seqi{\iota})$ be the direct sum of $\seqi{E}$ as vector spaces, and equip it with the inductive topology induced by $\seqi{\iota}$, then $(E, \seqi{\iota})$ satisfies (1) and (2). 
+    Let $(E, \seqi{\iota})$ be the direct sum of $\seqi{E}$ as vector spaces, and equip it with the locally convex inductive topology induced by $\seqi{\iota}$, then $(E, \seqi{\iota})$ satisfies (1) and (2). 
 
     (U): By (U) of the \hyperref[direct sum]{definition:direct-sum}, there exists a unique $T \in \hom(E; F)$ such that the diagram commutes. In which case, by (4) of \autoref{definition:lc-inductive}, $T \in L(E; F)$. 
 
     (4): By (6) of \autoref{definition:lc-inductive}.
 \end{proof}
 
+\begin{proposition}
+\label{proposition:finite-lc-product}
+    Let $\seqf{E_j}$ be TVSs over $K \in \RC$, then the following spaces coincide:
+    \begin{enumerate}
+        \item The product $\prod_{j = 1}^n E_j$.
+        \item The direct sum of $\seqf{E_j}$ as topological vector spaces.
+        \item The direct sum of $\seqf{E_j}$ as locally convex spaces. 
+    \end{enumerate}
+\end{proposition}
+\begin{proof}
+    By \autoref{proposition:finite-tvs-product}, it is sufficient to show that (1) and (3) coincide. The proof is \textit{exactly} the same as \autoref{proposition:finite-tvs-product}, but included here for completeness.  
+
+    Let $1 \le k \le n$, then for each $1 \le k, l \le n$, $\pi_l \circ \iota_k \in L(E_k, E_l)$, so by (U) of the \hyperref[product]{definition:tvs-product}, $\iota_k \in L(E_k; \prod_{j = 1}^n E_j)$. Thus $\prod_{j = 1}^n E_j$ satisfies (1) and (2) of the \hyperref[direct sum]{definition:lc-direct-sum}. 
+
+    For any locally convex space $F$ over $K$ and $\seqf{T_j}$ with $T_j \in L(E_j; F)$ for each $1 \le j \le n$, let
+    \[
+    T: \prod_{j = 1}^n E_j \to F \quad (x_1, \cdots, x_n) \mapsto \sum_{j = 1}^n T_jx_j
+    \]
+
+    then $T \in L(\prod_{j = 1}^n E_j; F)$ is the unique continuous linear map such that the following diagram commutes:
+    \[
+    \xymatrix{
+    E \ar@{->}[r]^{T} & F \\
+    E_i \ar@{->}[u]^{\iota_i} \ar@{->}[ru]_{T_i} & 
+    }
+    \]
+
+    Hence $\prod_{j = 1}^n E_j$ satisfies (U) of the \hyperref[direct sum]{definition:lc-direct-sum}, so the spaces coincide. 
+\end{proof}
+
+
+
 \begin{definition}[Inductive Limit]
 \label{definition:lc-inductive-limit}
     Let $(\seqi{E}, \bracsn{T^i_j| i, j \in I, i \lesssim j})$ be an upward-directed system of locally convex spaces over $K \in \RC$, then there exists $(E, \bracsn{T^i_E}_{i \in I})$ such that:

src/fa/tvs/complexify.tex

@@ -0,0 +1,119 @@
+\section{Complexification}
+\label{section:complexification}
+
+\begin{definition}[Complexification]
+\label{definition:complexification}
+    Let $E$ be a vector space over $\real$, then there exists a pair $(\complex(E), \iota)$ such that:
+    \begin{enumerate}
+        \item $\complex(E)$ is a vector space over $\complex$.
+        \item $\iota: E \to \complex(E)$ is a $\real$-linear map.
+        \item[(U)] For any pair $(F, T)$ satisfying (1) and (2), there exists a unique $\complex$-linear map $\complex(T): \complex(E) \to F$ such that the following diagram commutes:
+        \[
+        \xymatrix{
+        \mathbb{C}(E) \ar@{->}[r]^{\mathbb{C}(T)} & F \\
+        E \ar@{->}[u]^{\iota} \ar@{->}[ru]_{T} & 
+        }
+        \]
+        \item $\complex(E) = \iota(E) \oplus i\iota(E)$ as a vector space over $\real$. Under this decomposition, elements of $\complex(E)$ are written as $x + iy$, where $x, y \in E$. 
+    \end{enumerate}
+
+    The pair $(\complex(E), \iota)$ is the \textbf{complexification} of $E$, and
+    \begin{enumerate}
+        \item[(F)] For any vector space $F$ over $\real$ and $\real$-linear map $T: E \to F$, there exists a unique $\complex$-linear map $\complex(T): \complex(E) \to \complex(F)$ such that the following diagram commutes:
+        \[
+        \xymatrix{
+        \mathbb{C}(E) \ar@{->}[r]^{\mathbb{C}(T)} & \mathbb{C}(F) \\
+        E \ar@{->}[u]^{\iota} \ar@{->}[r]_{T} & F \ar@{->}[u]_{\iota}
+        }
+        \]
+
+        which is given by
+        \[
+        \complex(T)(x + iy) = Tx + iTy
+        \]
+    \end{enumerate}
+    
+\end{definition}
+\begin{proof}
+    (1): Let $\complex(E) = E \times E$ with coordinate-wise addition. For each $a, b \in \real$ and $x, y \in E$, let
+    \[
+    (a + bi)(x, y) = (ax - by, bx + ay)
+    \]
+
+    then $\complex(E)$ is a vector space over $\complex$. 
+
+    (2): Let $\iota: E \to \complex(E)$ be defined by $\iota(x) = (x, 0)$, then $\iota$ is $\real$-linear. 
+
+    (U): Let
+    \[
+    \complex(T): \complex(E) \to F \quad (x, y) \mapsto Tx + iTy
+    \]
+
+    then $\complex(T)$ is the unique $\complex$-linear map such that the given diagram commutes. 
+
+    (F): By (U) applied to $\iota \circ T$.
+\end{proof}
+
+\begin{definition}[Complexification of Topological Vector Space]
+\label{definition:complexification-tvs}
+    Let $E$ be a TVS over $\real$, then there exists a pair $(\complex(E), \iota)$ such that:
+    \begin{enumerate}
+        \item $\complex(E)$ is a TVS over $\complex$.
+        \item $\iota: E \to \complex(E)$ is a continuous $\real$-linear map. 
+        \item[(U)] For any pair $(F, T)$ satisfying (1) and (2), there exists a unique continuous $\complex$-linear map $\complex(T): \complex(E) \to F$ such that the following diagram commutes:
+        \[
+        \xymatrix{
+        \mathbb{C}(E) \ar@{->}[r]^{\mathbb{C}(T)} & F \\
+        E \ar@{->}[u]^{\iota} \ar@{->}[ru]_{T} & 
+        }
+        \]
+        \item $\complex(E) = \iota(E) \oplus i\iota(E)$ as a TVS over $\real$.
+    \end{enumerate}
+
+    The pair $(\complex(E), \iota)$ is the \textbf{complexification} of $E$ as a topological vector space, and
+    \begin{enumerate}[start=4]
+        \item If $E$ is locally convex, then so is $\complex(E)$. 
+        \item If $E$ is normed, then $\complex(E)$ is normable, and there exists a norm $\norm{\cdot}_{\complex(E)}: \complex(E) \to [0, \infty)$ such that $\iota: E \to \complex(E)$ is isometric. 
+        \item[(F)] For any vector space $F$ over $\real$ and continuous $\real$-linear map $T: E \to F$, there exists a unique continuous $\complex$-linear map $\complex(T): \complex(E) \to \complex(F)$ such that the following diagram commutes:
+        \[
+        \xymatrix{
+        \mathbb{C}(E) \ar@{->}[r]^{\mathbb{C}(T)} & \mathbb{C}(F) \\
+        E \ar@{->}[u]^{\iota} \ar@{->}[r]_{T} & F \ar@{->}[u]_{\iota}
+        }
+        \]
+
+        which is given by
+        \[
+        \complex(T)(x + iy) = Tx + iTy
+        \]
+    \end{enumerate}
+    
+\end{definition}
+\begin{proof}
+    (1), (2): Let $(\complex(E), \iota)$ be the complexification of $E$ as a vector space, and equip it with the \hyperref[direct sum]{definition:tvs-direct-sum} topology. 
+
+    (U): By (U) of the \hyperref[complexification]{definition:complexification}, there exists a $\complex$-linear map $\complex(T): \complex(E) \to F$ such that the given diagram commutes. Since $T \circ \iota$ and $iT \circ \iota$ are continuous, $T$ is continuous by (U) of the \hyperref[direct sum]{definition:tvs-direct-sum}.
+
+    (4): By \autoref{proposition:finite-lc-product}, the direct sum and product of finitely many locally convex spaces coincide. By \autoref{proposition:lc-projective-topology}, this topology is locally convex. 
+
+    (5): Let $\norm{\cdot}_E: E \to [0, \infty)$ be the norm of $E$, and define
+    \[
+    \norm{\cdot}_{\complex(E)}: \complex(E) \to [0, \infty) \quad (x, y) \mapsto \sup_{\theta \in [0, 2\pi]}\norm{\cos(\theta)x + \sin(\theta)y}_E
+    \]
+
+    then for any $\phi \in [0, 2\pi]$ and $x, y \in E$, 
+    \begin{align*}
+        \normn{e^{i \phi}(x, y)}_{\complex(E)} &= \normn{(\cos(\phi)x - \sin(\phi)y, \sin(\phi)x + \cos(\phi)y)}_{\complex(E)} \\
+        &= \sup_{\theta \in [0, 2\pi]}\norm{\cos(\theta - \phi)x + \sin(\theta - \phi)y}_E \\
+        &= \norm{(x, y)}_{\complex(E)}
+    \end{align*}
+
+    so $\norm{(x, y)}_{\complex(E)}$ is a norm. For any $x \in E$, 
+    \[
+    \norm{\iota x}_{\complex(E)} = \sup_{\theta \in [0, 2\pi]}\norm{\cos(\theta)x}_E = \norm{x}_E \\
+    \]
+
+    Therefore $\iota: E \to \complex(E)$ is isometric. 
+
+    (F): By (U) applied to $\iota \circ T$.
+\end{proof}

src/fa/tvs/index.tex

@@ -2,6 +2,7 @@
 \label{chap:tvs}
 
 \input{./definition.tex}
+\input{./complexify.tex}
 \input{./metric.tex}
 \input{./bounded.tex}
 \input{./dual.tex}

src/fa/tvs/inductive.tex

@@ -34,6 +34,58 @@
     (4): Let $U \in \cn_F(0)$ be circled and radial and $i \in I$. Since $T \circ E_i \in L(E_i; F)$, $T_i^{-1}(T^{-1}(U)) \in \cn_{E_i}(0)$, so $T^{-1}(U) \in \mathcal{B} \subset \cn_E(0)$.
 \end{proof}
 
+\begin{definition}[Direct Sum]
+\label{definition:tvs-direct-sum}
+    Let $\seqi{E}$ be TVSs over $K \in \RC$, then there exists $(E, \seqi{\iota})$ such that:
+    \begin{enumerate}
+        \item $E$ is a TVS over $K$. 
+        \item For each $i \in I$, $\iota_i \in L(E_i; E)$. 
+        \item[(U)] For each $(F, \seqi{T})$ satisfying (1) and (2), there exists a unique $T \in L(E; F)$ such that the following diagram commutes:
+        \[
+        \xymatrix{
+        E \ar@{->}[r]^{T} & F \\
+        E_i \ar@{->}[u]^{\iota_i} \ar@{->}[ru]_{T_i} & 
+        }
+        \]
+    \end{enumerate}
+
+    
+    The space $E = \bigoplus_{i \in I}E_i$ is the \textbf{direct sum} of $\seqi{E}$. 
+\end{definition}
+\begin{proof}
+    Let $(E, \seqi{\iota})$ be the direct sum of $\seqi{E}$ as vector spaces, and equip it with the inductive topology induced by $\seqi{\iota}$, then $(E, \seqi{\iota})$ satisfies (1) and (2). 
+
+    (U): By (U) of the \hyperref[direct sum]{definition:direct-sum}, there exists a unique $T \in \hom(E; F)$ such that the diagram commutes. In which case, by (4) of \autoref{definition:tvs-inductive}, $T \in L(E; F)$. 
+\end{proof}
+
+\begin{proposition}
+\label{proposition:finite-tvs-product}
+    Let $\seqf{E_j}$ be TVSs over $K \in \RC$, then
+    \[
+    \prod_{j = 1}^n E_j = \bigoplus_{j = 1}^n E_j
+    \]
+\end{proposition}
+\begin{proof}
+    Let $1 \le k \le n$, then for each $1 \le k, l \le n$, $\pi_l \circ \iota_k \in L(E_k, E_l)$, so by (U) of the \hyperref[product]{definition:tvs-product}, $\iota_k \in L(E_k; \prod_{j = 1}^n E_j)$. Thus $\prod_{j = 1}^n E_j$ satisfies (1) and (2) of the \hyperref[direct sum]{definition:tvs-direct-sum}. 
+
+    For any TVS $F$ over $K$ and $\seqf{T_j}$ with $T_j \in L(E_j; F)$ for each $1 \le j \le n$, let
+    \[
+    T: \prod_{j = 1}^n E_j \to F \quad (x_1, \cdots, x_n) \mapsto \sum_{j = 1}^n T_jx_j
+    \]
+
+    then $T \in L(\prod_{j = 1}^n E_j; F)$ is the unique continuous linear map such that the following diagram commutes:
+    \[
+    \xymatrix{
+    E \ar@{->}[r]^{T} & F \\
+    E_i \ar@{->}[u]^{\iota_i} \ar@{->}[ru]_{T_i} & 
+    }
+    \]
+
+    Hence $\prod_{j = 1}^n E_j$ satisfies (U) of the \hyperref[direct sum]{definition:tvs-direct-sum}, so the spaces coincide. 
+\end{proof}
+
+
+
 \begin{definition}[Inductive Limit]
 \label{definition:tvs-inductive-limit}
     Let $(\seqi{E}, \bracsn{T^i_j| i, j \in I, i \lesssim j})$ be an upward-directed system of TVSs over $K \in \RC$, then there exists $(E, \bracsn{T^i_E}_{i \in I})$ such that: