Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 9 results · all verified · 4 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 5 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Jensen Theory and Nevanlinna's First Main Theorem

1 · Prerequisites

2 · Summary

The Poisson–Jensen formula is the exact pointwise identity behind value distribution: on a disc, $\log ∣ f ∣$ is the Poisson average of its boundary values, corrected by the zeros and poles through the disc Green kernel $G_{R} (z, a) = \log ∣ (R^{2} - \overline{a} z) / (R (z - a)) ∣$ . The page proves it for a meromorphic $f$ on a neighbourhood of the closed disc, first at radii free of divisor points and then at a divisor radius through the angular $L^{1}$ limit.

The second half builds the counting, chordal proximity and characteristic functions of Nevanlinna theory. Counts use closed discs with local multiplicity; the integrated count regularises a divisor at the centre by $n (0, a) \log r$ ; and the chordal distance is normalised to diameter one, so it is half the Euclidean chord of the unit sphere's stereographic projection. Well-definedness, finiteness and the continuity of $N$ and $m$ across divisor radii are proved rather than assumed, including the $a = \infty$ convention that counts poles with their orders and the exact base-radius shift.

The centre-divisor Jensen identity turns the pointwise chordal identity $\log (1 / δ (f, a)) = \frac{1}{2} \log (1 + ∣ f ∣^{2}) + \frac{1}{2} \log (1 + ∣ a ∣^{2}) - \log ∣ f - a ∣$ into Nevanlinna's First Main Theorem $m (r, a; f) + N (r, a; f) = T (r, f) + C (f, a)$ , with the exact constant $C (f, a) = \frac{1}{2} \log (1 + ∣ a ∣^{2}) - \log ∣ c_{a} ∣$ at a finite target and $C (f, \infty) = 0$ ; the first nonzero Laurent coefficient $c_{a}$ of $f - a$ at the centre replaces the undefined expression $\log ∣ f (0) - a ∣$ . The Ahlfors–Shimizu area identity $T = T_{A S} + C_{\infty}$ is derived from the pole-corrected spherical potential, which also supplies monotonicity and log-radius convexity of the characteristic.

The final items derive the elementary characteristic laws for products, sums, inverses and fixed rational compositions, define order and lower order by $\log T (r, f) / \log r$ , prove that the Nevanlinna order of an entire function agrees with its maximum-modulus order, and characterise rational functions as exactly the nonconstant meromorphic functions with $T (r, f) = O (\log r)$ .

Every argument on this page is choice-free: divisor lists on bounded discs are finite, and the only nontrivial selection principle used is the well-ordering principle for the natural numbers.

3 · Logical flowchart

4 · Definitions, theorems and proofs

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-30Open item page →

Poisson–Jensen formula for a meromorphic function on a disc

Statement

Let $f$ be a meromorphic function on a neighbourhood of the closed disc $∣ z ∣ \leq R$ , not identically zero, and suppose first that it has no zero or pole on $∣ z ∣ = R$ . For $∣ z ∣ < R$ away from the zeros and poles of $f$ ,

$\log ∣ f (z) ∣ = \frac{1}{2 π} \int_{0}^{2 π} \frac{R^{2} - ∣ z ∣^{2}}{∣ R e^{i t} - z ∣^{2}} \log ∣ f (R e^{i t}) ∣ d t - \sum_{∣ b ∣ < R, f (b) = 0} m_{b} G_{R} (z, b) + \sum_{∣ p ∣ < R, p a pole} ν_{p} G_{R} (z, p) .$

where each distinct zero $b$ and pole $p$ is included once, $m_{b}$ is the zero multiplicity, $ν_{p}$ is the pole order, and

$G_{R} (z, a) = \log ∣ \frac{R^{2} - \overline{a} z}{R (z - a)} ∣ .$

At a radius meeting a zero or pole on its boundary, the identity means the limit through regular radii increasing to that radius; a boundary divisor has Green contribution zero in that limit.

Facts & Assumptions

Given: A meromorphic $f$ on a neighbourhood of $∣ z ∣ \leq R$ , with no boundary divisor for the regular-radius case.

[F1]

A nonzero holomorphic function has only isolated zeros (Zeros of a nonzero holomorphic function are isolated).

[F2]

Every pole has a neighbourhood containing no other pole (Poles of a meromorphic function form a closed discrete set and are at most countable).

[F3]

A zero of finite order factors locally as $(z - a)^{m} g (z)$ with $g (a) \neq 0$ (The order of a zero is the exponent in its local holomorphic factorization).

[F4]

A pole of order $m$ has a reciprocal with a zero of order $m$ (Characterizations of poles).

[F5]

A harmonic function on a neighbourhood of a closed disc is given inside by the Poisson integral of its boundary values (A harmonic function is recovered from its values on any containing circle by the Poisson formula).

[F6]

The real and imaginary parts of a holomorphic function satisfy the Cauchy–Riemann equations (Complex differentiability is equivalent to real total differentiability together with a complex-linear derivative, with $\partial_{\overset{ˉ}{z}} f = 0$ , or with the Cauchy–Riemann equations).

[F7]

A holomorphic function is smooth (Holomorphic functions are real analytic and smooth in their two real coordinates).

Proof

technique · factor each divisor with a disc Blaschke factor, then apply Poisson representation to the zero-free remainder

1.1F1F2F4given

On a regular closed disc there are finitely many zeros and poles: [F1] and [F2] make each divisor discrete, while a divisor cannot accumulate at a pole because [F4] makes $1 / f$ holomorphic with a zero there. List the zeros $b$ with multiplicities $m_{b}$ and poles $p$ with orders $ν_{p}$ .

1.2algebra

For every $∣ a ∣ < R$ , set $B_{a} (z) = R (z - a) / (R^{2} - \overline{a} z)$ . Its denominator is nonzero on a neighbourhood of the closed disc; it has one simple zero at $a$ , and direct modulus calculation gives $∣ B_{a} (R e^{i t}) ∣ = 1$ and $\log ∣ B_{a} (z) ∣ = - G_{R} (z, a)$ .

1.3

Form

g (z) = f (z) \frac{\prod_{p} B_{p} (z)^{ν_{p}}}{\prod_{b} B_{b} (z)^{m_{b}}} .

By [F3], each zero factor cancels locally against the corresponding denominator factor; by [F4], each pole is cancelled by the numerator factor. Thus $g$ is holomorphic and nowhere zero on a neighbourhood of the closed disc, and $∣ g ∣ = ∣ f ∣$ on the boundary. [F3, F4, step 1.1, step 1.2, given]

2.1F6F7step 1.3

To see that $u = \log ∣ g ∣$ is harmonic, near any point $w$ shrink a disc until $∣ g (z) / g (w) - 1 ∣ < 1$ and use the convergent power series for $\log (1 + ξ)$ to obtain a local holomorphic logarithm of $g$ . Its real part is $u$ up to the constant $\log ∣ g (w) ∣$ ; [F6] and [F7] make that real part $C^{2}$ with zero Laplacian. This is local at every point, so $u$ is harmonic on a neighbourhood of the closed disc.

3.1F5step 1.2step 1.3step 2.1algebra

Apply [F5] to $u$ . On the boundary $u = \log ∣ f ∣$ , so its Poisson integral is exactly the boundary term in the statement. On the interior, solve the defining equation for $\log ∣ f ∣$ using step 1.3 and $\log ∣ B_{a} ∣ = - G_{R} (z, a)$ from step 1.2. Each zero contributes $- m_{b} G_{R} (z, b)$ and each pole contributes $+ ν_{p} G_{R} (z, p)$ , proving the formula on regular radii.

4.1F3F4step 3.1algebra∎

