Ahlfors–Shimizu area form of the characteristic

Let $p$ be a pole of order $m$. The leading Laurent term in [F3] gives $g=1\mathrm{/}f=(z-p{)}^{m}q(z)$ with $q$ holomorphic and nonzero at $p$ by [F4].

On a pole-free neighbourhood write $f=\alpha +i\beta$. By [F5]–[F6], the Cauchy–Riemann equations and smoothness make $\alpha ,\beta$ harmonic; for $s=\mathrm{\mid }f{\mathrm{\mid }}^2$, direct differentiation gives $\mathrm{\mid }\mathrm{\nabla }s{\mathrm{\mid }}^2=4\mathrm{\mid }f{\mathrm{\mid }}^2\mathrm{\mid }{f}^{\mathrm{\prime }}{\mathrm{\mid }}^2$ and $\mathrm{\Delta }s=4\mathrm{\mid }{f}^{\mathrm{\prime }}{\mathrm{\mid }}^2$. Applying the real chain rule to $\frac{1}{2}\log (1+s)$ yields $\mathrm{\Delta }(\frac{1}{2}\log (1+\mathrm{\mid }f{\mathrm{\mid }}^2))=2\mathrm{\mid }{f}^{\mathrm{\prime }}{\mathrm{\mid }}^2\mathrm{/}(1+\mathrm{\mid }f{\mathrm{\mid }}^2{)}^2=2(f^{\mathrm{\#}}{)}^2$.

For any $p\in \mathbb{C}$ and $r>0$, $M_r\log \mathrm{\mid }r{e}^{it}-p\mathrm{\mid }=\log \max \{r,\mathrm{\mid }p\mathrm{\mid }\}$. If $r\mathrm{\ne }\mathrm{\mid }p\mathrm{\mid }$, factor out the larger of $r$ and $\mathrm{\mid }p\mathrm{\mid }$ and average the uniformly convergent series $\log (1-\zeta )=-{\sum }_{n\ge 1}{\zeta }^n\mathrm{/}n$. If $r=\mathrm{\mid }p\mathrm{\mid }>0$, rotate to $p=r$; then $\mathrm{\mid }r{e}^{it}-p\mathrm{\mid }=2r\mathrm{\mid }\sin (t\mathrm{/}2)\mathrm{\mid }$. The logarithm is integrable since $\sin (t\mathrm{/}2)$ is comparable to the distance from an endpoint near $0$ and $2\pi$. With $J={\int }_0^{\pi \mathrm{/}2}\log (\sin x)dx$, symmetry and $\sin (2x)=2\sin x\cos x$ give $2J=-(\pi \mathrm{/}2)\log 2+J$, hence $J=-(\pi \mathrm{/}2)\log 2$ and the angular mean of $\log (2\mathrm{\mid }\sin (t\mathrm{/}2)\mathrm{\mid })$ is zero. The case $p=0$ is immediate.

Fix a regular radius $r$, so its circle contains no pole, and list the finitely many poles $p$ in $\mathrm{\mid }z\mathrm{\mid }<r$ with orders $m_p$; finiteness follows from [F7]. Integrating the defining count [F1] over its step intervals gives $N(r,\mathrm{\infty };f)=m_0\log r+{\sum }_{0<\mathrm{\mid }p\mathrm{\mid }<r}{m}_p\log (r\mathrm{/}\mathrm{\mid }p\mathrm{\mid })$, where $m_0=0$ if $0$ is not a pole. Each pole at radius $\mathrm{\mid }p\mathrm{\mid }$ contributes $m_p{\int }_{\mathrm{\mid }p\mathrm{\mid }}^{r}dt\mathrm{/}t$.

Put $u_f=\frac{1}{2}\log (1+\mathrm{\mid }f{\mathrm{\mid }}^2)$ away from poles and define $v(z)=u_f(z)+{\sum }_{\mathrm{\mid }p\mathrm{\mid }<r}{m}_p\log \mathrm{\mid }z-p\mathrm{\mid }$. The list is finite by [F7]; since $r$ is regular, it is the full pole set in a slightly larger disc. Near a listed pole $p$, [F3] gives $h_p(z)=(z-p{)}^{m_p}f(z)$ holomorphic and nonzero, so the singular part of $v$ is $\frac{1}{2}\log (\mathrm{\mid }z-p{\mathrm{\mid }}^{2m_p}+\mathrm{\mid }{h}_p(z){\mathrm{\mid }}^2)$. It extends as a $C^2$ function through $p$ by [F6]; all other logarithmic terms are smooth near $p$. Thus $v$ is $C^2$ on a neighbourhood of the closed disc.

Away from poles $f^{\mathrm{\#}}$ is continuous by holomorphic smoothness; at a pole, step 1.1 gives $\mathrm{\mid }{f}^{\mathrm{\prime }}\mathrm{\mid }\mathrm{/}(1+\mathrm{\mid }f{\mathrm{\mid }}^2)=\mathrm{\mid }{g}^{\mathrm{\prime }}\mathrm{\mid }\mathrm{/}(1+\mathrm{\mid }g{\mathrm{\mid }}^2)$ off the pole, which extends continuously there by [F6]. Hence $(f^{\mathrm{\#}}{)}^2$ is continuous and bounded on compact sets, so its absolute area integral is finite by [F8] and $A(t)=O(t^2)$ near zero.

Let $V(t)=M_{t}v$. By step 1.3, $V(r)=m_0\log r+{\sum }_{0<\mathrm{\mid }p\mathrm{\mid }<r}{m}_p\log \max \{r,\mathrm{\mid }p\mathrm{\mid }\}+m(r,\mathrm{\infty };f)$. Using the count formula of step 1.4 gives $T(r,f)=V(r)-{\sum }_{0<\mathrm{\mid }p\mathrm{\mid }<r}{m}_p\log \mathrm{\mid }p\mathrm{\mid }$. At the centre, $V(0)=C_{\mathrm{\infty }}(f)+{\sum }_{0<\mathrm{\mid }p\mathrm{\mid }<r}{m}_p\log \mathrm{\mid }p\mathrm{\mid }$: this follows from continuity of $v$ and the finite value of $u_f(0)$, or from $u_f(z)+m_0\log \mathrm{\mid }z\mathrm{\mid }\to \log \mathrm{\mid }c\mathrm{\mid }$ when $0$ is a pole. Consequently $T(r,f)=V(r)-V(0)+C_{\mathrm{\infty }}(f)$.

Away from the listed poles, every $\log \mathrm{\mid }z-p\mathrm{\mid }$ is harmonic and step 1.2 gives $\mathrm{\Delta }v=2(f^{\mathrm{\#}}{)}^2$. Both sides are continuous on the closed disc by steps 1.5 and 2.1, so the equality holds at the poles as well.

Polar coordinates and step 3.1 give $(t{V}^{\mathrm{\prime }}(t){)}^{\mathrm{\prime }}=t{M}_t(\mathrm{\Delta }v)=2t{M}_t((f^{\mathrm{\#}}{)}^2)=A^{\mathrm{\prime }}(t)$, since $A^{\mathrm{\prime }}(t)={\pi }^{-1}t{\int }_0^{2\pi }(f^{\mathrm{\#}}(t{e}^{i\theta }){)}^{2}d\theta$. The angular second-derivative term in the polar Laplacian integrates to zero.

The function $v$ is $C^2$ at $0$, so $t{V}^{\mathrm{\prime }}(t)\to 0$ as $t\downarrow 0$, while $A(t)\to 0$ by step 2.1. Integrating step 4.1 from $0$ to $r$ gives $t{V}^{\mathrm{\prime }}(t)=A(t)$, and integrating once more gives $V(r)-V(0)={\int }_0^{r}A(t)dt\mathrm{/}t=T_{\mathrm{A}\mathrm{S}}(r,f)$. Step 2.2 now proves the claimed exact identity for every regular radius.

The area function $A$ is continuous and nondecreasing because $(f^{\mathrm{\#}}{)}^2$ is continuous and nonnegative; step 2.1 gives $A(t)=O(t^2)$ and a finite integral $T_{\mathrm{A}\mathrm{S}}$. The derivative of $x\mapsto T_{\mathrm{A}\mathrm{S}}(e^x)$ is $A(e^x)$, which is nondecreasing, so this function is convex. Finally [F7] makes $T=m(r,\mathrm{\infty };f)+N(r,\mathrm{\infty };f)$ continuous across pole radii; $T_{\mathrm{A}\mathrm{S}}$ is continuous because $A$ is. Pole radii are locally finite by [F7], so regular radii approach every $r>0$, and taking this limit in step 5.1 proves the identity there.