Added the principal logarithm.

src/dg/complex/derivative.tex

@@ -0,0 +1,34 @@
+\section{Complex Differentiability}
+\label{section:complex-derivative}
+
+\begin{definition}[Complex Analytic]
+\label{definition:complex-analytic}
+    Let $E$ be a separated locally convex space over $\complex$, $U \subset \complex$, and $f: U \to E$, then the following are equivalent:
+    \begin{enumerate}
+        \item $f \in C^1(U; E)$. 
+        \item Under the identification of $C = \real^2$, $\frac{\partial f}{\partial x}, \frac{\partial f}{\partial y} \in C(U; E)$ and
+        \[
+        \frac{\partial f}{\partial x} = i\frac{\partial f}{\partial y}
+        \]
+    \end{enumerate}
+\end{definition}
+\begin{proof}
+    (1) $\Rightarrow$ (2): Let $x_0 \in U$, then
+    \[
+    \frac{\partial f}{\partial x} = \lim_{\substack{h \to 0 \\ h \in \real}}\frac{f(x_0 + h) - f(x_0)}{h} 
+    = \lim_{h \to 0}\lim_{\substack{h \to 0 \\ h \in \real}}\frac{f(x_0 + ih) - f(x_0)}{ih} = \frac{1}{i} \frac{\partial f}{\partial y}
+    \]
+
+    (2) $\Rightarrow$ (1): Let $x_0 \in U$ and
+    \[
+    L: \complex \to E \quad a + bi \mapsto a \frac{\partial f}{\partial x}(x_0) + b \frac{\partial f}{\partial y}(x_0)
+    \]
+
+    by assumption and \autoref{proposition:polarisation-linear}, $L \in L(\complex; E)$. By \autoref{proposition:partial-total-derivative}, $f \in C^1(U \subset \real^2; E)$, where for any $(a, b) \in \real^2$, 
+    \[
+    Df(x_0)(a, b) = a \frac{\partial f}{\partial x}(x_0) + b \frac{\partial f}{\partial y}(x_0)
+    \]
+
+    so by definition of differentiability, $f$ is complex-differentiable at $x_0$ with derivative $L$. 
+\end{proof}
+