Finite spherical area criterion for an isolated singularity (source code)

= Finite spherical area criterion for an isolated singularity

A <meromorphic function> on a punctured disk has finite pulled-back spherical area precisely when it extends to the <Riemann sphere> at the puncture. A removable singularity or <pole> gives a smooth spherical extension and finite area. At an <essential singularity>, the meromorphic version of the <Great Picard theorem> gives infinitely many preimages of all but at most two spherical targets. The <area formula> then makes the area infinite. The logarithmically weighted annular area divided by $\log(1/r)$ tends to the total unweighted area divided by $4\pi$, by averaging a nondecreasing area function.