Rational composition law for the Nevanlinna characteristic (source code)

= Rational composition law for the Nevanlinna characteristic
{title2=$T_{U\circ f}(r)=dT_f(r)+O(1)$}

For a degree-$d$ <rational function> $U$ of the <Riemann sphere>, choose relatively prime homogeneous <polynomials> $(P,Q)$ of degree $d$. Their joint norm on the unit three-sphere has positive lower and finite upper bounds. Thus $\log\|(P,Q)(v)\|-d\log\|v\|$ is bounded. Averaging over a circle using a nonvanishing entire homogeneous lift of a <meromorphic function> proves the displayed law for the spherical characteristic. <Jensen's formula> and $0\le\tfrac12\log(1+x^2)-\log^+x\le\tfrac12\log2$ show that it also holds for the ordinary <Nevanlinna characteristic>.