[proofplan] We reduce to the case $M(0), M(1) > 0$ and construct an auxiliary function $F(z) = M(0)^{z-1} M(1)^{-z} f(z)$, which has modulus at most $1$ on the boundary lines $\operatorname{Re}(z) = 0$ and $\operatorname{Re}(z) = 1$. To handle the unbounded strip, we introduce a regularising factor $e^{\varepsilon z^2}$ (for $\varepsilon > 0$) that forces decay as $|\operatorname{Im}(z)| \to \infty$, apply the [Maximum Modulus Principle](/theorems/491) on a large truncated rectangle, and then send $\varepsilon \to 0$. [/proofplan]

[step:Reduce to the case $M(0), M(1) > 0$ and normalise the boundary]If $M(0) = 0$, then $|f(it)| = 0$ for all $t \in \mathbb{R}$, so $f$ vanishes identically on the line $\operatorname{Re}(z) = 0$. For any $x_0 \in (0, 1)$, the sequence $z_n = x_0/n + i \cdot 0$ lies in the open strip $S$ and converges to $0 \in \overline{S}$, with $f(z_n) \to f(0) = 0$ by continuity. Since $f$ is holomorphic on $S$, bounded, and vanishes on the entire boundary line $\{it : t \in \mathbb{R}\}$, we apply the Schwarz reflection principle: reflecting $f$ across the imaginary axis and using the [Identity Theorem for Analytic Functions](/theorems/208) on the reflected domain shows $f \equiv 0$ on $S$. Hence $M(x) = 0$ for all $x \in [0, 1]$, and the inequality $M(x) \le M(0)^{1-x} M(1)^x = 0$ holds (with the convention $0^a = 0$ for $a > 0$; at $x = 0$ the bound is $M(0)^1 M(1)^0 = 0$, which is also satisfied). The case $M(1) = 0$ is handled symmetrically by reflecting the strip. So we may assume $M(0), M(1) > 0$. Define the auxiliary function \begin{align*} F: \overline{S} &\to \mathbb{C} \\ z &\mapsto M(0)^{z-1} \cdot M(1)^{-z} \cdot f(z), \end{align*} where $M(0)^{z-1} = e^{(z-1)\log M(0)}$ and $M(1)^{-z} = e^{-z \log M(1)}$ use the real-valued logarithms $\log M(0)$ and $\log M(1)$. The function $F$ is holomorphic on $S$ and continuous on $\overline{S}$. On the boundary $\operatorname{Re}(z) = 0$, write $z = it$: \begin{align*} |F(it)| &= M(0)^{-1} \cdot 1 \cdot |f(it)| \le M(0)^{-1} \cdot M(0) = 1. \end{align*} On the boundary $\operatorname{Re}(z) = 1$, write $z = 1 + it$: \begin{align*} |F(1+it)| &= 1 \cdot M(1)^{-1} \cdot |f(1+it)| \le M(1)^{-1} \cdot M(1) = 1. \end{align*} Moreover, since $f$ is bounded on $\overline{S}$, there exists $B > 0$ with $|f(z)| \le B$ for all $z \in \overline{S}$. Hence $|F(z)| \le M(0)^{x-1} M(1)^{-x} B$ for $z = x + it$, which is bounded on $\overline{S}$. It suffices to show $|F(z)| \le 1$ for all $z \in \overline{S}$, since this gives $|f(z)| \le M(0)^{1-x} M(1)^x$ for $z = x + it$.[/step]

