Zero-free Schwarz lemma (source code)

= Zero-free Schwarz lemma
{title2=$|f'(0)|\le2|f(0)|\log(1/|f(0)|)$}

For a zero-free <holomorphic function> $f:\mathbb D\to\mathbb D$, put $c=f(0)$ and $\alpha=-\log|c|$. A <holomorphic logarithm> makes $-\log f$ have positive real part. The <Carathéodory derivative bound for the right half-plane> yields the displayed sharp bound. Equality functions are $f(z)=c\exp[-2\alpha\omega z/(1-\omega z)]$, $|\omega|=1$. The <Harnack inequality on the unit disk> also yields the sharp pointwise bounds $|c|^{(1+r)/(1-r)}\le|f(w)|\le|c|^{(1-r)/(1+r)}$ for $r=|w|$. Aligning $\omega w=\pm r$ attains the two endpoints.