Added Hadamard's Three Lines Lemma.

src/dg/complex/zero.tex

@@ -94,3 +94,39 @@
 
     so $Df = 0$ and $f$ is constant. 
 \end{proof}
+
+
+\begin{lemma}[Hadamard's Three Lines Lemma]
+\label{lemma:three-lines}
+    Let $S = \bracs{z \in \complex| \text{Re}(z) \in [0, 1]}$, $E$ be a Banach space over $\complex$, and $f \in H(S; E) \cap BC(\ol{S}; E)$. For each $s \in [0, 1]$, let
+    \[
+    M(\theta) = \sup_{t \in \real}\norm{f(s + it)}_E
+    \]
+
+    then for each $s \in [0, 1]$, $M(s) \le M(0)^s M(1)^{1-s}$. 
+\end{lemma}
+\begin{proof}
+    Assume without loss of generality that $M(0), M(1) > 0$. Let
+    \[
+    g: \complex \to \complex \quad z \mapsto M(0)^z M(1)^{1 - z}
+    \]
+
+    then $g$ is a non-vanishing entire function, and for each $z \in \complex$, 
+    \[
+    |g(z)| = M(0)^{\text{Re}(z)} M(1)^{\text{Re}(1 - z)}
+    \]
+
+    so $|g|^{-1}$ is bounded on $\ol S$ by \autoref{proposition:compact-extensions}. Let
+    \[
+    h: \ol S \to E \quad z \mapsto \frac{f(z)}{g(z)}
+    \]
+
+    then $h \in H(S; E) \cap BC(\ol S; E)$ with $\norm{h(z)}_E \le 1$ for all $z \in \partial S$. By the \hyperref[Maximum Modulus Theorem]{theorem:maximum-modulus-theorem}, $\norm{h(z)}_E \le 1$ for all $z \in S$. Thus for every $z \in S$,
+    \[
+    f(z) \le M(0)^{\text{Re}(z)} M(1)^{1-\text{Re}(z)}
+    \]
+
+    Therefore $M(s) \le M(0)^s M(1)^{1-s}$ for every $s \in [0, 1]$.
+\end{proof}
+
+