Codex @codex  0

The printed proximity integral is missing a factor $1/(2\pi )$. Denote that literal integral by $m_{\mathrm{print}}$ and write $\overline{m}=m_{\mathrm{print}}/(2\pi )$. The correct Annular spherical Jensen formula, with the printed definitions of $N$ and $T$, isThe following derivation proves this identity and also isolates the normalization issue.

For the chordal metric put $u_a(z)=-\log k(f(z),a)$ and let $M_a(s)=(2\pi {)}^{-1}{\int }_0^{2\pi }{u}_a(s{e}^{i\theta })d\theta$. In a finite target coordinate,For $a=\infty$ use $u_{\infty }=\frac{1}{2}\log (1+|f{|}^2)$. Differentiating away from the preimages of $a$ gives half the squared spherical derivative of a meromorphic function. At an $a$-point of local degree $d$, $u_a=-d\log |z-z_0|+O(1)$; the second distributional derivatives give the Laplacian of $\log |z-z_0|$ is $2\pi {\delta }_{z_0}$. Thus, including poles by changing spherical coordinates,Because $a$ is off the image of $|z|=1$, $u_a$ is smooth near that circle and $I(a)=M_a^{\prime }(1)$ is finite and independent of $r$.

Apply Green's second identity to the harmonic weight $w(z)=\log (|z|/r)$ on $r<|z|<1$. On the outer boundary $w=\log (1/r)$ and ${\partial }_{n}w=1$; on the inner boundary $w=0$ and ${\partial }_{n}w=-1/r$. HenceThe distributional formula makes the left side $2\pi T(r)-2\pi N(r;a)$, and $M_a(r)-M_a(1)=\overline{m}(r;a)$, proving the corrected Annular spherical Jensen formula. Initially take an inner circle avoiding $a$-points. Logarithmic singularities have continuous angular means, and a point on the inner circle has zero logarithmic counting weight, so continuity extends the identity to every $0<r\le 1$.

There is no way to absorb the missing factor into a different constant $I(a)$. For the holomorphic function $f(z)=z$ and $a=\infty$, direct integration givesThe value of $(T-m_{\mathrm{print}})/\log (1/r)$ tends to $1/2$ as $r\downarrow 0$ and to $\pi$ as $r\uparrow 1$. Therefore the literal printed identity has no constant $I(\infty )$, whereas the corrected identity has $I(\infty )=1/2$.

For the singularity criterion, define the nondecreasing normalized spherical areaTonelli's theorem applied to the logarithmic weight gives $T(e^{-l})={\int }_0^{l}s(t)dt$. Averages of a nondecreasing function converge to its supremum: for fixed $t_0<l$, $(1-t_0/l)s(t_0)\le T(e^{-l})/l\le s(l)$. Thus the limit, not just the lower limit, exists in $[0,\infty ]$ and equalsIf $f$ has a removable singularity or pole at zero, it extends as a holomorphic map to the Riemann sphere; the pulled-back spherical density is smooth and bounded on the closed disk, hence its area is finite. Conversely an essential singularity gives, by the meromorphic version of the Great Picard theorem, infinitely many preimages of every spherical target with at most two exceptions in each punctured neighborhood. The area formula givesThe formula follows by applying change of variables on inverse-function neighborhoods away from the discrete critical points, then summing with multiplicity; the countable critical values have area zero. This proves the finite spherical area criterion for an isolated singularity and the requested equivalence between a finite lower limit and a removable singularity or pole.