Let be a universal covering map. On a small evenly covered neighborhood in , choose a local inverse of and set
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 .
For a piecewise continuously differentiable path , define its length by , 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 . Every joining path must leave that disc and has length at least 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 from the complex upper half-plane. The half-plane line element is , while and . Consequently
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 and 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 .
Use the universal covering by the modular lambda function , whose construction is given in the following solution. Its deck transformation group is the projective level-two principal congruence subgroup . Rescale the source punctured disc to unit radius. Lift to a holomorphic function . Uniqueness of lifts gives
for a fixed deck transformation . The Schwarz-Pick lemma gives
as . 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 with , . Since , its displacement is at least , contradicting this inequality.
If is the identity, compose 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 ; a constant lift gives a constant .
In the parabolic case, its fixed point is a rational modular cusp. Indeed, a parabolic integral matrix of trace 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 for a nonzero integer . The conjugated lift consequently satisfies
The modular transformations permute the three target cusp values , as seen from the lambda transformation formulas below. It is therefore enough to examine .
To fix the sign of , the function is periodic in the real direction. Its mean satisfies by the Cauchy-Riemann equations and the increment of . Positivity for all forces . The function
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 , because a unit increment in increases by . The argument principle therefore shows that has a zero of order at the origin.
At the infinite cusp, the modular lambda function has the convergent expansion in . Thus extends and tends to zero. Undoing the target permutation gives a removable singularity or a pole for . 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 . The same proof applies because omission of infinity makes the transformed function holomorphic. Hence the meromorphic version has at most two exceptional spherical values.
Use the curvature-minus-one normalization of the hyperbolic metric:
The associated distance is . A connected Riemann surface has its complete canonical Poincare metric on a Riemann surface precisely when its universal cover is conformally the unit disc. By the uniformization theorem, the other simply connected covering types are the complex plane and Riemann sphere. Disc automorphisms preserve , as direct differentiation of shows; therefore the metric descends through the deck group. This is the uniformization notion of hyperbolicity, not the different potential-theoretic Green-function classification.
First prove the needed Schwarz lemma. If is holomorphic and , then extends holomorphically at zero. On its modulus is at most . The maximum modulus principle and give and .
Write . Conjugating by the source and target disc automorphisms, fixes zero. Applying the derivative bound gives
Integrate along any piecewise smooth path and then take the infimum of lengths: . This proves the Schwarz-Pick theorem. Contraction means nonexpansion, not a uniform Lipschitz constant strictly smaller than one; automorphisms preserve all distances.
If both and have disc universal covers, lift to through . The disc is simply connected, so the lift exists, and it is holomorphic because the covering maps are local biholomorphisms. Both covering maps are local hyperbolic isometries. The disc contraction therefore descends to and, by the path-length argument, . If only is known to have a hyperbolic metric, a nonconstant forces to have one too: otherwise lift from the plane or sphere universal cover of to the disc cover of . A bounded entire function is constant by the Liouville theorem, and a holomorphic map from the compact sphere into the disc is constant by the maximum modulus principle. Thus a nonconstant map into a hyperbolic surface is distance-nonincreasing between the canonical hyperbolic metrics; a nonhyperbolic source admits only constant such maps.
For the prescribed point, Schwarz-Pick theorem gives . Therefore
is holomorphic after filling the removable singularity at , and . Inverting the target automorphism proves
Conversely every holomorphic with this bound gives an admissible disc map: , its inverse target automorphism remains in the disc, and the denominator cannot vanish.
Fix and put . The possible intermediate values fill , since constant choices , , attain them all. Thus the one-point value region of a holomorphic disc map is . Completing the square in gives its Euclidean centre and radius:
This closed disc lies strictly inside the unit disc because . For it degenerates to the single point . Its boundary is attainable by unimodular constant ; requiring to map into the open disc does not remove that boundary.