If $b$ is a zero or pole on $∣ z ∣ = R$ , locally $f (ζ) = (ζ - b)^{k} h (ζ)$ with integer $k$ and nonvanishing holomorphic $h$ (use [F3] for zeros and [F4] for poles). Therefore the boundary logarithm is a multiple of $\log ∣ r e^{i t} - b ∣$ plus a continuous term; these logarithms converge in angular $L^{1}$ as $r ↑ R$ . For each fixed interior $z$ , the Poisson kernels converge boundedly, and $G_{r} (z, b) \to 0$ for $∣ b ∣ = R$ . Passing to the limit in step 3.1 proves the stated boundary-radius convention.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6-sol)audited 2026-09-30Open item page →

Counting, chordal proximity and characteristic

Definition

Let $f$ be meromorphic on $C$ and not identically $\infty$ . Fix $a \in \hat{C}$ with $f \equiv̸ a$ . For $r > 0$ , let $n (r, a; f)$ be the sum of the local multiplicities of the $a$ -points in the closed disc $∣ z ∣ \leq r$ ; when $a = \infty$ , these are the poles with their pole orders. Define

$N (r, a; f) = n (0, a; f) \log r + \int_{0}^{r} \frac{n (t, a; f) - n (0, a; f)}{t} d t .$

For finite $w, a$ , put

$δ (w, a) = \frac{∣ w - a ∣}{\sqrt{1 + ∣ w ∣^{2}} \sqrt{1 + ∣ a ∣^{2}}}, δ (w, \infty) = δ (\infty, w) = \frac{1}{\sqrt{1 + ∣ w ∣^{2}}}, δ (\infty, \infty) = 0.$

At a pole or a point where $f = a$ , the expressions below are understood as logarithmic singularities in the angular Lebesgue integral. Define the proximity and characteristic by

$m (r, a; f) = \frac{1}{2 π} \int_{0}^{2 π} \log \frac{1}{δ (f (r e^{i t}), a)} d t, T (r, f) = m (r, \infty; f) + N (r, \infty; f) .$

For stereographic projection of the unit sphere, $δ$ is half the Euclidean chord length, so the chordal sphere has diameter one. This definition allows constant finite maps, but excludes their attained target from $n$ and $m$ .

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-30Open item page →

Well-definedness and radius conventions for Nevanlinna quantities

Statement

For every allowed pair $(f, a)$ in Counting, chordal proximity and characteristic, the count $n (r, a; f)$ is finite for each bounded disc, and $N (r, a; f)$ and $m (r, a; f)$ are finite and continuous for $r > 0$ , including at a divisor radius. For $a = \infty$ , $n (r, \infty; f)$ counts precisely the poles with their pole orders. For $r, r_{0} > 0$ , define $N_{r_{0}} (r, a; f) = \int_{r_{0}}^{r} n (t, a; f) d t / t$ . Then

$N_{r_{0}} (r, a; f) = N (r, a; f) - N (r_{0}, a; f),$

so replacing $N$ by $N_{r_{0}}$ changes the characteristic by the fixed constant $- N (r_{0}, \infty; f)$ . Proximity alone need not be monotone in $r$ .

Facts & Assumptions

Given: A meromorphic $f$ on $C$ and $a \in \hat{C}$ with $f \equiv̸ a$ .

[F1]

The definition counts local multiplicities on closed discs and treats infinity-points as poles (Counting, chordal proximity and characteristic).

[F2]

Chordal distance is given by the finite-target and infinity formulas (Counting, chordal proximity and characteristic).

[F3]

A nonzero holomorphic function has only isolated zeros (Zeros of a nonzero holomorphic function are isolated).

[F4]

Every pole is isolated (Poles of a meromorphic function form a closed discrete set and are at most countable).

[F5]

A finite-order zero factors locally as $(z - b)^{m} h (z)$ with $h (b) \neq 0$ (The order of a zero is the exponent in its local holomorphic factorization).

[F6]

At a pole, $1 / f$ extends holomorphically and vanishes (Characterizations of poles).

[F7]

A real measurable function is integrable when its absolute value has finite integral (Integrable real and complex functions, and their integrals).

Proof

technique · write the integrated counts as finite divisor sums and remove each angular logarithmic singularity before varying the radius

1.1F1F4given

For $a = \infty$ , [F1] identifies the counted points as poles; [F4] makes them isolated, so compactness gives finitely many poles in each bounded closed disc, each of finite order.

1.2F2F3F5given

At a finite $a$ -point $b$ of order $m_{b}$ , [F2], [F3] and [F5] give $f - a = (z - b)^{m_{b}} h$ with $h (b) \neq 0$ and $ψ_{a} (z) : = \log (1 / δ (f (z), a)) = - m_{b} \log ∣ z - b ∣ + q (z)$ for a continuous $q$ near $b$ .

1.3F2F6

At any pole, [F6] makes $w = 1 / f$ extend holomorphically with $w (b) = 0$ ; for finite $a$ , [F2] rewrites the chordal distance as $δ (f, a) = ∣ 1 - a w ∣ / (\sqrt{1 + ∣ w ∣^{2}} \sqrt{1 + ∣ a ∣^{2}})$ , which has a positive limit, so $ψ_{a}$ extends continuously over the pole.

1.4algebra

For $b \neq 0$ and $r < ∣ b ∣$ , factor $r e^{i t} - b = - b (1 - (r / b) e^{i t})$ ; for $r > ∣ b ∣$ , factor it as $r e^{i t} (1 - (b / r) e^{- i t})$ . The uniformly convergent series $\log (1 - ζ) = - \sum_{n \geq 1} ζ^{n} / n$ for $∣ ζ ∣ < 1$ has zero mean term by term, so the mean of $\log ∣ r e^{i t} - b ∣$ is $\log ∣ b ∣$ or $\log r$ , respectively; for $b = 0$ it is $\log r$ .

2.1F2F5F6step 1.3

For $a = \infty$ at a pole $b$ of order $m_{b}$ , [F6] gives the reciprocal zero order $m_{b}$ from the leading Laurent term, and [F5] applied to the zero $w = 1 / f$ from step 1.3 gives $f = (z - b)^{- m_{b}} h$ with $h$ holomorphic and nonzero; hence $ψ_{\infty} + m_{b} \log ∣ z - b ∣ = \frac{1}{2} \log (∣ z - b ∣^{2 m_{b}} + ∣ h ∣^{2})$ extends continuously.

2.2F3F6step 1.1given

For finite $a$ , [F3] isolates the zeros of $f - a$ away from poles, and [F6] prevents such zeros from accumulating at a pole. The finitely many poles from step 1.1 have neighborhoods free of $a$ -points; the remaining compact set contains only finitely many isolated zeros. Thus every bounded-disc finite-target count is finite.

2.3F7step 1.4algebra

If $r = ∣ b ∣ > 0$ , rotate to $b = ∣ b ∣$ . Then the mean is $\log ∣ b ∣ + (2 π)^{- 1} \int_{0}^{2 π} \log (2 ∣ \sin (t / 2) ∣) d t = \log ∣ b ∣$ : with $J = \int_{0}^{π / 2} \log (\sin x) d x$ , symmetry and $\sin (2 x) = 2 \sin x \cos x$ give $2 J = - (π / 2) \log 2 + J$ , hence $J = - (π / 2) \log 2$ and the integral is zero. The endpoint singularities have finite absolute integral since $\int_{0}^{ϵ} ∣ \log x ∣ d x < \infty$ , so [F7] applies.

3.1F1step 1.1step 2.2algebra

Integrating the step function in [F1] gives $N (r, a; f) = n (0, a; f) \log r + \sum_{0 < ∣ b ∣ \leq r} m_{b} \log (r / ∣ b ∣)$ , a finite sum by steps 1.1 and 2.2; each term is zero when first included at $r = ∣ b ∣$ , so $N$ is continuous.

3.2step 1.1step 1.2step 1.3step 2.1step 2.2

