Solution (source code)

= Solution

<Rouché's theorem> states that if $g$ and $h$ are <holomorphic functions> on a neighbourhood of the closure of a bounded domain and
$$
|h(z)|<|g(z)|
$$
on its positively oriented boundary, then $g$ and $g+h$ have the same number of zeros in the domain, counted with multiplicity.

The <Open mapping theorem (complex analysis)> states that a nonconstant <holomorphic function> on a domain maps every open subset to an open subset. To prove it, fix $z_0$ and put $w_0=f(z_0)$. By the <identity theorem>, the zeros of $f-w_0$ are isolated. Choose $r>0$ so that the closed disc $\overline{D(z_0,r)}$ lies in the domain and $z_0$ is the only zero of $f-w_0$ in that disc. Then
$$
\delta=\min_{|z-z_0|=r}|f(z)-w_0|>0.
$$
Whenever $|w-w_0|<\delta$, the constant $w_0-w$ has <modulus> smaller than $f-w_0$ on the circle. The Rouche theorem therefore says that
$$
f(z)-w=(f(z)-w_0)+(w_0-w)
$$
has the same positive number of zeros in the disc as $f-w_0$. Thus every $w\in D(w_0,\delta)$ lies in the image of $f$, proving that the image is open.

If $|f|$ had a local maximum at $z_0$, take a small <open disc> $D$ on which $|f(z)|\leq|f(z_0)|$. The restriction of $f$ to $D$ cannot be constant, since the identity theorem would then make $f$ constant on the whole domain. The complex open mapping theorem says that $f(D)$ is an open neighbourhood of $f(z_0)$, and such a neighbourhood contains points of <modulus> greater than $|f(z_0)|$, a contradiction. This proves the <maximum modulus principle from the complex open mapping theorem>.

Now let $\Omega$ be bounded. Its closure is compact, so the <continuous> <function> $|f|$ attains a maximum there. If $f$ is nonconstant, the <maximum modulus principle> excludes an interior maximum; if $f$ is constant, the claimed bound is immediate. Hence
$$
\max_{z\in\overline\Omega}|f(z)|
=\max_{z\in\partial\Omega}|f(z)|\leq M,
$$
which is the <maximum modulus principle on a bounded domain>.

Finally let $\Omega=\{z:\operatorname{Re}z>1\}$ and suppose $|f|\leq K$ throughout $\overline\Omega$. Fix $z_0\in\Omega$. The principal <complex logarithm> is holomorphic on the right half-plane, so for each positive integer $n$ the <function>
$$
g_n(z)=f(z)z^{-1/n}
=f(z)\exp\left(-\frac1n\operatorname{Log}z\right)
$$
is holomorphic on $\Omega$ and continuous on its closure. Given $\varepsilon>0$, choose $R>|z_0|$ so large that
$$
K R^{-1/n}\leq M+\varepsilon.
$$
Apply the bounded-domain result to $g_n$ on $\Omega\cap D(0,R)$. On the vertical part of the boundary, $|z|\geq1$ and hence $|g_n(z)|\leq M$. On the circular part,
$$
|g_n(z)|\leq K R^{-1/n}\leq M+\varepsilon.
$$
It follows that
$$
|f(z_0)|\leq(M+\varepsilon)|z_0|^{1/n}.
$$
Letting $n\to\infty$ and then $\varepsilon\to0$ gives $|f(z_0)|\leq M$. Since $z_0$ was arbitrary, this proves the <bounded half-plane maximum principle>.

The boundedness assumption is necessary. The <function>
$$
f(z)=e^z
$$
is holomorphic on $\Omega$ and continuous on its closure, and $|f(1+iy)|=e$ on the boundary, but $|f(x)|=e^x$ is unbounded for real $x>1$. Thus the boundary estimate does not control an unbounded <holomorphic function> on this unbounded domain.