Added characterisation of positive linear functionals.

src/fa/tvs/complexify.tex

@@ -195,3 +195,28 @@
     
     
 \end{proof}
+
+
+\begin{proposition}
+\label{proposition:hermitian-functional-norm}
+    Let $E$ be a normed vector space over $\complex$, $*: E \to E$ be a complex conjugation map such that $\norm{x}_E = \normn{x^*}_E$ for all $x \in E$, and $\phi \in E^*$ be a Hermitian functional, then
+    \[
+    \norm{\phi}_{E^*} = \sup\bracsn{\dpn{x, \phi}{E}|x \in E, x = x^*, \norm{x}_E = 1}
+    \]
+\end{proposition}
+\begin{proof}
+    Since $\bracsn{x \in E|x = x^*} \subset E$, $\norm{\phi}_{E^*} \ge \sup\bracsn{\dpn{x, \phi}{E}|x \in E, x = x^*, \norm{x}_E = 1}$. 
+
+    On the other hand, let $x \in E$ with $\norm{x}_E = 1$. Assume without loss of generality that $\dpn{x, \phi}{E} \in \real$, then
+    \begin{align*}
+        \dpn{x, \phi}{E} &= \dpn{\text{Re}(x), \phi}{E} + \underbrace{i\dpn{\text{Im}(x), \phi}{E}}_{\in \real} =
+\dpn{\text{Re}(x), \phi}{E} \\
+&\le  \norm{\text{Re}(x)}_E \cdot \sup\bracsn{\dpn{y, \phi}{E}|y \in E, y = y^*, \norm{y}_E = 1}
+    \end{align*}
+
+    where $\norm{\text{Re}(x)}_E = \norm{{(x + x^*)}/{2}}_E \le \norm{x}_E$. As the above holds for all $x \in E$, 
+    \[
+    \norm{\phi}_{E^*} \le \sup\bracsn{\dpn{x, \phi}{E}|x \in E, x = x^*, \norm{x}_E = 1}
+    \]
+\end{proof}
+