Around any fixed $r_{0} > 0$ , take a compact annulus containing all nearby circles. Steps 1.1 and 2.2 give finitely many relevant divisor points there; by steps 1.2, 1.3 and 2.1, adding $m_{b} \log ∣ z - b ∣$ at each singular divisor leaves a continuous function on the annulus, whose circular mean varies continuously with $r$ .

4.1F1step 3.1algebra

Splitting the defining integral at $r_{0}$ gives $N (r, a; f) - N (r_{0}, a; f) = n (0, a; f) \log (r / r_{0}) + \int_{r_{0}}^{r} (n (t, a; f) - n (0, a; f)) d t / t = \int_{r_{0}}^{r} n (t, a; f) d t / t$ , also for $r < r_{0}$ as an oriented integral.

4.2step 1.4step 2.3step 3.2algebra

By steps 1.4 and 2.3, each removed logarithm has continuous mean $\log \max (r, ∣ b ∣)$ , including at $r = ∣ b ∣$ . Combining those means with the continuous remainder from step 3.2 proves $m (r, a; f)$ finite and continuous at every radius. Only finite divisor lists are used, so no AC is needed.

5.1F2algebra∎

For $f (z) = z + 1 / z$ and $a = \infty$ , the reverse triangle inequality gives $∣ f (r e^{i t}) ∣ \geq ∣ r - r^{- 1} ∣$ . Thus [F2] gives $m (r, \infty; f) \geq \frac{1}{2} \log (1 + (r - r^{- 1})^{2})$ . At $r = 1$ , $∣ f (e^{i t}) ∣ = ∣ 2 \cos t ∣ \leq 2$ , so $m (1, \infty; f) \leq \frac{1}{2} \log 5$ . At both $r = 1 / 4$ and $r = 4$ , the lower bound is $\frac{1}{2} \log (241 / 16) > \frac{1}{2} \log 5$ . Consequently $m (1 / 4, \infty; f) > m (1, \infty; f)$ and $m (4, \infty; f) > m (1, \infty; f)$ , ruling out both nondecreasing and nonincreasing behaviour. Proximity alone need not be monotone.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-30Open item page →

Meromorphic Jensen identity with a zero or pole at the centre

Statement

Let $a \in C$ and let $f$ be nonconstant meromorphic. Near $0$ , write $f (z) - a = c_{a} z^{k_{a}} + higher Laurent terms$ with $c_{a} \neq 0$ and $k_{a} \in Z$ . Then for every $r > 0$ ,

M_{r} \log ∣ f - a ∣ = \log ∣ c_{a} ∣ + N (r, a; f) - N (r, \infty; f),

where $M_{r}$ is the angular mean on $∣ z ∣ = r$ . If that circle contains a zero or pole of $f - a$ , its mean is interpreted by its continuous radial limit.

Facts & Assumptions

Given: A nonconstant meromorphic $f$ on $C$ and a finite target $a$ .

[F1]

Poisson–Jensen expresses the logarithm as the boundary Poisson mean minus zero Green terms plus pole Green terms (Poisson–Jensen formula for a meromorphic function on a disc).

[F2]

The integrated count is $N (r, a; f) = n (0, a; f) \log r + \int_{0}^{r} (n (t, a; f) - n (0, a; f)) d t / t$ (Counting, chordal proximity and characteristic).

[F3]

A function holomorphic on a punctured annulus has a locally uniformly convergent Laurent expansion there (Laurent expansion on an annulus).

[F4]

The divisor counts are finite on bounded discs, and $N$ and chordal proximities are finite and continuous at every positive radius (Well-definedness and radius conventions for Nevanlinna quantities).

[F5]

Chordal distance and its logarithmic proximity are given by the normalized formulas in the definition (Counting, chordal proximity and characteristic).

[F6]

An infinite-order zero occurs exactly when the function vanishes on a neighborhood; a finite-order zero has a local factorization (The order of a zero is the exponent in its local holomorphic factorization).

[F7]

A pole has a finite Laurent principal part, and its order is the largest negative exponent (Characterizations of poles).

[F8]

The pole set is closed and discrete (Poles of a meromorphic function form a closed discrete set and are at most countable).

[F9]

Holomorphic functions on a complex domain that agree on a set with an accumulation point agree everywhere (Identity theorem for holomorphic functions).

[F10]

A meromorphic function is holomorphic away from its pole set (Meromorphic functions on a plane domain).

Proof

technique · apply Poisson–Jensen to $f-a$, isolate the central Green term, and identify the remaining divisor sums with $N(r,a)-N(r,\infty)$

1.1F1given

Fix a radius $r$ with no zero or pole of $f - a$ on its boundary, and write $m_{0} = n (0, a; f)$ and $ν_{0} = n (0, \infty; f)$ . Applying [F1] to $f - a$ gives its boundary Poisson mean, a negative sum over $a$ -points, and a positive sum over poles; the central Green factor is $G_{r} (z, 0) = \log (r / ∣ z ∣)$ .

1.2F8F10given

Let $P$ be the pole set and $Ω = C ∖ P$ . By [F8] and [F10], $Ω$ is open and $f$ is holomorphic there; it is nonempty because a discrete pole set cannot equal $C$ . For any two points of $Ω$ , take a bounded closed disc containing a polygonal path between them in its interior. This disc meets $P$ in finitely many points because $P$ is closed and discrete. Choose small disjoint discs around those finitely many poles, avoiding the path endpoints and containing no other poles; replacing portions of the polygonal path through these discs by arcs in the punctured discs gives a path in $Ω$ . Thus $Ω$ is connected.

1.3F3F7given

If $f$ has a pole at $0$ of order $ν_{0}$ , [F3] gives a Laurent expansion on a punctured disc and [F7] makes its first nonzero exponent $- ν_{0}$ ; subtracting finite $a$ does not change that leading exponent.

1.4givenalgebra

If $f (0)$ is finite and not equal to $a$ , then $f - a$ is nonzero at $0$ , so its leading exponent is $k_{a} = 0 = m_{0} - ν_{0}$ .

2.1F6F7F9step 1.2given

If $f (0) = a$ and the zero of $f - a$ at $0$ had infinite order, [F6] would make $f - a$ vanish near $0$ . By [F9] on the connected domain from step 1.2, it would then vanish on all of $Ω$ ; if $P$ is empty this makes $f$ constant, while if $P$ is nonempty it contradicts [F7] at each pole. Thus the order is finite, and [F6] gives $f - a = z^{m_{0}} h$ with $h (0) \neq 0$ , so its leading exponent is $k_{a} = m_{0}$ .

3.1step 2.1step 1.3step 1.4algebra

The three cases in steps 1.3, 1.4, and 2.1 show that $f (z) - a = c_{a} z^{k_{a}} (1 + o (1))$ and $k_{a} = m_{0} - ν_{0}$ ; hence $\log ∣ f (z) - a ∣ = \log ∣ c_{a} ∣ + k_{a} \log ∣ z ∣ + o (1)$ .

4.1F1step 1.1step 3.1algebra

Let $z \to 0$ in step 1.1 through nondivisor points. The boundary Poisson mean tends to $M_{r} \log ∣ f - a ∣$ ; every noncentral Green term tends to $\log (r / ∣ b ∣)$ or $\log (r / ∣ p ∣)$ ; and the central contribution is $- k_{a} (\log r - \log ∣ z ∣)$ . Comparing with step 3.1 and cancelling $k_{a} \log ∣ z ∣$ yields $M_{r} \log ∣ f - a ∣ = \log ∣ c_{a} ∣ + k_{a} \log r + \sum_{0 < ∣ b ∣ < r} m_{b} \log (r / ∣ b ∣) - \sum_{0 < ∣ p ∣ < r} ν_{p} \log (r / ∣ p ∣)$ .

