Solution (source code)

= Solution

Let $p:\mathbb D\to D$ be a <universal covering map>. On a small evenly covered neighborhood in $D$, choose a local inverse $s$ of $p$ and set
$$
ds_D=\lambda_D(z)|dz|,\qquad
\lambda_D(z)=\frac{2|s'(z)|}{1-|s(z)|^2}.
$$
Any two such lifts differ by a <deck transformation> of the disc. Every <automorphism of the unit disk> preserves the disc density: apply the derivative <Schwarz-Pick lemma> to the automorphism and its inverse to get equality. Hence the definition is independent of the local inverse. Uniqueness of the <universal cover> up to a covering isomorphism gives independence of the chosen cover as well. This is the <Poincare metric on a Riemann surface>, normalized to curvature $-1$.

For a piecewise continuously differentiable path $\gamma$, define its length by $L_D(\gamma)=\int\lambda_D(\gamma)|\gamma'|$, and the distance by the infimum of lengths of joining paths. Path reversal and concatenation prove symmetry and the triangle inequality. The distance between distinct points is positive: choose a small closed Euclidean disc around one point not containing the other, on which the positive continuous density is bounded below by $c>0$. Every joining path must leave that disc and has length at least $c$ times its radius before doing so. Joining paths of finite length exist because a plane domain is path connected and the density is locally bounded. Thus this construction gives an actual <metric>, not just a nonnegative path-length expression.

For the punctured <unit disc>, use $p(w)=e^{iw}$ from the <complex upper half-plane>. The half-plane line element is $|dw|/\operatorname{Im}w$, while $|dz|=|z||dw|$ and $\operatorname{Im}w=\log(1/|z|)$. Consequently
$$
\boxed{ds_A=\frac{|dz|}{|z|\log(1/|z|)}.}
$$
The domain called an annulus in the paper has inner radius zero, so it is this punctured-disc metric, not the metric of an annulus with positive inner radius.

We now prove the <Great Picard theorem>. In its holomorphic form, an <essential singularity> takes every complex value, with at most one exception, infinitely often in every punctured neighborhood. It suffices to prove that a <holomorphic function> on a punctured disc omitting $0$ and $1$ extends meromorphically through the puncture: if two values occurred only finitely often, a smaller punctured disc would omit both, and an affine change of target would reduce them to $0,1$.

Use the <universal covering by the modular lambda function> $\lambda:\mathbb H\to Y=\mathbb C\setminus\{0,1\}$, whose construction is given in the following solution. Its <deck transformation group> is the projective level-two <principal congruence subgroup> $\Gamma(2)$. Rescale the source punctured disc to unit radius. Lift $f(e^{2\pi iw})$ to a <holomorphic function> $L:\mathbb H\to\mathbb H$. Uniqueness of lifts gives
$$
L(w+1)=T L(w)
$$
for a fixed <deck transformation> $T\in\Gamma(2)$. The <Schwarz-Pick lemma> gives
$$
\rho_{\mathbb H}(L(w),T L(w))
\leq\rho_{\mathbb H}(w,w+1)
=2\operatorname{arsinh}\frac1{2\operatorname{Im}w}\longrightarrow0
$$
as $\operatorname{Im}w\to\infty$. A nonidentity deck transformation has no interior fixed point, so it is either a <hyperbolic Möbius transformation> or a <parabolic Möbius transformation>. The hyperbolic case is conjugate to a dilation $w\mapsto aw$ with $a>0$, $a
eq1$. Since $|d\log\operatorname{Im}w|\leq ds_{\mathbb H}$, its displacement is at least $|\log a|>0$, contradicting this inequality.

If $T$ is the identity, compose $L$ with the <Cayley transform between the half-plane and disk>. Its periodicity lets the resulting bounded function descend to the punctured disc and extend by the <Riemann removable singularity theorem>. A nonconstant extension takes its central value inside the disc by the <maximum modulus principle>. The covering map then gives an extension of $f$; a constant lift gives a constant $f$.

In the parabolic case, its fixed point is a rational <modular cusp>. Indeed, a parabolic integral matrix of trace $\pm2$ has a rational eigenvector for its repeated eigenvalue. Conjugate by an element of the <modular group> sending this cusp to infinity. The level-two subgroup is normal, so the conjugated transformation is $\zeta\mapsto\zeta+2n$ for a nonzero integer $n$. The conjugated lift $P$ consequently satisfies
$$
P(w+1)=P(w)+2n,\qquad\operatorname{Im}P(w)>0.
$$
The modular transformations permute the three target cusp values $0,1,\infty$, as seen from the lambda transformation formulas below. It is therefore enough to examine $\lambda(P(w))$.

To fix the sign of $n$, the function $\operatorname{Im}P$ is periodic in the real direction. Its mean $M(y)=\int_0^1\operatorname{Im}P(x+iy)\,dx$ satisfies $M'(y)=2n$ by the <Cauchy-Riemann equations> and the increment of $\operatorname{Re}P$. Positivity for all $y>0$ forces $n>0$. The function
$$
Q(e^{2\pi iw})=e^{\pi iP(w)}
$$
is well-defined, nonvanishing and bounded by one on the punctured disc, so it extends holomorphically to zero. Its <winding number> along a circle around the puncture is $n$, because a unit increment in $w$ increases $\pi iP$ by $2\pi in$. The <argument principle> therefore shows that $Q$ has a zero of order $n$ at the origin.

At the infinite cusp, the <modular lambda function> has the convergent expansion $\lambda(\zeta)=16q+O(q^2)$ in $q=e^{\pi i\zeta}$. Thus $\lambda(P(w))=16Q(z)+O(Q(z)^2)$ extends and tends to zero. Undoing the target permutation gives a removable singularity or a pole for $f$. In every case the puncture is not essential, which proves the holomorphic <Great Picard theorem>. For a meromorphic function with an essential singularity, if three spherical values occurred only finitely often, a <Möbius transformation> would make the omitted values $0,1,\infty$. The same proof applies because omission of infinity makes the transformed function holomorphic. Hence the meromorphic version has at most two exceptional spherical values.