Definition 27.1.1 (Complex Analytic).label Let $E$ be a separated locally convex space over $\complex$, $U \subset \complex$, and $f: U \to E$, then the following are equivalent:
- (1)
$f \in C^{1}(U; E)$.
- (2)
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}\]
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 Proposition 10.4.1, $L \in L(\complex; E)$. By Proposition 26.6.2, $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$.$\square$