Reference request for "Elementary" Proofs of Picard's Great Theorem

Question

This is Picard's Great Theorem;

$\textbf{Great Picard Theorem.}$ Suppose an analytic function $f$ has an essential singularity at $z=a$. Then in each neighbourhood of $a$, $f$ assumes each complex number with one possible exception, an infinite number of times.

I was wondering if there are any essentially elementary proofs of Picard's Great Theorem that could be taught to a student not well versed in complex analysis. Or a relatively short proof that could be taught to a student who has taken at least one semester of complex analysis. Also how many different proofs of this theorem are there?

The proof I have seen, using normal families and Montel's Theorem, is the one in John B Conway's Functions of One Complex Variable. The proof is in Chapter 12 Section 4 and uses quite a number of results that aren't immediately apparent and many of the intermediary results are quite long.

If anyone could point me to a book that provides the kind of proof I'm looking for, or explain that such a proof does not exist, I would appreciate it.

Answer 1

The most elementary proof I know uses Zalcman's lemma. You can find it in chapter 12 of Theodore W. Gamelin's "Complex Analysis" book. The proof is somewhat magical but quite short (two pages) compared to other proofs and doesn't require as much background. The basic ingredients are:

1. A generalization of Arzela-Ascoli for meromorphic functions called Marty's theorem that states that a family of meromorphic functions is normal if and only if their spherical derivatives are uniformly bounded on each compact set. Since meromorphic functions are maps into the Riemann sphere, one needs to define an appropriate notion of derivative which takes into account that points with large modulus should be close to each other and then applies Arzela-Ascoli.
2. A result called Zalcman's lemma which roughly says that if a family is not normal, then by choosing an appropriate sequence of functions, an appropriate sequence of points and "zooming it" (rescaling) around the points fast enough, you can make the sequence converge uniformly to a non-constant meromorphic function. The idea is to perform the rescaling in a way that makes the spherical derivatives bounded and use Marty's theorem. This idea plays a role also in the theory of $J$-holomorphic curves where it is used to extract spherical bubbles from a sequence of $J$-holomorphic curves with bounded energy.