4.2F2F4step 3.1algebra

By [F2] and the finite divisor lists in [F4], integrating each counting step gives $N (r, a; f) = m_{0} \log r + \sum_{0 < ∣ b ∣ < r} m_{b} \log (r / ∣ b ∣)$ and $N (r, \infty; f) = ν_{0} \log r + \sum_{0 < ∣ p ∣ < r} ν_{p} \log (r / ∣ p ∣)$ . Since $k_{a} = m_{0} - ν_{0}$ , step 3.1 is exactly $\log ∣ c_{a} ∣ + N (r, a; f) - N (r, \infty; f)$ .

5.1F4F5step 4.2∎

For any radius meeting a divisor, the pointwise chordal identity gives $M_{r} \log ∣ f - a ∣ = m (r, \infty; f) + \frac{1}{2} \log (1 + ∣ a ∣^{2}) - m (r, a; f)$ . By [F4]–[F5], this mean is finite and continuous in $r$ ; the two counting functions are continuous as well. Taking regular radii to the divisor radius in step 4.2 proves the same identity there by continuous radial limit.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30Open item page →

Ahlfors–Shimizu area form of the characteristic

Statement

Let $f$ be a nonconstant meromorphic function on $C$ . At regular points set $f^{#} (z) = \frac{∣ f^{'} (z) ∣}{1 + ∣ f (z) ∣^{2}},$ and extend $f^{#}$ continuously at poles. Define $A (r, f) = \frac{1}{π} \int_{∣ z ∣ \leq r} (f^{#} (z))^{2} d A (z), T_{A S} (r, f) = \int_{0}^{r} A (t, f) \frac{d t}{t} .$ Write $M_{r} h = (2 π)^{- 1} \int_{0}^{2 π} h (r e^{i t}) d t$ for a circular mean whenever it exists. If $f (0)$ is finite, set $C_{\infty} (f) = \frac{1}{2} \log (1 + ∣ f (0) ∣^{2})$ . If $0$ is a pole and $f (z) = c z^{- m} + higher Laurent terms, c \neq 0,$ set $C_{\infty} (f) = \log ∣ c ∣$ . Then, for every $r > 0$ , $T (r, f) = T_{A S} (r, f) + C_{\infty} (f) .$ In particular, $T_{A S}$ is finite and nondecreasing, and is convex as a function of $\log r$ .

Facts & Assumptions

Given: A nonconstant meromorphic $f$ on $C$ , the counting, proximity, and characteristic conventions in Counting, chordal proximity and characteristic, and plane area measure $d A$ .

[F1]

$N (r, a; f) = n (0, a; f) \log r + \int_{0}^{r} (n (t, a; f) - n (0, a; f)) d t / t$ (Counting, chordal proximity and characteristic).

[F2]

$T (r, f) = m (r, \infty; f) + N (r, \infty; f)$ , where $m (r, \infty; f)$ is the mean of $\frac{1}{2} \log (1 + ∣ f ∣^{2})$ (Counting, chordal proximity and characteristic).

[F3]

The Laurent principal part at a pole of order $m$ begins with $c_{- m} (z - p)^{- m}$ , where $c_{- m} \neq 0$ (Characterizations of poles).

[F4]

A finite-order zero factors locally as $(z - p)^{m} q (z)$ with $q (p) \neq 0$ (The order of a zero is the exponent in its local holomorphic factorization).

[F5]

A holomorphic function satisfies the Cauchy–Riemann equations (Complex differentiability is equivalent to real total differentiability together with a complex-linear derivative, with $\partial_{\overset{ˉ}{z}} f = 0$ , or with the Cauchy–Riemann equations).

[F6]

A holomorphic function is of class $C^{k}$ for every natural $k$ , hence smooth (Holomorphic functions are real analytic and smooth in their two real coordinates).

[F7]

Pole counts on bounded discs are finite, and $N (r, \infty; f)$ and $m (r, \infty; f)$ are finite and continuous for $r > 0$ (Well-definedness and radius conventions for Nevanlinna quantities).

[F8]

A measurable function whose absolute value has finite integral is integrable (Integrable real and complex functions, and their integrals).

Proof

technique · correct the logarithmic singularities of the spherical potential at each pole, apply the radial Laplacian identity to its circular mean, and identify the finite pole corrections with the integrated count

1.1F3F4algebra

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

1.2F5F6algebra

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

1.3F8algebra

For any $p \in C$ and $r > 0$ , $M_{r} \log ∣ r e^{i t} - p ∣ = \log \max {r, ∣ p ∣}$ . If $r \neq ∣ p ∣$ , factor out the larger of $r$ and $∣ p ∣$ and average the uniformly convergent series $\log (1 - ζ) = - \sum_{n \geq 1} ζ^{n} / n$ . If $r = ∣ p ∣ > 0$ , rotate to $p = r$ ; then $∣ r e^{i t} - p ∣ = 2 r ∣ \sin (t / 2) ∣$ . The logarithm is integrable since $\sin (t / 2)$ is comparable to the distance from an endpoint near $0$ and $2 π$ . With $J = \int_{0}^{π / 2} \log (\sin x) d x$ , symmetry and $\sin (2 x) = 2 \sin x \cos x$ give $2 J = - (π / 2) \log 2 + J$ , hence $J = - (π / 2) \log 2$ and the angular mean of $\log (2 ∣ \sin (t / 2) ∣)$ is zero. The case $p = 0$ is immediate.

1.4F1F7algebra

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

1.5F3F6F7

Put $u_{f} = \frac{1}{2} \log (1 + ∣ f ∣^{2})$ away from poles and define $v (z) = u_{f} (z) + \sum_{∣ p ∣ < r} m_{p} \log ∣ z - p ∣$ . 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 (∣ z - p ∣^{2 m_{p}} + ∣ h_{p} (z) ∣^{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.

2.1F6F8step 1.1algebra

Away from poles $f^{#}$ is continuous by holomorphic smoothness; at a pole, step 1.1 gives $∣ f^{'} ∣ / (1 + ∣ f ∣^{2}) = ∣ g^{'} ∣ / (1 + ∣ g ∣^{2})$ off the pole, which extends continuously there by [F6]. Hence $(f^{#})^{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.

2.2F2step 1.3step 1.4step 1.5algebra

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

3.1step 1.2step 1.5step 2.1algebra

Away from the listed poles, every $\log ∣ z - p ∣$ is harmonic and step 1.2 gives $Δ v = 2 (f^{#})^{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.

4.1step 3.1algebra

Polar coordinates and step 3.1 give $(t V^{'} (t))^{'} = t M_{t} (Δ v) = 2 t M_{t} ((f^{#})^{2}) = A^{'} (t)$ , since $A^{'} (t) = π^{- 1} t \int_{0}^{2 π} (f^{#} (t e^{i θ}))^{2} d θ$ . The angular second-derivative term in the polar Laplacian integrates to zero.

5.1step 4.1step 2.2step 2.1algebra

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

6.1F2F7step 2.1step 5.1algebra∎

The area function $A$ is continuous and nondecreasing because $(f^{#})^{2}$ is continuous and nonnegative; step 2.1 gives $A (t) = O (t^{2})$ and a finite integral $T_{A S}$ . The derivative of $x \mapsto T_{A S} (e^{x})$ is $A (e^{x})$ , which is nondecreasing, so this function is convex. Finally [F7] makes $T = m (r, \infty; f) + N (r, \infty; f)$ continuous across pole radii; $T_{A 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.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30Open item page →

Nevanlinna’s First Main Theorem with exact centre constant

Statement

Write $M_{r} h = (2 π)^{- 1} \int_{0}^{2 π} h (r e^{i t}) d t$ for a circular mean whenever it exists.

Let $f$ be a nonconstant meromorphic function on $C$ and let $a \in \hat{C}$ . For every $r > 0$ , $m (r, a; f) + N (r, a; f) = T (r, f) + C (f, a) .$ For $a = \infty$ , set $C (f, \infty) = 0$ . For finite $a$ , write the first nonzero Laurent term at the centre as $f (z) - a = c_{a} z^{k_{a}} + higher Laurent terms, c_{a} \neq 0,$ and set $C (f, a) = \frac{1}{2} \log (1 + ∣ a ∣^{2}) - \log ∣ c_{a} ∣$ . In particular, the difference $m (r, a; f) + N (r, a; f) - T (r, f)$ is $O_{f, a} (1)$ as $r \to \infty$ .

Facts & Assumptions

Given: A nonconstant meromorphic $f$ on $C$ and a target $a \in \hat{C}$ .

[F1]

The normalized chordal distance is $δ (w, a) = ∣ w - a ∣ / (\sqrt{1 + ∣ w ∣^{2}} \sqrt{1 + ∣ a ∣^{2}})$ for finite $w, a$ , and $δ (w, \infty) = 1 / \sqrt{1 + ∣ w ∣^{2}}$ (Counting, chordal proximity and characteristic).

[F2]

$m (r, a; f)$ is the circular mean of $\log (1 / δ (f, a))$ , and $T (r, f) = m (r, \infty; f) + N (r, \infty; f)$ (Counting, chordal proximity and characteristic).

[F3]

For finite $a$ , the centre-divisor Jensen identity is $M_{r} \log ∣ f - a ∣ = \log ∣ c_{a} ∣ + N (r, a; f) - N (r, \infty; f)$ , with divisor-circle means interpreted by continuous radial limits (Meromorphic Jensen identity with a zero or pole at the centre).

[F4]

The divisor counts are finite on bounded discs and $N (r, a; f)$ and $m (r, a; f)$ are finite and continuous for every $r > 0$ , including divisor radii (Well-definedness and radius conventions for Nevanlinna quantities).

Proof

technique · use the pointwise chordal identity for finite targets, average it on a regular circle, and substitute the centre-divisor Jensen identity; handle infinity directly from the definition

1.1F1given

Fix finite $a$ and a regular radius $r$ whose circle contains no pole and no $a$ -point. From [F1], at every point of that circle, $\log (1 / δ (f, a)) = \frac{1}{2} \log (1 + ∣ f ∣^{2}) + \frac{1}{2} \log (1 + ∣ a ∣^{2}) - \log ∣ f - a ∣$ .

2.1F2step 1.1

Averaging the identity in step 1.1 and using [F2] gives $m (r, a; f) - m (r, \infty; f) = \frac{1}{2} \log (1 + ∣ a ∣^{2}) - M_{r} \log ∣ f - a ∣$ .

3.1F2F3step 2.1algebra

Substitute [F3] into step 2.1 to obtain $m (r, a; f) - m (r, \infty; f) = \frac{1}{2} \log (1 + ∣ a ∣^{2}) - \log ∣ c_{a} ∣ - N (r, a; f) + N (r, \infty; f)$ . Rearranging and using [F2] yields the claimed formula for finite $a$ at each regular radius.

4.1F2F4step 3.1

Regular radii are dense because [F4] makes the divisor sets finite on bounded discs. The finite-target quantities in the formula are continuous by [F4], so the equality from step 3.1 on that dense set extends to every $r > 0$ . For $a = \infty$ , $C (f, \infty) = 0$ and the asserted identity is exactly the defining equality in [F2].

5.1step 4.1algebra∎

For each fixed $f, a$ , the constant $C (f, a)$ in step 4.1 is finite and independent of $r$ ; therefore the difference in the statement is bounded as $r \to \infty$ .

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30Open item page →

Elementary characteristic laws and fixed rational composition

Statement

For meromorphic $f, g$ on $C$ , as $r \to \infty$ , $T (r, f g) \leq T (r, f) + T (r, g) + O (1), T (r, f + g) \leq T (r, f) + T (r, g) + O (1) .$ If $f$ is not identically zero, then $T (r, 1 / f) = T (r, f) + O_{f} (1) .$ If $R = P / Q$ is a fixed rational map written with coprime polynomials and $d = \max (\deg P, \deg Q)$ , then for nonconstant meromorphic $f$ and $d \geq 1$ , $T (r, R (f)) = d T (r, f) + O_{R, f} (1) .$ A degree-zero rational map is constant and has bounded characteristic after composition with $f$ .

Facts & Assumptions

Given: Meromorphic functions on $C$ ; counting, proximity, and characteristic are normalized as in Counting, chordal proximity and characteristic.

[F1]

The normalized chordal distance and the proximity and characteristic are defined by the formulas in Counting, chordal proximity and characteristic.

[F2]

$N (r, a; h) = n (0, a; h) \log r + \int_{0}^{r} (n (t, a; h) - n (0, a; h)) d t / t$ (Counting, chordal proximity and characteristic).

[F3]

For nonconstant meromorphic $h$ and any finite target $a$ , $m (r, a; h) + N (r, a; h) = T (r, h) + C (h, a)$ for every $r > 0$ (Nevanlinna’s First Main Theorem with exact centre constant).

[F4]

Every nonconstant complex polynomial has a complex root (Fundamental theorem of algebra by Liouville's theorem); in particular the normalized denominator $Q$ of degree $d \geq 1$ in step 4.1 has a nonempty finite zero set.

Proof

technique · Compare the chordal characteristic with $T_0=m_0+N_\infty$, where $m_0(r,h)$ is the circular mean of $\log^+|h|$. Prove the algebraic laws for $T_0$, then transfer them across the uniformly bounded normalization difference

1.1F1algebra

Define $T_{0} (r, h) = m_{0} (r, h) + N (r, \infty; h)$ . For every finite $w$ , $\log^{+} ∣ w ∣ \leq \frac{1}{2} \log (1 + ∣ w ∣^{2}) \leq \log^{+} ∣ w ∣ + \frac{1}{2} \log 2$ . By [F1], $m (r, \infty; h)$ is the mean of $\frac{1}{2} \log (1 + ∣ h ∣^{2})$ , so averaging gives $0 \leq T (r, h) - T_{0} (r, h) \leq \frac{1}{2} \log 2$ for every meromorphic $h$ and $r > 0$ .

2.1F1F2step 1.1algebra

For complex $x, y$ , $\log^{+} ∣ x y ∣ \leq \log^{+} ∣ x ∣ + \log^{+} ∣ y ∣$ and $\log^{+} ∣ x + y ∣ \leq \log^{+} ∣ x ∣ + \log^{+} ∣ y ∣ + \log 2$ . At each point the pole order of either $f g$ or $f + g$ is at most the sum of the pole orders of $f$ and $g$ ; this includes cancellation and the identically zero sum, whose pole order is zero. For $r \geq 1$ , every pole-count weight in [F2] is nonnegative, including the centre weight $\log r$ . Integrating the logarithmic bounds and the divisor bounds gives both upper laws for $T_{0}$ ; step 1.1 transfers them to $T$ .

2.2F1F3step 1.1algebra

Suppose first that $f$ is nonconstant and not identically zero. Away from its zeros and poles, [F1] gives $\log (1 / δ (f, 0)) = \frac{1}{2} \log (1 + ∣ f ∣^{2}) - \log ∣ f ∣ = \frac{1}{2} \log (1 + ∣ 1 / f ∣^{2})$ . The poles of $1 / f$ are precisely the zeros of $f$ with the same multiplicities. Therefore $T (r, 1 / f) = m (r, 0; f) + N (r, 0; f) = T (r, f) + C (f, 0)$ by [F1] and [F3]. If $f$ is a nonzero constant, both characteristics are constant in $r$ . This proves the reciprocal law for $T$ ; step 1.1 gives the same law for $T_{0}$ with a bounded error.

2.3F1F2step 1.1algebra

Let $P (w) = a_{p} w^{p} + \dots + a_{0}$ with $p \geq 1$ and $a_{p} \neq 0$ . For sufficiently large $∣ w ∣$ , the leading term bounds $∣ P (w) ∣$ above and below by positive constant multiples of $∣ w ∣^{p}$ ; on the remaining compact $w$ -disc both $\log^{+} ∣ P (w) ∣$ and $p \log^{+} ∣ w ∣$ are bounded. Hence $\log^{+} ∣ P (w) ∣ = p \log^{+} ∣ w ∣ + O_{P} (1)$ uniformly in $w$ . Averaging gives $m_{0} (r, P (f)) = p m_{0} (r, f) + O_{P} (1)$ . At every pole of $f$ of order $λ$ , the leading term of $P$ makes $P (f)$ have pole order exactly $p λ$ , and $P (f)$ has no other poles. Thus [F2] gives $N (r, \infty; P (f)) = p N (r, \infty; f)$ , and step 1.1 yields $T (r, P (f)) = p T (r, f) + O_{P} (1)$ . If $P$ is constant, $P (f)$ is constant and has bounded characteristic.

3.1step 2.2algebra

Let $R = P / Q$ be nonconstant of degree $d \geq 1$ , with $P, Q$ coprime. The composition $R (f)$ is nonconstant: otherwise the connected image of the nonconstant meromorphic map $f : C \to \hat{C}$ would lie in a finite fiber of $R$ . By step 2.2, replacing $R$ by $1 / R$ changes the characteristic of its composition by only $O_{R, f} (1);$ this handles $\deg P = d > \deg Q$ . If $\deg P = \deg Q = d$ , subtract $c = R (\infty)$ : translating a meromorphic function by a constant changes $m_{0}$ by a bounded amount and leaves its pole orders unchanged, while $P - c Q$ has degree less than $d$ . Thus it suffices to prove the result when $\deg Q = d$ and $\deg P < d$ .

4.1F4step 3.1algebra

In this normalized case, the nonempty finite zero set of $Q$ is disjoint from that of $P$ . If $P$ has zeros, let $ϵ$ be one third of the minimum distance between the two finite zero sets; if $P$ has none, take any $ϵ > 0$ . Let $Γ$ be the union of the open $ϵ$ -discs around the zeros of $Q$ and put $Ω = \hat{C} ∖ Γ$ . Its closure avoids the zeros of $P$ . On $\overline{Γ}$ , $∣ P ∣$ has a positive lower bound and a finite upper bound, so $∣ R ∣ = ∣ P / Q ∣$ is bounded above and below by positive constant multiples of $∣ 1 / Q ∣$ . On $Ω$ , both $R$ and $1 / Q$ are bounded, including at infinity because $\deg P < \deg Q$ . Splitting each circle into the sets where $f$ lies in $Γ$ and $Ω$ , these comparisons and the boundedness of $\log^{+}$ on bounded values give $m_{0} (r, R (f)) = m_{0} (r, 1 / Q (f)) + O_{R} (1)$ . Values at isolated poles are interpreted through their integrable logarithmic singularities.

5.1F2step 3.1step 4.1algebra

The pole divisors of $R (f)$ and $1 / Q (f)$ agree. At a point where $f$ is finite, a pole occurs exactly when $Q (f) = 0$ ; coprimality makes $P (f) \neq 0$ there, so its order is the zero order of $Q (f)$ . At a pole of $f$ , the inequalities $\deg P < \deg Q = d$ imply both $R (f) \to 0$ and $1 / Q (f) \to 0$ , so neither has a pole. Hence [F2] gives $N (r, \infty; R (f)) = N (r, \infty; 1 / Q (f))$ . Combining this with step 4.1 yields $T_{0} (r, R (f)) = T_{0} (r, 1 / Q (f)) + O_{R} (1)$ .

6.1step 1.1step 2.2step 2.3step 3.1step 5.1algebra

Since $f$ is nonconstant, $Q (f)$ is not identically zero: otherwise the connected image of $f$ would lie in the finite zero set of $Q$ , forcing $f$ to be constant. Applying the reciprocal law of step 2.2 and the polynomial law of step 2.3 gives $T_{0} (r, 1 / Q (f)) = T_{0} (r, Q (f)) + O_{Q, f} (1) = d T_{0} (r, f) + O_{Q, f} (1)$ . Step 1.1 transfers this estimate to $T$ , while steps 3.1 and 5.1 reduce the original composition to this normalized estimate.

7.1F1algebra∎

If $d = 0$ , $R$ is a constant $c$ and $R (f)$ has no poles; by [F1], $T (r, R (f)) = \frac{1}{2} \log (1 + ∣ c ∣^{2})$ for every $r$ , which is bounded.

DefinitionDefinition: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-30Open item page →

Order and lower order from the Nevanlinna characteristic

Statement

Let $f$ be nonconstant meromorphic on $C$ . Its characteristic is nondecreasing, and $T (r, f) > 1$ for all sufficiently large $r$ . Define its order and lower order by $ρ (f) = {lim sup}_{r \to \infty} \frac{\log T (r, f)}{\log r}, λ (f) = {lim inf}_{r \to \infty} \frac{\log T (r, f)}{\log r},$ using only sufficiently large $r > 1$ with $T (r, f) > 1$ . Both values lie in $[0, \infty]$ ; $f$ has finite order when $ρ (f) < \infty$ . For every constant finite map, set $ρ (f) = λ (f) = 0$ by convention. For entire functions, the next proposition compares this order with the classical maximum-modulus order; meromorphic growth is measured by $T$ , which remains finite in the presence of poles.

Facts & Assumptions

Given: The characteristic, integrated counts, and normalized chordal proximity for a meromorphic function on $C$ .

[F1]

The integrated count is $N (r, a; f) = n (0, a; f) \log r + \int_{0}^{r} (n (t, a; f) - n (0, a; f)) d t / t$ (Counting, chordal proximity and characteristic).

[F2]

The characteristic is $T (r, f) = m (r, \infty; f) + N (r, \infty; f)$ (Counting, chordal proximity and characteristic).

[F3]

The normalized chordal sphere has diameter one, so $\log (1 / δ (f, a)) \geq 0$ and every proximity is nonnegative (Counting, chordal proximity and characteristic).

[F4]

The First Main Theorem gives $m (r, a; f) + N (r, a; f) = T (r, f) + C (f, a)$ with a fixed finite centre constant (Nevanlinna’s First Main Theorem with exact centre constant).

[F5]

The Ahlfors–Shimizu identity is $T (r, f) = T_{A S} (r, f) + C_{\infty} (f)$ , and $T_{A S}$ is finite and nondecreasing (Ahlfors–Shimizu area form of the characteristic).

Proof

technique · use a central divisor to force logarithmic growth of $T$, then use the area identity to establish monotonicity of the characteristic

1.1F1algebra

For any target $a$ , $n (t, a; f) \geq n (0, a; f)$ , so [F1] gives $N (r, a; f) \geq n (0, a; f) \log r$ for $r > 1$ .

2.1F2F3F4step 1.1algebra

If $f (0)$ is finite, take $a = f (0)$ ; then $n (0, a; f) \geq 1$ and [F4], [F3], and step 1.1 give $T (r, f) \geq \log r - C (f, a)$ . If $0$ is a pole, then $n (0, \infty; f) \geq 1$ and [F2], [F3], and step 1.1 give $T (r, f) \geq \log r$ . Thus $T (r, f) \to \infty$ and is greater than $1$ for all sufficiently large $r$ .

3.1F5step 2.1algebra∎

By [F5], $T$ is nondecreasing; by step 2.1 the logarithmic ratio in the statement is defined and nonnegative for all sufficiently large $r$ . Its limsup and liminf therefore lie in $[0, \infty]$ .

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-30Open item page →

Entire-function order agrees with maximum-modulus order

Statement

For an entire function $f$ , define $M (r, f) = \max_{∣ z ∣ = r} ∣ f (z) ∣, m_{0} (r, f) = \frac{1}{2 π} \int_{0}^{2 π} \log^{+} ∣ f (r e^{i t}) ∣ d t, T_{0} (r, f) = m_{0} (r, f) + N (r, \infty; f) = m_{0} (r, f) .$ For every nonconstant entire $f$ and $0 < r < R$ , $T_{0} (r, f) \leq \log^{+} M (r, f) \leq \frac{R + r}{R - r} T_{0} (R, f) .$ Its Nevanlinna order $ρ (f)$ and lower order $λ (f)$ from Order and lower order from the Nevanlinna characteristic agree with ${lim sup}_{r \to \infty} \frac{\log (\log^{+} M (r, f))}{\log r}, {lim inf}_{r \to \infty} \frac{\log (\log^{+} M (r, f))}{\log r},$ respectively; these limits are taken for sufficiently large $r$ with $\log^{+} M (r, f) > 1$ .

Facts & Assumptions

Given: A nonconstant entire $f$ on $C$ and the chordal characteristic and order conventions of Counting, chordal proximity and characteristic and Order and lower order from the Nevanlinna characteristic.

[F1]

$T (r, h) = m (r, \infty; h) + N (r, \infty; h)$ , and $m (r, \infty; h)$ is the circular mean of $\frac{1}{2} \log (1 + ∣ h ∣^{2})$ (Counting, chordal proximity and characteristic).

[F2]

The Poisson–Jensen identity on $∣ z ∣ \leq R$ subtracts the zero Green terms and adds the pole Green terms; at a boundary divisor the identity is interpreted by the limit through regular radii (Poisson–Jensen formula for a meromorphic function on a disc).

[F3]

For nonconstant meromorphic $f$ , $T (r, f) > 1$ for all sufficiently large $r$ (Order and lower order from the Nevanlinna characteristic).

[F4]

An entire function equals its Taylor series throughout its largest centred disc; for $f$ entire this gives $f (z) = \sum_{n \geq 0} a_{n} z^{n}$ for every $z \in C$ (A holomorphic function equals its Taylor series throughout the largest centred disc in its domain).

[F5]

If $M$ bounds $∣ f ∣$ on $∣ z ∣ = r$ , then each Taylor coefficient $a_{n}$ satisfies $∣ a_{n} ∣ \leq M / r^{n}$ (Cauchy's inequalities bound the Taylor coefficients by the circle supremum).

[F6]

Every nonempty subset of $N$ has a least element (The well-ordering principle), used to select the first nonzero positive Taylor index.

Proof

technique · Compare the chordal characteristic with $T_0=m_0+N_\infty$, bound the maximum modulus above by Poisson–Jensen, and squeeze both logarithmic limits after setting $R=2r$

1.1F1algebra

For every finite $w$ , $\log^{+} ∣ w ∣ \leq \frac{1}{2} \log (1 + ∣ w ∣^{2}) \leq \log^{+} ∣ w ∣ + \frac{1}{2} \log 2$ . Since an entire function has no poles, [F1] gives $T_{0} (r, f) = m_{0} (r, f)$ and $0 \leq T (r, f) - T_{0} (r, f) \leq c$ , where $c = \frac{1}{2} \log 2 < 1$ .

1.2F4F5F6givenalgebra

By [F4], write $f (z) = \sum_{n \geq 0} a_{n} z^{n}$ on $C$ . Since $f$ is nonconstant, let $k \geq 1$ be the least index with $a_{k} \neq 0$ . Applying [F5] on the radius- $r$ circle, with any larger holomorphy radius such as $2 r$ , gives $∣ a_{k} ∣ \leq M (r, f) / r^{k}$ . Thus $M (r, f) \geq ∣ a_{k} ∣ r^{k}$ and $\log^{+} M (r, f) \to \infty$ ; in particular $\log^{+} M (r, f) > 1$ for all sufficiently large $r$ .

2.1F1step 1.1algebra

On $∣ z ∣ = r$ , $\log^{+} ∣ f (z) ∣ \leq \log^{+} M (r, f)$ . Averaging gives $T_{0} (r, f) = m_{0} (r, f) \leq \log^{+} M (r, f)$ .

2.2F1F2step 1.1algebra

Fix $0 < r < R$ . For $∣ z ∣ = r$ with $f (z) \neq 0$ , [F2] and the absence of poles give $\log ∣ f (z) ∣ \leq (2 π)^{- 1} \int_{0}^{2 π} P_{R} (z, t) \log^{+} ∣ f (R e^{i t}) ∣ d t$ , since every zero Green term is nonnegative. Indeed $∣ R^{2} - \overline{b} z ∣^{2} - R^{2} ∣ z - b ∣^{2} = (R^{2} - ∣ z ∣^{2}) (R^{2} - ∣ b ∣^{2}) > 0$ , so $G_{R} (z, b) > 0$ . Also $0 < P_{R} (z, t) \leq (R + ∣ z ∣) / (R - ∣ z ∣) \leq (R + r) / (R - r)$ . If $f (z) = 0$ , its $\log^{+}$ is zero, so the same bound for $\log^{+} ∣ f (z) ∣$ holds trivially. Taking the supremum over $∣ z ∣ = r$ yields $\log^{+} M (r, f) \leq \frac{R + r}{R - r} m_{0} (R, f) = \frac{R + r}{R - r} T_{0} (R, f)$ . For a zero on the outer circle, pass through the boundary-radius limit in [F2]; $m_{0} (s, f)$ is continuous in $s$ because $f$ is continuous on compact annuli.

3.1F1F3step 1.1step 1.2step 2.1step 2.2algebra∎

Put $L (r) = \log^{+} M (r, f)$ . From steps 2.1–2.2 with $R = 2 r$ , $T_{0} (r, f) \leq L (r) \leq 3 T_{0} (2 r, f)$ . By [F3] and step 1.1, $T_{0} (r, f) \geq T (r, f) - c > 1 - c > 0$ for all sufficiently large $r$ , while step 1.2 gives $L (r) > 1$ there. Thus the logarithms are defined, $\log T (r, f) - \log T_{0} (r, f) = O (1)$ by the mean-value bound on $[1 - c, \infty)$ , and $\frac{\log T_{0} (r, f)}{\log r} \leq \frac{\log L (r)}{\log r} \leq \frac{\log 3}{\log r} + \frac{\log T_{0} (2 r, f)}{\log r} .$ Replacing $r$ by $2 r$ leaves both limsup and liminf of $\log T_{0} (r, f) / \log r$ unchanged because $\log (2 r) / \log r \to 1$ ; the additive $\log 3 / \log r$ and the bounded $\log T - \log T_{0}$ terms vanish after division by $\log r$ . The squeeze proves both asserted order equalities.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30Open item page →

Rational functions are exactly those with logarithmic characteristic

Statement

Let $f$ be a nonconstant meromorphic function on $C$ . Then $f$ is rational if and only if $T (r, f) = O (\log r) (r \to \infty) .$ More precisely, if $f$ is rational of degree $d \geq 1$ , then $T (r, f) = d \log r + O (1) (r \to \infty),$ for the normalized chordal characteristic.

Facts & Assumptions

Given: A nonconstant meromorphic $f$ on $C$ , with characteristic, closed-disc pole counts, and local pole orders as defined in the cited items.

[F1]

$T (r, h) = m (r, \infty; h) + N (r, \infty; h)$ (Counting, chordal proximity and characteristic).

[F2]

The integrated pole count is $N (r, \infty; h) = n (0, \infty; h) \log r + \int_{0}^{r} \frac{n (t, \infty; h) - n (0, \infty; h)}{t} d t$ (Counting, chordal proximity and characteristic).

[F3]

If $R$ is a fixed rational map of degree $d \geq 1$ and $h$ is nonconstant meromorphic, then $T (r, R (h)) = d T (r, h) + O_{R, h} (1)$ (Elementary characteristic laws and fixed rational composition).

[F4]

For meromorphic $u, v$ and $r \to \infty$ , $T (r, u v) \leq T (r, u) + T (r, v) + O (1)$ (Elementary characteristic laws and fixed rational composition).

[F5]

The count $n (r, a; h)$ is finite for each bounded disc (Well-definedness and radius conventions for Nevanlinna quantities).

[F6]

At a pole of order $m$ , the finite nonzero principal part ends in a nonzero $c_{- m} (z - a)^{- m}$ term; in particular its pole order is $m$ (Characterizations of poles).

[F7]

For an entire $g$ and $0 < r < R$ , $T_{0} (r, g) \leq \log^{+} M (r, g) \leq \frac{R + r}{R - r} T_{0} (R, g),$ where $T_{0} = m_{0} + N (\cdot, \infty; g)$ and $m_{0} (r, g) = (2 π)^{- 1} \int_{0}^{2 π} \log^{+} ∣ g (r e^{i t}) ∣ d t$ (Entire-function order agrees with maximum-modulus order).

[F8]

If $M$ bounds $∣ g ∣$ on $∣ z ∣ = r$ , each Taylor coefficient $a_{n}$ of $g$ at $0$ satisfies $∣ a_{n} ∣ \leq M / r^{n}$ (Cauchy's inequalities bound the Taylor coefficients by the circle supremum).

[F9]

An entire function equals its Taylor series at $0$ throughout $C$ (A holomorphic function equals its Taylor series throughout the largest centred disc in its domain).

[F10]

$δ (w, \infty) = δ (\infty, w) = 1 / \sqrt{1 + ∣ w ∣^{2}}$ , so the integrand of $m (r, \infty; h)$ is $\frac{1}{2} \log (1 + ∣ h ∣^{2})$ (Counting, chordal proximity and characteristic).

[F11]

Every nonempty subset of $N$ has a least element (The well-ordering principle), used for the first integer radius with pole count at least $M$ .

Proof

technique · The rational-composition law proves the forward direction. For the reverse, first bound the pole count, then cancel the finite pole divisor and use the entire maximum-modulus estimate and Cauchy inequalities

1.1F1F3F10algebra

The identity function $z \mapsto z$ is entire and has no poles, so [F1, F10] give its characteristic $T (r, z) = \frac{1}{2} \log (1 + r^{2}) = \log r + O (1)$ . If $f$ is rational of degree $d \geq 1$ , applying [F3] to the composition of $f$ with the identity function gives $T (r, f) = d T (r, z) + O (1) = d \log r + O (1)$ , proving the forward implication and the degree formula.

1.2F1F10algebra

Suppose $T (r, f) = O (\log r)$ , and choose $A \geq 0$ , $r_{0} \geq 1$ so $T (r, f) \leq A \log r$ for every $r \geq r_{0}$ ; by [F1, F10], the integrand defining $m (r, \infty; f)$ is nonnegative, hence $N (r, \infty; f) \leq T (r, f) \leq A \log r$ for $r \geq r_{0}$ .

2.1F2F5F11step 1.2algebra

Let $n_{0} = n (0, \infty; f)$ , finite by [F5], and suppose there are infinitely many poles; since each bounded-disc count is finite by [F5], $n (k, \infty; f)$ is unbounded over positive integers $k$ . Choose an integer $M > \max {A, n_{0}}$ and an integer $s > r_{0}$ , and let $R_{M}$ be the least integer $k \geq s$ with $n (k, \infty; f) \geq M$ ; it exists by unboundedness and well-ordering. For $R \geq R_{M}$ , closed-disc monotonicity gives $n (t, \infty; f) \geq M$ on $[R_{M}, R]$ and $n (t, \infty; f) \geq n_{0}$ everywhere, so [F2] yields $N (R, \infty; f) \geq n_{0} \log R + (M - n_{0}) \log (R / R_{M}) = M \log R - (M - n_{0}) \log R_{M}$ . This contradicts step 1.2 as $R \to \infty$ because $M > A$ , proving that $f$ has finitely many poles.

3.1F5F6step 2.1algebra

List the finite poles as $p_{1}, \dots, p_{s}$ with orders $m_{1}, \dots, m_{s}$ , and set $q (z) = \prod_{j = 1}^{s} (z - p_{j})^{m_{j}}$ , taking $q = 1$ for the empty pole set; at each $p_{j}$ , [F6] gives the exact pole order, so the corresponding zero of $q$ cancels it and $g = q f$ extends holomorphically there, making $g$ entire.

4.1F1F4F7F10step 1.2step 3.1algebra

Put $D = \sum_{j} m_{j}$ and $C_{q} = \prod_{j} (1 + ∣ p_{j} ∣)^{m_{j}}$ , with $D = 0$ , $C_{q} = 1$ for the empty product; for $r \geq 1$ and $∣ z ∣ = r$ , $∣ q (z) ∣ \leq C_{q} r^{D}$ , so [F1, F10] and $\frac{1}{2} \log (1 + ∣ w ∣^{2}) \leq \log^{+} ∣ w ∣ + \frac{1}{2} \log 2$ give $T (r, q) = O (\log r)$ . The product law [F4] applied to $g = q f$ and step 1.2 give $T (r, g) = O (\log r)$ . Define $T_{0} (r, g) = m_{0} (r, g) + N (r, \infty; g)$ as in [F7]; since $g$ is entire its pole count vanishes, and [F1, F10] give $T_{0} (r, g) \leq T (r, g) = O (\log r)$ .

5.1F7F8F9step 4.1algebra∎

If $g$ is constant then $f = g / q$ is rational; otherwise [F7] with $R = 2 r$ gives $\log^{+} M (r, g) \leq 3 T_{0} (2 r, g) = O (\log r)$ , hence $M (r, g) \leq C_{1} r^{B}$ for some $C_{1} > 0$ , $B \geq 0$ and all large $r$ . Write $g (z) = \sum_{n \geq 0} a_{n} z^{n}$ ; for every integer $n > B$ , [F8] gives $∣ a_{n} ∣ \leq M (r, g) / r^{n} \leq C_{1} r^{B - n} \to 0$ , so $a_{n} = 0$ . Thus only finitely many coefficients are nonzero, [F9] makes $g$ a polynomial, and $f = g / q$ is rational.

5 · Examples, counterexamples and false statements

None yet.

Jensen Theory and Nevanlinna's First Main Theorem

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

Poisson–Jensen formula for a meromorphic function on a disc

Statement

Facts & Assumptions

Proof

Counting, chordal proximity and characteristic

Definition

Well-definedness and radius conventions for Nevanlinna quantities

Statement

Facts & Assumptions

Proof

Meromorphic Jensen identity with a zero or pole at the centre

Statement

Facts & Assumptions

Proof

Ahlfors–Shimizu area form of the characteristic

Statement

Facts & Assumptions

Proof

Nevanlinna’s First Main Theorem with exact centre constant

Statement

Facts & Assumptions

Proof

Elementary characteristic laws and fixed rational composition

Statement

Facts & Assumptions

Proof

Order and lower order from the Nevanlinna characteristic

Statement

Facts & Assumptions

Proof

Entire-function order agrees with maximum-modulus order

Statement

Facts & Assumptions

Proof

Rational functions are exactly those with logarithmic characteristic

Statement

Facts & Assumptions

Proof

5 · Examples, counterexamples and false statements

Sources