[guided]If $M(0) = 0$, then $|f(it)| = 0$ for all $t \in \mathbb{R}$, meaning $f$ vanishes on the entire line $\operatorname{Re}(z) = 0$. We need to show $f \equiv 0$ on the strip. The [Identity Theorem for Analytic Functions](/theorems/208) requires zeros to accumulate at a point in the domain of holomorphy. The zeros of $f$ on $\operatorname{Re}(z) = 0$ lie on the boundary of $S$, not in its interior, so we cannot apply the identity theorem directly. Instead, we use the Schwarz reflection principle: define $g(z) = f(z)$ for $z \in \overline{S}$ and $g(z) = \overline{f(\bar{z})}$ for $\operatorname{Re}(z) < 0$. Since $f(it) = 0$ for all $t$, the function $g$ is holomorphic on the wider strip $\{-1 < \operatorname{Re}(z) < 1\}$. The zeros $\{it : t \in \mathbb{R}\}$ accumulate at $0$, which is now an interior point, so by the [Identity Theorem for Analytic Functions](/theorems/208), $g \equiv 0$, hence $f \equiv 0$ on $S$. Therefore $M(x) = 0$ for all $x \in [0,1]$. At each $x$, the bound $M(x) \le M(0)^{1-x} M(1)^x$ holds: for $x \in (0,1)$, both sides are $0$ (using the convention $0^a = 0$ for $a > 0$); at $x = 0$, the RHS is $M(0)^1 M(1)^0 = 0$; at $x = 1$, the RHS is $M(0)^0 M(1)^1 = M(1)$, and $M(1) = \sup_t |f(1+it)| = 0$ since $f \equiv 0$. The case $M(1) = 0$ is symmetric. We assume $M(0), M(1) > 0$ for the rest of the proof. The normalisation strategy is: multiply $f$ by a holomorphic function of $z$ alone that adjusts the modulus to be at most $1$ on both boundary lines. Define \begin{align*} F(z) &= M(0)^{z-1} \cdot M(1)^{-z} \cdot f(z), \end{align*} where $M(0)^{z-1} := e^{(z-1)\log M(0)}$ and $M(1)^{-z} := e^{-z\log M(1)}$. These exponentials use the real logarithm (since $M(0), M(1) > 0$), so they are entire functions of $z$. Why this particular choice? The modulus of $M(0)^{z-1}$ is $M(0)^{\operatorname{Re}(z)-1} = M(0)^{x-1}$, and the modulus of $M(1)^{-z}$ is $M(1)^{-\operatorname{Re}(z)} = M(1)^{-x}$. So $|F(x+it)| = M(0)^{x-1} M(1)^{-x} |f(x+it)|$. On $x = 0$: $|F(it)| = M(0)^{-1} |f(it)| \le 1$. On $x = 1$: $|F(1+it)| = M(1)^{-1} |f(1+it)| \le 1$. The exponential multiplier is tuned to normalise the supremum to $1$ on each boundary line. If we can show $|F(z)| \le 1$ throughout the strip, then $|f(z)| = M(0)^{1-x} M(1)^x |F(z)| \le M(0)^{1-x} M(1)^x$, which gives the result.[/guided]

[step:Introduce the regularising factor $e^{\varepsilon z^2}$ to ensure decay at infinity]The strip $S$ is unbounded, so we cannot directly apply the [Maximum Modulus Principle](/theorems/491). For each $\varepsilon > 0$, define \begin{align*} F_\varepsilon: \overline{S} &\to \mathbb{C} \\ z &\mapsto F(z) \cdot e^{\varepsilon z^2}. \end{align*} The function $F_\varepsilon$ is holomorphic on $S$ and continuous on $\overline{S}$. For $z = x + it$ with $x \in [0, 1]$: \begin{align*} |e^{\varepsilon z^2}| &= |e^{\varepsilon(x+it)^2}| = |e^{\varepsilon(x^2 - t^2 + 2ixt)}| = e^{\varepsilon(x^2 - t^2)}. \end{align*} Since $x \in [0, 1]$, we have $x^2 \le 1$, so $|e^{\varepsilon z^2}| = e^{\varepsilon(x^2 - t^2)} \le e^{\varepsilon(1 - t^2)}$. As $|t| \to \infty$, this factor decays to zero. Hence $|F_\varepsilon(z)| \to 0$ as $|\operatorname{Im}(z)| \to \infty$, uniformly for $x \in [0, 1]$. On the left boundary ($x = 0$): $|e^{\varepsilon(it)^2}| = e^{-\varepsilon t^2} \le 1$, so $|F_\varepsilon(it)| \le |F(it)| \le 1$. On the right boundary ($x = 1$): $|e^{\varepsilon(1+it)^2}| = e^{\varepsilon(1 - t^2)} \le e^{\varepsilon}$, so $|F_\varepsilon(1+it)| \le |F(1+it)| \cdot e^{\varepsilon} \le e^{\varepsilon}$.[/step]

