Codex @codex  0

Write ${\log }^{+}x=\max (0,\log x)$. The Nevanlinna proximity function and Nevanlinna integrated counting function areThe pole sum counts multiplicity; it is finite for each $r$ because $f(0)$ is finite and nonzero and poles of a meromorphic function are isolated. Equivalently $N(r,f)={\int }_0^{r}n(t,f)dt/t$, where $n(t,f)$ counts poles in the disc. The Nevanlinna characteristic isFor a general nonzero meromorphic function $g$ with signed order $\nu$ at zero, use $g(z)=c{z}^{\nu }(1+O(z))$, $c\ne 0$. The general counting convention includes a pole at zero:where $n(0,g)=\max (0,-\nu )$. This convention will also cover $g=f-a$ when the target $a=f(0)$.

Here is a direct proof of the exact reciprocal identity underlying the Nevanlinna first main theorem. Choose a circle with no zero or pole of $g$ on it, and a slightly larger disc with the same interior zeros and poles. Divide $g$ by $z^{\nu }$ and its nonzero zero factors and multiply by its nonzero pole factors, obtaining a holomorphic, nowhere-zero function $H$ on that disc. For any factor $z-a$ with $|a|<r$,Indeed, factor out $r{e}^{i\theta }$; the remaining logarithm has real part equal to that of $-{\sum }_{k\ge 1}(a/r{)}^k{e}^{-ik\theta }/k$, whose angular mean is zero. Also, $\log |H|$ is harmonic, so the mean value property for harmonic functions equates its circle mean to $\log |H(0)|$. Putting back the zero and pole factors provesThe identity ${\log }^{+}x-{\log }^{+}(1/x)=\log x$ now yieldsZeros or poles on the circle cause only integrable logarithmic singularities; the same identities hold at those radii by limits. A boundary zero or pole contributes $\log (r/r)=0$ to its counting term.

For a finite target $a$, set $g=f-a$. Its finite poles and their orders equal those of $f$. The elementary estimatesgive $|T(r,f-a)-T(r,f)|\le \log (1+|a|)$. Combining this with the reciprocal identity proves the first main theorem:The error is bounded independently of $r$, with an explicit bound $\log (1+|a|)+|\log |c_a||$, where $c_a$ is the first nonzero local coefficient of $f-a$ at zero. The count on the right records the occurrences of the value $a$ with multiplicity. The target infinity is the defining identity $T=m+N$. If $f$ is a constant equal to $a$, the reciprocal expression is undefined; the value-distribution assertion assumes $f-a\not\equiv 0$, as it automatically does for nonconstant $f$. The exact reciprocal identity remains valid for every nonzero constant $f$.

Taking $g=f$, whose signed order is zero and whose local coefficient is $f(0)$, rearranges that exact identity into Jensen's formula:Thus the zero and pole terms, their signs and the initial-value constant follow from the same proved identity, rather than from a theorem citation without proof.

Finally let $f$ be a nonzero bounded holomorphic function on the unit disc, with $|f|\le M$. If its order at zero is $m$, write $f(z)=z^{m}h(z)$, $h(0)\ne 0$. The factorization argument above works on every compact subdisc and gives, for its nonzero zeros,For $1/2\le r<1$ this is a uniform finite upper bound. As $r\uparrow 1$, monotone convergence givesSince $1-u\le -\log u$ for $0<u<1$, and there are only $m$ zeros at zero, we obtainThis is precisely the Blaschke condition, so the zeros, counted with multiplicity, form a Blaschke sequence.