Borel–Carathéodory theorem

Remarks

Proof idea: first let $f(0) = 0$ and $f$ not constant, so that $A(R) > 0$ by the mean value property of $\operatorname{Re} f$. Then $g = f / (2A(R) - f)$ maps the disc of radius $R$ into the unit disc with $g(0) = 0$. The Schwarz lemma gives $\abs{g(z)} \le \abs{z}/R$, and solving for $f$ gives $\abs{f(z)} \le \frac{2r A(R)}{R - r}$ on $\abs{z} = r$. In general, apply this to $f - f(0)$, whose real part is at most $A(R) + \abs{f(0)}$ on $\abs{z} = R$. Example: a real constant $f = c \le 0$ gives equality. The left side is $\abs{c}$, and the right side is $\frac{2rc + (R + r)\abs{c}}{R - r} = \abs{c}$.

Going deeper

For a student

The theorem is a standard tool for entire functions and in analytic number theory. A typical use is to bound $\log f$ when $f$ has no zeros in a disc. There $\operatorname{Re} \log f = \log \abs{f}$ is easy to bound from above. The theorem then bounds $\abs{\log f}$ and, through Cauchy's estimates, its derivatives. This is a step in the proof of the Hadamard factorization theorem and in zero-free region arguments for the Riemann zeta function.