[guided]The maximum modulus principle applies to bounded domains. The strip $S = \{0 < \operatorname{Re}(z) < 1\}$ is unbounded (it extends infinitely in the imaginary direction), so we need a trick to reduce to a bounded domain. The standard technique is to multiply by a factor that decays as $|\operatorname{Im}(z)| \to \infty$, making the function negligible far from the real axis. The factor $e^{\varepsilon z^2}$ works: for $z = x + it$, \begin{align*} |e^{\varepsilon z^2}| &= e^{\varepsilon \operatorname{Re}(z^2)} = e^{\varepsilon(x^2 - t^2)}. \end{align*} Since $x \in [0, 1]$, the term $x^2 - t^2 \le 1 - t^2 \to -\infty$ as $|t| \to \infty$, giving the decay $|e^{\varepsilon z^2}| \to 0$. Define $F_\varepsilon(z) = F(z) e^{\varepsilon z^2}$, which is holomorphic on $S$ (product of holomorphic functions) and continuous on $\overline{S}$. On the boundary $\operatorname{Re}(z) = 0$: $|e^{\varepsilon(it)^2}| = e^{-\varepsilon t^2} \le 1$, so $|F_\varepsilon(it)| \le |F(it)| \le 1$. On the boundary $\operatorname{Re}(z) = 1$: $|e^{\varepsilon(1+it)^2}| = e^{\varepsilon(1-t^2)}$. When $|t| \ge 1$, this is $\le 1$, so $|F_\varepsilon(1+it)| \le |F(1+it)| \le 1$. When $|t| < 1$, the factor $e^{\varepsilon(1-t^2)} \le e^{\varepsilon}$, so $|F_\varepsilon(1+it)| \le 1 \cdot e^{\varepsilon} = e^{\varepsilon}$. This means the boundary bound on the right side is $e^{\varepsilon}$ rather than $1$. This is acceptable: the [Maximum Modulus Principle](/theorems/491) on the truncated rectangle will give $|F_\varepsilon(z)| \le e^{\varepsilon}$ throughout the strip, and when we send $\varepsilon \to 0^+$ in the next step, the bound tightens to $|F(z)| \le 1$. The key property is: since $F$ is bounded on $\overline{S}$ and $|e^{\varepsilon z^2}| \to 0$ as $|t| \to \infty$ (uniformly in $x \in [0,1]$), we have $|F_\varepsilon(z)| \to 0$ as $|\operatorname{Im}(z)| \to \infty$.[/guided]

[step:Apply the [Maximum Modulus Principle](/theorems/491) on a truncated rectangle and send $\varepsilon \to 0$] Choose $T > 0$ large enough so that $|F_\varepsilon(z)| \le 1$ whenever $|\operatorname{Im}(z)| \ge T$ and $\operatorname{Re}(z) \in [0, 1]$. This is possible because $|F_\varepsilon(z)| \to 0$ as $|\operatorname{Im}(z)| \to \infty$. Consider the closed rectangle \begin{align*} R_T &= \{z \in \mathbb{C} : 0 \le \operatorname{Re}(z) \le 1, \, |\operatorname{Im}(z)| \le T\}. \end{align*} The function $F_\varepsilon$ is holomorphic on the interior of $R_T$ and continuous on $R_T$. By the [Maximum Modulus Principle](/theorems/491) applied to the bounded domain $\operatorname{int}(R_T)$, the maximum of $|F_\varepsilon|$ on $R_T$ is attained on $\partial R_T$. The boundary $\partial R_T$ consists of: - The left side $\{0\} \times [-T, T]$: $|F_\varepsilon(it)| \le 1$. - The right side $\{1\} \times [-T, T]$: $|F_\varepsilon(1+it)| \le e^{\varepsilon}$ (since $|F(1+it)| \le 1$ and $|e^{\varepsilon(1+it)^2}| = e^{\varepsilon(1-t^2)} \le e^{\varepsilon}$). - The top and bottom $[0, 1] \times \{\pm T\}$: $|F_\varepsilon(z)| \le 1$ by the choice of $T$. Therefore $|F_\varepsilon(z)| \le e^{\varepsilon}$ for all $z \in R_T$. For $z$ with $|\operatorname{Im}(z)| > T$, we already have $|F_\varepsilon(z)| \le 1 \le e^{\varepsilon}$. Hence $|F_\varepsilon(z)| \le e^{\varepsilon}$ for all $z \in \overline{S}$. Now fix any $z_0 = x_0 + it_0 \in \overline{S}$. For every $\varepsilon > 0$: \begin{align*} |F(z_0)| \cdot e^{\varepsilon(x_0^2 - t_0^2)} = |F_\varepsilon(z_0)| &\le e^{\varepsilon}. \end{align*} Sending $\varepsilon \to 0^+$: the left side converges to $|F(z_0)| \cdot 1 = |F(z_0)|$ and the right side to $1$. Therefore $|F(z_0)| \le 1$.[/step]

[guided]We want to show $|F(z)| \le 1$ on $\overline{S}$. We use $F_\varepsilon$ as a proxy. Since $F$ is bounded on $\overline{S}$ (say $|F(z)| \le C$) and $|e^{\varepsilon z^2}| = e^{\varepsilon(x^2 - t^2)} \le e^{\varepsilon} \cdot e^{-\varepsilon t^2}$, we get $|F_\varepsilon(z)| \le Ce^{\varepsilon} e^{-\varepsilon t^2}$. For $|t|$ large enough (depending on $\varepsilon$), this is less than $1$. Specifically, choose $T = T(\varepsilon)$ such that $Ce^{\varepsilon} e^{-\varepsilon T^2} < 1$, i.e., $T > \sqrt{(\log C + \varepsilon)/\varepsilon}$. On the rectangle $R_T = [0,1] \times [-T, T]$, the [Maximum Modulus Principle](/theorems/491) applies (the interior is a bounded domain, $F_\varepsilon$ is holomorphic there and continuous on the closure). The maximum of $|F_\varepsilon|$ on $R_T$ is attained on $\partial R_T$, which we bound: - Left side ($x = 0$): $|F_\varepsilon(it)| = |F(it)| e^{-\varepsilon t^2} \le 1 \cdot 1 = 1$. - Right side ($x = 1$): $|F_\varepsilon(1+it)| = |F(1+it)| e^{\varepsilon(1-t^2)} \le 1 \cdot e^{\varepsilon}$ (using $|F(1+it)| \le 1$ and $1 - t^2 \le 1$). - Top/bottom ($|t| = T$): $|F_\varepsilon(z)| \le 1$ by the choice of $T$. So $|F_\varepsilon(z)| \le e^{\varepsilon}$ on $R_T$, and also $|F_\varepsilon(z)| \le 1 \le e^{\varepsilon}$ outside $R_T$. Hence $|F_\varepsilon(z)| \le e^{\varepsilon}$ on $\overline{S}$. Now fix $z_0 \in \overline{S}$. We have $|F(z_0)| \cdot |e^{\varepsilon z_0^2}| \le e^{\varepsilon}$ for all $\varepsilon > 0$. As $\varepsilon \to 0^+$, the factor $|e^{\varepsilon z_0^2}| = e^{\varepsilon \operatorname{Re}(z_0^2)} \to e^0 = 1$, so $|F(z_0)| \le \lim_{\varepsilon \to 0^+} e^{\varepsilon} = 1$.[/guided]

[step:Conclude the three-lines inequality $M(x) \le M(0)^{1-x} M(1)^x$]We have shown $|F(z)| \le 1$ for all $z \in \overline{S}$. Recalling $F(z) = M(0)^{z-1} M(1)^{-z} f(z)$, we take moduli with $z = x + it$: \begin{align*} M(0)^{x-1} M(1)^{-x} |f(x + it)| = |F(x + it)| &\le 1. \end{align*} Rearranging: \begin{align*} |f(x + it)| &\le M(0)^{1-x} M(1)^x. \end{align*} Since this holds for all $t \in \mathbb{R}$, taking the supremum over $t$: \begin{align*} M(x) = \sup_{t \in \mathbb{R}} |f(x + it)| &\le M(0)^{1-x} M(1)^x. \end{align*} Taking logarithms: $\log M(x) \le (1-x)\log M(0) + x \log M(1)$, which is the statement that $\log M(x)$ is a convex function of $x$ on $[0, 1]$.[/step]

[guided]We established in the previous step that $|F(z)| \le 1$ for all $z \in \overline{S}$. Now we translate this back to the original function $f$. Recall the definition $F(z) = M(0)^{z-1} M(1)^{-z} f(z)$, so $f(z) = M(0)^{1-z} M(1)^z F(z)$. Taking moduli at $z = x + it$ (where $x \in [0,1]$, $t \in \mathbb{R}$): the factor $M(0)^{1-z}$ has modulus $M(0)^{1-x}$ (since $|e^{(1-z)\log M(0)}| = e^{(1-x)\log M(0)} = M(0)^{1-x}$, the imaginary part of $z$ contributes only a phase), and similarly $|M(1)^z| = M(1)^x$. Therefore: \begin{align*} |f(x + it)| &= M(0)^{1-x} M(1)^x |F(x + it)| \le M(0)^{1-x} M(1)^x \cdot 1 = M(0)^{1-x} M(1)^x. \end{align*} This bound holds for every $t \in \mathbb{R}$. Taking the supremum over $t$: \begin{align*} M(x) = \sup_{t \in \mathbb{R}} |f(x + it)| &\le M(0)^{1-x} M(1)^x. \end{align*} This is the three-lines inequality. For the convexity interpretation, take logarithms of both sides: $\log M(x) \le (1-x)\log M(0) + x \log M(1)$. The right-hand side is the linear interpolation between $\log M(0)$ and $\log M(1)$, so this says exactly that the graph of $x \mapsto \log M(x)$ lies below every chord — i.e., $\log M$ is convex on $[0, 1]$.[/guided]