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.

Nevanlinna's Second Main Theorem and Defects

1 · Prerequisites

2 · Summary

The Second Main Theorem is the quantitative statement that a meromorphic function cannot distribute its preimages too evenly. This page sets up the error notation $S (r, f)$ , an error bounded by $C (\log^{+} T (r, f) + \log r)$ outside a Lebesgue-measurable set of finite linear measure, and the truncated count $\overset{ˉ}{N}$ and ramification count $N_{1}$ , measuring distinct preimages and local-degree surplus respectively. The ramification counting identity $N_{1} (r, f) = N (r, 0; f^{'}) + 2 N (r, \infty; f) - N (r, \infty; f^{'})$ converts the derivative divisor into the local-degree surplus.

The analytic input is the logarithmic-derivative lemma, proved from a separated-radius Poisson–Jensen derivative bound and the Borel finite-measure growth increment, with the finite-order refinement $O (\log r)$ at every large radius and the rational refinement $O (1)$ . The plane Second Main Theorem then reads $\sum_{j} m (r, a_{j}; f) + N_{1} (r, f) \leq 2 T (r, f) + S (r, f)$ for distinct targets $a_{1}, \dots, a_{q}$ , $q \geq 3$ , and rearranges to $(q - 2) T (r, f) \leq \sum_{j} \overset{ˉ}{N} (r, a_{j}; f) + S (r, f)$ . A separate punctured-disc theorem supplies the same inequality on an exterior characteristic after inversion of an isolated singularity, with the exceptional set measured in the exterior radius.

Deficiency and ramification indices, the defect relation $\sum_{a} (δ (a, f) + ε (a, f)) \leq 2$ , the five-value uniqueness theorem and the Little and Great Picard theorems are derived from these estimates. A choice-free Schottky/normal-family exterior lemma gives an independent route to the three-omitted-values extension. Countable Choice is carried by the exceptional-set measure interface and by the analytic suppliers that use it; the counting and covering arguments are choice-free.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-10-02Open item page →

Nevanlinna exceptional-radius error notation

Definition

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Under this assumption the Lebesgue measurable subsets of $R$ form a $σ$ -algebra and Lebesgue measure is a complete measure (Lebesgue measurable sets, the family $L (R^{n})$ , and the restricted set function $λ_{n}$ , Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume).

Let $f$ be a nonconstant meromorphic function on $C$ , with characteristic $T (r, f)$ as in Counting, chordal proximity and characteristic. By Order and lower order from the Nevanlinna characteristic, $T (r, f) > 1$ for all sufficiently large $r$ .

An error term for $f$ , written $S (r, f)$ , is a function $e$ on a half-line $[r_{0}, \infty)$ with $r_{0} \geq 1$ for which there are a constant $C \geq 0$ , a radius $r_{0}^{'} \geq r_{0}$ , and a Lebesgue measurable set $E \subseteq [r_{0}^{'}, \infty)$ of finite linear measure, $λ (E) < \infty$ , such that

$∣ e (r) ∣ \leq C (\log^{+} T (r, f) + \log r) for every r \geq r_{0}^{'} with r \notin E .$

The notation $X (r, f) = S (r, f)$ means that the function $r \mapsto X (r, f)$ is an error term in this sense; the constant $C$ , the threshold $r_{0}^{'}$ and the exceptional set $E$ belong to that particular occurrence. No bound is asserted at the radii belonging to $E$ .

Remarks

The exceptional set is part of each occurrence. Two occurrences of $S (r, f)$ in one formula may use different constants, thresholds and exceptional sets. A chain of estimates that uses $k$ occurrences may take the union $E_{1} \cup \dots \cup E_{k}$ as a common exceptional set; a finite union of sets of finite linear measure again has finite linear measure, and the sum of the constants bounds the sum of the error terms.
$S (r, f)$ denotes no single fixed function. Error terms for fixed $f$ are closed under finite real linear combinations on a common half-line, by the finite-union estimate above. The symbol abbreviates "some function satisfying the displayed bound"; replacing the constant or the exceptional set by larger ones produces another valid occurrence of the same symbol.
No all-radius bound and no sharper order is implicit. Membership in $S (r, f)$ alone gives no information at exceptional radii and no information beyond the stated bound. The logarithmic-derivative lemma supplies an all-radius $O (\log r)$ estimate when $f$ has finite order and an all-radius $O (1)$ estimate when $f$ is rational. These are sufficient hypotheses for those estimates, not necessary ones: for $f (z) = e^{z}$ , $f^{'} / f = 1$ and $m_{0} (r, f^{'} / f) = 0$ at every radius although $f$ is transcendental. No refinement of an arbitrary occurrence of $S (r, f)$ follows solely from the order or rationality of $f$ .
The exact use of Countable Choice. It is used only through the published measure interface: finite linear measure of $E$ and its finite unions, and the measurability of the sets of bad radii that occur. Every occurrence of $S (r, f)$ in this page carries the assumption explicitly, and no stronger choice principle is used.

DefinitionDefinition: Literature-sourcedProof: AI-adaptedjudge pass (gpt-6.1-sol)audited 2026-10-02Open item page →

Truncated value and ramification counts

Definition

Let $f$ be a nonconstant meromorphic function on $C$ and let $a \in \hat{C}$ be a sphere target. Fix $r > 0$ and let $D_{r}$ be the closed disc $∣ z ∣ \leq r$ . Counting conventions and the integrated count $N (r, a; f)$ follow Counting, chordal proximity and characteristic; its centre-regularized integral is

$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 .$

Truncated and weighted counts at one target. For finite $a$ , write the $a$ -points of $f$ in $D_{r}$ as the finite set of distinct points $b$ with local degree $m_{b}$ , so that $m_{b} \geq 1$ is the order of the zero of $f - a$ at $b$ ; for $a = \infty$ write the poles in $D_{r}$ as $p$ with pole order $m_{p}$ . Put

$\overset{ˉ}{n} (r, a; f) : = # {b \in D_{r} : f (b) = a} (a \neq \infty), \overset{ˉ}{n} (r, \infty; f) : = # {p \in D_{r} : p a pole},$

the number of distinct $a$ -points counted once, and

$n_{1} (r, a; f) : = \sum_{b \in D_{r}, f (b) = a} (m_{b} - 1) (a \neq \infty), n_{1} (r, \infty; f) : = \sum_{p \in D_{r}} (m_{p} - 1),$

the same points counted with weight "local degree minus one". The corresponding integrated quantities use the same centre regularization:

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

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

Then $n (r, a; f) = \overset{ˉ}{n} (r, a; f) + n_{1} (r, a; f)$ for every $r > 0$ and every sphere target $a$ , and consequently

$N (r, a; f) = \overset{ˉ}{N} (r, a; f) + N_{1} (r, a; f) .$

Ramification of the sphere map. Let $m_{b} \geq 1$ denote the local degree of the meromorphic sphere map $f$ at $b$ : for a non-pole $b$ , this is the order of the zero of $f - f (b)$ at $b$ , and at a pole it is the pole order. Call $b$ a ramification point when $m_{b} \geq 2$ and put

$n_{1} (t, f) : = \sum_{b \in D_{t}, m_{b} \geq 2} (m_{b} - 1), N_{1} (r, f) : = n_{1} (0, f) \log r + \int_{0}^{r} \frac{n_{1} (t, f) - n_{1} (0, f)}{t} d t,$

the integrated count of all ramification points of the sphere map $f$ , each weighted by its local degree minus one. The symbols $\overset{ˉ}{N}$ and $N_{1}$ are reserved for these counts; the unbarred $N$ keeps full multiplicity.

Facts & Assumptions

Given: A nonconstant meromorphic $f$ on $C$ , a sphere target $a$ , and $r > 0$ .

[F1]

$n (r, a; f)$ counts local multiplicities on the closed disc $∣ z ∣ \leq r$ with poles counted for $a = \infty$ , and $N$ is its centre-regularized integral (Counting, chordal proximity and characteristic).

[F2]

The counts $n (r, a; f)$ are finite for every bounded disc, and $N (r, a; f)$ is finite for every $r > 0$ (Well-definedness and radius conventions for Nevanlinna quantities).

[F3]

A zero of finite order $m$ 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).

[F4]

A pole of order $m$ has a reciprocal with a zero of order $m$ , and $∣ f (z) ∣ \to \infty$ as $z$ tends to the pole (Characterizations of poles).

[F5]

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

[F6]

A holomorphic function with $f^{'} = 0$ throughout a complex domain is constant there (A holomorphic function with zero derivative on a domain is constant).

Proof

Proof technique: verify that the local-degree weights add up to the full multiplicity, then show that $f^{'} \equiv̸ 0$ so that the ramification points form a locally finite divisor.

1.1F1F3F4algebra

At a finite target $a$ and a point $b \in D_{r}$ with $f (b) = a$ , [F3] writes $f - a = (z - b)^{m_{b}} h$ with $h (b) \neq 0$ and $m_{b} \geq 1$ ; the point contributes $1$ to $\overset{ˉ}{n}$ and $m_{b} - 1$ to $n_{1}$ , hence $m_{b}$ to their sum, matching its contribution to $n$ . At $a = \infty$ , [F4] gives a pole of order $m_{p}$ contributing $1$ and $m_{p} - 1$ ; summing the finitely many points of $D_{r}$ gives $n (r, a; f) = \overset{ˉ}{n} (r, a; f) + n_{1} (r, a; f)$ .

1.2F4F5F6algebra

The derivative satisfies $f^{'} \equiv̸ 0$ : if $f^{'} \equiv 0$ , then $f$ is holomorphic with zero derivative on $Ω = C ∖ P$ , where $P$ is the pole set, and $Ω$ is a domain because [F5] makes $P$ closed and discrete, so $P \neq C$ and any two points of $Ω$ are joined by a polygonal path that meets $P$ in only finitely many points and can be detoured around them. By [F6], $f$ is constant, say $f = c$ , on $Ω$ . Near a pole $p \in P$ it would then follow from [F4] that $∣ f ∣ \to \infty$ , contradicting $f = c$ on a punctured neighbourhood of $p$ ; so $P = \emptyset$ and $f \equiv c$ on $C$ , contradicting nonconstancy.

2.1F2step 1.1algebra

Since $0 \leq \overset{ˉ}{n} (r, a; f) \leq n (r, a; f)$ and $0 \leq n_{1} (r, a; f) \leq n (r, a; f)$ pointwise by step 1.1, and $n (r, a; f)$ is finite on every bounded disc, both $\overset{ˉ}{n}$ and $n_{1}$ are finite there.

2.2F4F5step 1.2algebra

The zeros of $f^{'}$ are locally finite and do not accumulate at poles. At a pole $p$ of order $m$ , [F4] gives a local representation $f = (z - p)^{- m} g$ with $g$ holomorphic and $g (p) \neq 0$ , so $f^{'} = (z - p)^{- m - 1} (- m g + (z - p) g^{'})$ has a pole of order $m + 1$ there and no zero in a small punctured neighbourhood. Away from the poles $f^{'}$ is holomorphic and, by step 1.2, not identically zero on the domain $C ∖ P$ ; hence its zeros are isolated (Zeros of a nonzero holomorphic function are isolated). A set of isolated points with no accumulation point in $C$ has only finitely many members in each bounded closed disc: otherwise a sequence of distinct zeros in the disc would converge, by compactness, to a limit that is an accumulation point.

2.3F1F2step 1.1algebra

Since $n = \overset{ˉ}{n} + n_{1}$ pointwise by step 1.1, including at the centre $z = 0$ , and since $n_{1} (t, a; f) \leq n (t, a; f)$ is finite for every $t > 0$ by [F2], subtracting the centre terms and integrating against $d t / t$ gives $N (r, a; f) = \overset{ˉ}{N} (r, a; f) + N_{1} (r, a; f)$ for every $r > 0$ ; the definition of $N_{1} (r, f)$ uses the same centre regularization as the displayed formulas.

3.1F2F3F4step 2.2algebra

The ramification points of the sphere map are exactly the zeros of $f^{'}$ together with the poles of order at least two. At a non-pole point $b$ where [F3] gives $f - f (b) = (z - b)^{m} h$ with $h (b) \neq 0$ and $m \geq 1$ , the product rule gives $f^{'} = (z - b)^{m - 1} (m h + (z - b) h^{'})$ with $m h (b) \neq 0$ , so $f^{'}$ has a zero of order exactly $m - 1$ at $b$ ; hence $m \geq 2$ exactly when $f^{'} (b) = 0$ , and then the ramification weight $m - 1$ equals the zero order of $f^{'}$ . At a pole of order $m$ , the representation of step 2.2 shows that the local degree is $m$ and the weight $m - 1$ , while $f^{'}$ has no zero there. Therefore $n_{1} (t, f) = n (t, 0; f^{'}) + \sum_{∣ p ∣ \leq t} (m_{p} - 1)$ for every $t > 0$ , and this is finite by [F2] and step 2.2.

4.1step 2.1step 2.2step 2.3step 3.1∎

Steps 1.1 and 2.3 give the pointwise and integrated identities, and steps 2.1, 2.2 and 3.1 show that every count introduced above is finite on each bounded disc and that the ramification points form a locally finite divisor, so the definition is well posed.

LemmaStatement: Literature-sourcedProof: AI-adaptedaudited 2026-10-02Open item page →

Finite-measure growth increment lemma

Statement

Assume Countable Choice. Let $u : [r_{0}, \infty) \to [1, \infty)$ be continuous, nondecreasing and unbounded, and let $ε > 0$ . Then there is a Lebesgue measurable set $E \subseteq [r_{0}, \infty)$ of finite linear measure such that for every $r \in [r_{0}, \infty) ∖ E$ $u (r + u (r)^{- 1 - ε}) < u (r) + 1.$ In particular the lemma applies to $u (r) = T (r, f)$ for a nonconstant meromorphic $f$ after increasing $r_{0}$ so that $T (r, f) > 1$ there.

Facts & Assumptions

Given: A continuous, nondecreasing, unbounded $u : [r_{0}, \infty) \to [1, \infty)$ and $ε > 0$ ; Countable Choice is assumed.

[F1]

Under Countable Choice, the Lebesgue measurable sets of $R$ form a $σ$ -algebra, Lebesgue measure is complete, and every elementary set (a finite union of half-open intervals) is Lebesgue measurable of the expected length (Nevanlinna exceptional-radius error notation, Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume).

[F2]

Lebesgue measure is countably subadditive on measurable sets: if $E_{1}, E_{2}, \dots$ are measurable with measurable union, then $λ (⋃_{j} E_{j}) \leq \sum_{j} λ (E_{j})$ (Finite and countable subadditivity of measures).

[F3]

For every real exponent $p > 1$ the series $\sum_{m \geq 1} m^{- p}$ converges (The p-series for a real exponent p converges exactly when p is greater than one).

[F4]

Ahlfors–Shimizu: $T (r, f) = T_{A S} (r, f) + C_{\infty} (f)$ , where $T_{A S}$ is finite and nondecreasing and is convex as a function of $\log r$ ; hence $T (\cdot, f)$ is continuous and nondecreasing, and $T (r, f) > 1$ for all sufficiently large $r$ (Ahlfors–Shimizu area form of the characteristic, Nevanlinna exceptional-radius error notation).

[F5]

$f$ is rational if and only if $T (r, f) = O (\log r)$ ; for rational $f$ of degree $d \geq 1$ , $T (r, f) = d \log r + O (1)$ (Rational functions are exactly those with logarithmic characteristic).

Proof

technique · split the failure set according to the integer level of $u$; the first crossing radii $s_m$ of the levels $m$ give an explicit cover of the failure set by intervals of lengths $m^{-1-\varepsilon}$, whose total length is a convergent series

1.1F1givenchoose

For every integer $m \geq 1$ the superlevel set ${r \geq r_{0} : u (r) \geq m}$ is closed in $[r_{0}, \infty)$ , and it is nonempty for $m \leq \lim_{r \to \infty} u (r) = \infty$ ; let $s_{m}$ be its least element, and put $m_{0} : = ⌈ u (r_{0}) ⌉$ . Then $s_{m} \leq s_{m + 1}$ .

1.2givenalgebra

(Failure set) Put $φ (t) : = t^{- 1 - ε}$ and $F : = {r \geq r_{0} : u (r + φ (u (r))) \geq u (r) + 1}$ . The function $r \mapsto u (r + φ (u (r))) - u (r) - 1$ is continuous on $[r_{0}, \infty)$ because $u$ and $φ$ are continuous; hence $F$ is closed in $[r_{0}, \infty)$ .

1.3F4F5given

(Application to $T$ ) Let $f$ be a nonconstant meromorphic function. By [F4] the function $T (\cdot, f)$ is continuous and nondecreasing in $r$ (the constant $C_{\infty} (f)$ is additive). It is also unbounded: $T$ has a limit because it is nondecreasing, and if that limit were finite then $T (r, f) = O (\log r)$ for large $r$ ; [F5] would then make $f$ rational of some degree $d \geq 1$ , and the same item gives $T (r, f) = d \log r + O (1) \to \infty$ , a contradiction, while constant $f$ is excluded. Increasing $r_{0}$ so that $T (r_{0}, f) \geq 1$ , the lemma applies to $u = T (\cdot, f)$ .

2.1F1F2F3step 1.1algebra

(Measurability and finite measure of the cover) Every bounded closed interval $[a, b]$ is a countable intersection of half-open intervals $(a - 1 / n, b]$ , hence Lebesgue measurable by [F1]; the same intervals cover it with measures tending to $b - a$ , so $λ ([a, b]) \leq b - a$ . Set $E : = [r_{0}, \infty) \cap ([r_{0}, s_{m_{0}}] \cup ⋃_{m \geq m_{0}} [s_{m + 1} - m^{- 1 - ε}, s_{m + 1}]) .$ This set is measurable, is contained in $[r_{0}, \infty)$ , and by [F2] $λ (E) \leq s_{m_{0}} - r_{0} + \sum_{m \geq m_{0}} m^{- 1 - ε} < \infty$ by [F3] and $ε > 0$ .

2.2givenstep 1.1algebra

If $m > u (r_{0})$ then $s_{m} > r_{0}$ and $u (s_{m}) = m$ : by definition $u (s_{m}) \geq m$ , and if $u (s_{m}) > m$ then by continuity $u > m$ on a left neighbourhood of $s_{m}$ inside $[r_{0}, \infty)$ , contradicting minimality. If $m = u (r_{0})$ the same holds with $s_{m} = r_{0}$ .

3.1givenstep 2.2step 1.2step 1.1algebra

(Cover of the failure set) Recall $m_{0} = ⌈ u (r_{0}) ⌉$ from step 1.1 and let $r \in F$ with $r \geq s_{m_{0}}$ . Write $m : = ⌊ u (r) ⌋ \geq m_{0}$ . Then $u (r) \in [m, m + 1)$ , so $r \geq s_{m}$ and $r < s_{m + 1}$ . Moreover $u (r) \geq m$ , so by step 2.2, $u (r + φ (u (r))) \geq u (r) + 1 \geq m + 1 = u (s_{m + 1})$ ; monotonicity of $u$ then forces $r + φ (u (r)) \geq s_{m + 1}$ , i.e. $r \geq s_{m + 1} - φ (u (r)) \geq s_{m + 1} - φ (m)$ . Hence $F \cap [s_{m_{0}}, \infty) \subseteq ⋃_{m \geq m_{0}} [s_{m + 1} - m^{- 1 - ε}, s_{m + 1}] \cup [r_{0}, s_{m_{0}}] .$

4.1step 3.1step 2.1algebra

(Conclusion off $E$ ) If $r \geq r_{0}$ and $r \notin E$ , then $r \notin [r_{0}, s_{m_{0}}]$ , so $r > s_{m_{0}}$ ; since $r$ lies in no interval $[s_{m + 1} - m^{- 1 - ε}, s_{m + 1}]$ with $m \geq m_{0}$ either, step 3.1 gives $r \notin F$ : unwinding the definition of $F$ , $u (r + φ (u (r))) < u (r) + 1$ , as required.

5.1F1given∎

The argument selects nothing: each $s_{m}$ is the least element of a nonempty closed set, and the covering intervals are defined from the $s_{m}$ and the given constants. Countable Choice is used only through the published Lebesgue measure interface of [F1].

LemmaStatement: Literature-sourcedProof: AI-adaptedaudited 2026-10-02Open item page →

Separated-radius Poisson–Jensen derivative bound

Statement

Let $f$ be a nonconstant meromorphic function on $C$ , let $0 < α < 1$ , and let $2 \leq r < R$ . Denote by $m_{0}$ the standard proximity, $m_{0} (r, f^{'} / f) = \frac{1}{2 π} \int_{0}^{2 π} \log^{+} ∣ f^{'} (r e^{i t}) / f (r e^{i t}) ∣ d t$ , with the logarithmic singularities interpreted as an integrable angular integrand. Then there are constants $C_{f, α} < \infty$ (depending only on $f$ and $α$ ) and $C_{α} < \infty$ (depending only on $α$ ) with $m_{0} (r, f^{'} / f) \leq C_{f, α} + C_{α} (\log^{+} T (R, f) + \log R + \log^{+} \frac{1}{R - r}) .$ No limit $R ↓ r$ is asserted: the bound depends on the separation $R - r$ .

Facts & Assumptions

Given: A nonconstant meromorphic $f$ on $C$ , $0 < α < 1$ and radii $2 \leq r < R$ .

[F1]

Poisson–Jensen formula on $∣ z ∣ < s$ : for meromorphic $h$ on a neighbourhood of $∣ z ∣ \leq s$ with no zero or pole on $∣ z ∣ = s$ , $\log ∣ h (z) ∣ = \frac{1}{2 π} \int_{0}^{2 π} P_{s} (z, s e^{i t}) \log ∣ h (s e^{i t}) ∣ d t - \sum m_{b} G_{s} (\cdot)$ contributions of the zeros and poles, with $G_{s} (z, a) = \log ∣ \frac{s^{2} - \overset{ˉ}{a} z}{s (z - a)} ∣$ ; at a divisor radius the identity is the limit through regular radii (Poisson–Jensen formula for a meromorphic function on a disc).

[F2]

Counting, proximity and characteristic: for finite $w$ , $\log \frac{1}{δ (w, \infty)} = \frac{1}{2} \log (1 + ∣ w ∣^{2})$ ; $T = m (\cdot, \infty) + N (\cdot, \infty)$ ; the centre-regularized count is $N (r, a; h) = n (0, a; h) \log r + \int_{0}^{r} \frac{n (t, a; h) - n (0, a; h)}{t} d t$ (Counting, chordal proximity and characteristic). The bounds $\log^{+} ∣ w ∣ \leq \frac{1}{2} \log (1 + ∣ w ∣^{2})$ and $\log^{+} ∣ 1 / w ∣ \leq \frac{1}{2} \log (1 + ∣ w ∣^{- 2})$ control the two standard proximities separately.

[F3]

First Main Theorem for nonconstant meromorphic $h$ , with exact centre constant: $m (r, a; h) + N (r, a; h) = T (r, h) + C (h, a)$ for every sphere target $a$ , with $C (h, \infty) = 0$ ; for finite $a$ and $h (z) - a = c_{a} z^{k_{a}} + \dots$ , $C (h, a) = \frac{1}{2} \log (1 + ∣ a ∣^{2}) - \log ∣ c_{a} ∣$ (Nevanlinna’s First Main Theorem with exact centre constant). In particular $m (r, a; h) \leq T (r, h) + C (h, a)$ .

[F4]

Characteristic laws: $T (r, 1 / h) = T (r, h) + O_{h} (1)$ and $T (r, g h) \leq T (r, g) + T (r, h) + O (1)$ as $r \to \infty$ (Elementary characteristic laws and fixed rational composition).

[F5]

$n (r, a; h)$ is finite on bounded discs, and $N (\cdot, a; h)$ and $m (\cdot, a; h)$ are finite and continuous; for $s < R$ , $N (R, a; h) - N (s, a; h) = \int_{s}^{R} n (t, a; h) \frac{d t}{t}$ (Well-definedness and radius conventions for Nevanlinna quantities).

[F6]

A zero of finite order $k$ at the centre factors as $h (z) = z^{k} g (z)$ with $g$ holomorphic and $g (0) \neq 0$ (The order of a zero is the exponent in its local holomorphic factorization).

[F7]

At a pole, the reciprocal has a zero of the same order (Characterizations of poles).

[F8]

On a probability space, Jensen's integral inequality for the convex function $x \mapsto - \log (1 + x)$ gives $E \log (1 + X) \leq \log (1 + E X)$ for nonnegative integrable $X$ ; the logarithm is integrable since $\log (1 + X) \leq X$ (Jensen's integral inequality for a probability measure).

Proof

technique · normalize the centre value; differentiate the Poisson–Jensen formula; bound the boundary kernel by the characteristic and the divisor kernels by $1/|z-c|$; use $\alpha$-power angular means and Jensen's inequality to obtain the proximity bound

1.1F4F6F7algebra

(Reduction to centre value $1$ ) Let $k \in Z$ be the signed order of $f$ at $0$ (negative for a pole), and write $f (z) = c z^{k} h (z)$ with $c \neq 0$ , $h$ meromorphic on $C$ , and $h (0) = 1$ . The local zero and pole factorizations justify this form; when $k = 0$ , take $c = f (0)$ . Then $f^{'} / f = k / z + h^{'} / h$ . The proximity sum inequality gives, for $r \geq 2$ , $m_{0} (r, f^{'} / f) \leq m_{0} (r, h^{'} / h) + \log^{+} (∣ k ∣ / r) + \log 2 \leq m_{0} (r, h^{'} / h) + \log^{+} ∣ k ∣ + \log 2,$ where the $k / z$ term is zero when $k = 0$ . If $h$ is constant then $h \equiv 1$ , so $f^{'} / f = k / z$ and $m_{0} (r, f^{'} / f) \leq \log^{+} ∣ k ∣$ for $r \geq 2$ , proving the stated bound directly with a constant depending on $f$ . In all subsequent steps assume $h$ is nonconstant. The characteristic laws and the direct rational-map estimate $T (R, c^{- 1} z^{- k}) = ∣ k ∣ \log R + O_{f} (1)$ for $R \geq 2$ give $T (R, h) \leq T (R, f) + ∣ k ∣ \log R + O_{f} (1) .$

1.2F2F3algebra

(Vanishing centre constants) For $h$ with $h (0) = 1$ , [F3] gives $C (h, 0) = \frac{1}{2} \log 1 - \log 1 = 0$ and $C (h, \infty) = 0$ , hence $m (s, 0; h) + N (s, 0; h) = T (s, h) = m (s, \infty; h) + N (s, \infty; h)$ . For every $w$ one has $\log^{+} ∣ w ∣ \leq \frac{1}{2} \log (1 + ∣ w ∣^{2})$ and $\log^{+} \frac{1}{∣ w ∣} \leq \frac{1}{2} \log (1 + ∣ w ∣^{- 2})$ , so taking angular means gives $\frac{1}{2 π} \int_{0}^{2 π} ∣ \log ∣ h (s e^{i t}) ∣ ∣ d t \leq m (s, 0; h) + m (s, \infty; h) \leq 2 T (s, h) .$

1.3F1F5algebra

(Differentiated Poisson–Jensen) Let $0 < r < s < R$ with $∣ z ∣ = s$ carrying no zero or pole of $h$ ; [F1] applies on $∣ z ∣ < s$ . Differentiation in $z$ of [F1], whose boundary kernel and Green kernels are smooth for $∣ z ∣ < s$ and whose divisor sum is finite, gives for $∣ z ∣ < s$ $\frac{h^{'} (z)}{h (z)} = \frac{1}{2 π} \int_{0}^{2 π} \log ∣ h (s e^{i t}) ∣ \frac{2 s e^{i t}}{(s e^{i t} - z)^{2}} d t + \sum_{h (c) = 0} \frac{s^{2} - ∣ c ∣^{2}}{(s^{2} - \overset{ˉ}{c} z) (z - c)} - \sum_{p p o l e} \frac{s^{2} - ∣ p ∣^{2}}{(s^{2} - \overset{ˉ}{p} z) (z - p)},$ the divisor sums running over the zeros and poles in $∣ z ∣ < s$ with multiplicity; at a radius $s$ meeting the divisor, take regular $s_{j} ↓ s$ and pass to the limit using the continuity of [F5].

1.4algebra

(Angular integral of one kernel) For any $c$ and every $φ$ one has $∣ r e^{i φ} - c ∣ \geq r ∣ \sin φ ∣$ after rotating $c$ to $∣ c ∣$ : indeed $r^{2} - 2 r ∣ c ∣ \cos φ + ∣ c ∣^{2} - r^{2} \sin^{2} φ = (r \cos φ - ∣ c ∣)^{2} \geq 0$ . Hence, using $\sin φ \geq 2 φ / π$ on $[0, π / 2]$ , $\frac{1}{2 π} \int_{0}^{2 π} \frac{d φ}{∣ r e^{i φ} - c ∣^{α}} \leq \frac{1}{2 π r^{α}} \int_{0}^{2 π} \frac{d φ}{∣ \sin φ ∣^{α}} \leq \frac{2}{(1 - α) r^{α}} .$

2.1step 1.3algebra

(Kernel bounds) For $∣ z ∣ = r < s$ : $∣ \frac{2 s e^{i t}}{(s e^{i t} - z)^{2}} ∣ \leq \frac{2 s}{(s - r)^{2}}$ ; and for a divisor point $c$ with $∣ c ∣ < s$ , using $∣ s^{2} - \overset{ˉ}{c} z ∣ \geq s^{2} - ∣ c ∣ r$ , $∣ \frac{s^{2} - ∣ c ∣^{2}}{(s^{2} - \overset{ˉ}{c} z) (z - c)} ∣ = \frac{(s + ∣ c ∣) (s - ∣ c ∣)}{∣ s^{2} - \overset{ˉ}{c} z ∣ ∣ z - c ∣} \leq \frac{s + ∣ c ∣}{s} \cdot \frac{1}{∣ z - c ∣} \leq \frac{2}{∣ z - c ∣},$ because $\frac{(s - ∣ c ∣) s}{s^{2} - r ∣ c ∣} \leq 1$ for $0 \leq ∣ c ∣ < s$ and $r < s$ .

3.1F5step 1.2step 1.3step 2.1algebra

(Pointwise bound) Combining steps 1.3 and 2.1 with step 1.2 at $∣ z ∣ = r$ , $∣ \frac{h^{'} (z)}{h (z)} ∣ \leq \frac{2 s}{(s - r)^{2}} \cdot 2 T (s, h) + 2 \sum_{∣ c ∣ < s} \frac{1}{∣ z - c ∣} = \frac{4 s T (s, h)}{(s - r)^{2}} + 2 Σ (z),$ where the last sum extends over all zeros and poles of $h$ in $∣ z ∣ < s$ (each repeated according to multiplicity) and is finite by [F5].

4.1step 3.1algebra

( $α$ -power mean) Fix $α \in (0, 1)$ . By $(x + y)^{α} \leq x^{α} + y^{α}$ for $x, y \geq 0$ , $\frac{1}{2 π} \int_{0}^{2 π} ∣ \frac{h^{'} (r e^{i φ})}{h (r e^{i φ})} ∣^{α} d φ \leq (\frac{4 s T (s, h)}{(s - r)^{2}})^{α} + \frac{2^{α}}{2 π} \int_{0}^{2 π} Σ (r e^{i φ})^{α} d φ,$ and $Σ (r e^{i φ})^{α} \leq \sum_{∣ c ∣ < s} ∣ r e^{i φ} - c ∣^{- α}$ again by the subadditivity for exponent $α < 1$ .

4.2F3F5step 3.1algebra

(Counting the divisor) Let $n (s; 0, \infty) : = n (s, 0; h) + n (s, \infty; h)$ . From [F5], $N (R, a; h) - N (s, a; h) \geq n (s, a; h) \log (R / s)$ for $a = 0, \infty$ ; by [F3], $N (R, a; h) \leq T (R, h) + C (h, a)$ , and $\log \frac{R}{s} \geq \frac{R - s}{R}$ for $s < R$ . With $s : = \frac{R + r}{2}$ this gives $n (s, a; h) \leq \frac{2 R (T (R, h) + C (h, a))}{R - r}$ , hence $n (s; 0, \infty) \leq \frac{4 R T (R, h)}{R - r} + C_{h}^{'}$ for a constant $C_{h}^{'} \geq 0$ .

5.1F8step 1.2step 4.1step 4.2algebra

(Proximity bound) On normalized angular measure put $X (φ) : = ∣ h^{'} (r e^{i φ}) / h (r e^{i φ}) ∣^{α}$ , defined arbitrarily at its measure-zero singularities. Step 4.1 gives $X \in L^{1}$ , so $\log (1 + X) \in L^{1}$ . For $u \geq 0$ , $\log^{+} u \leq α^{- 1} \log (1 + u^{α})$ ; applying this pointwise and [F8] to $X$ yields $m_{0} (r, h^{'} / h) \leq \frac{1}{α} \log (1 + \frac{1}{2 π} \int_{0}^{2 π} X (φ) d φ) .$ For $s = \frac{R + r}{2}$ , steps 4.1 and 4.2 bound the integral mean by $A^{α} + B$ , where $A : = \frac{16 R T (R, h)}{(R - r)^{2}}, B : = \frac{2^{α + 1}}{(1 - α) r^{α}} (\frac{4 R T (R, h)}{R - r} + C_{h}^{'}) .$ Thus $m_{0} (r, h^{'} / h) \leq α^{- 1} \log (1 + A^{α} + B)$ . Since $r \geq 2$ , $\log (1 + A^{α} + B) \leq \log 3 + \log^{+} A + \log^{+} B,$ while $\log^{+} A \leq \log^{+} T (R, h) + \log R + 2 \log^{+} \frac{1}{R - r} + \log 16$ and $\log^{+} B \leq C_{α} + C_{h} + \log^{+} T (R, h) + \log R + \log^{+} \frac{1}{R - r} .$ Absorbing fixed terms into $C_{h, α}$ and enlarging $C_{α}$ proves the required bound.

6.1step 1.1step 5.1algebra∎

(Undoing the normalization) By step 1.1, $T (R, h) \leq T (R, f) + O_{f} (\log R)$ and $\log^{+} T (R, h) \leq \log^{+} T (R, f) + \log R + O_{f} (1)$ for $R \geq 2$ after enlarging the fixed constants, by continuity on any remaining compact radius interval; absorbing the constants depending on $f$ (including $\log^{+} ∣ k ∣$ and the fixed normalization terms) into $C_{f, α}$ and the numerical factors into $C_{α}$ yields $m_{0} (r, f^{'} / f) \leq C_{f, α} + C_{α} (\log^{+} T (R, f) + \log R + \log^{+} \frac{1}{R - r})$ for all $2 \leq r < R$ .

LemmaStatement: Literature-sourcedProof: AI-adaptedaudited 2026-10-02Open item page →

Ramification count from the derivative divisor

Statement

Let $f$ be a nonconstant meromorphic function on $C$ . For every $r > 0$ the ramification count of the sphere map, including the centre regularisation, is $N_{1} (r, f) = N (r, 0; f^{'}) + 2 N (r, \infty; f) - N (r, \infty; f^{'}) .$ Moreover, for every $r \geq 1$ and every finite set $A$ of distinct sphere targets, $\sum_{a \in A} N_{1} (r, a; f) \leq N_{1} (r, f) .$

Facts & Assumptions

Given: A nonconstant meromorphic $f$ on $C$ and $r > 0$ .

[F1]

Truncated and ramification counts: $n (r, a; f) = \overset{ˉ}{n} (r, a; f) + n_{1} (r, a; f)$ and $N = N_{1} (r, a; f) + \overset{ˉ}{N} (r, a; f)$ ; $n_{1} (t, f)$ sums $(m_{b} - 1)$ over the points of local degree $m_{b} \geq 2$ of the sphere map, and $N_{1} (r, f)$ is its centre-regularized integral (Truncated value and ramification counts).

[F2]

Counting conventions: $n (r, a; f)$ is the multiplicity sum over the closed disc $∣ z ∣ \leq r$ , and $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$ (Counting, chordal proximity and characteristic).

[F3]

A zero of finite order $m$ 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).

[F4]

At a pole $p$ of order $m$ , the function factors as $(z - p)^{- m} g$ with $g$ holomorphic, $g (p) \neq 0$ (Characterizations of poles).

[F5]

All counts $n (t, a; f)$ and $n_{1} (t, f)$ are finite, and the regularized integrals are finite and continuous in $r$ (Well-definedness and radius conventions for Nevanlinna quantities, Truncated value and ramification counts).

Proof

technique · compare the local weights of the two sides point by point, then integrate and sum over disjoint target classes

1.1F1F2F3algebra

(Finite target) Let $b$ be a point with $f (b) = a \in C$ and local degree $m \geq 1$ . By [F3], $f - a = (z - b)^{m} h$ with $h (b) \neq 0$ ; the product rule gives $f^{'} = (z - b)^{m - 1} (m h + (z - b) h^{'})$ with $m h (b) \neq 0$ , so $f^{'}$ has a zero of order exactly $m - 1$ at $b$ . Thus $b$ contributes $m - 1$ to $n (t, 0; f^{'})$ and, when $m \geq 2$ , exactly $m - 1$ to $n_{1} (t, a; f)$ ; when $m = 1$ both contributions vanish.

1.2F1F2F4algebra

(Poles) Let $p$ be a pole of order $m \geq 1$ . By [F4], $f = (z - p)^{- m} g$ with $g$ holomorphic and $g (p) \neq 0$ , so $f^{'} = (z - p)^{- m - 1} (- m g + (z - p) g^{'})$ has a pole of order $m + 1$ and no zero at $p$ . Hence $p$ contributes $m$ to $n (t, \infty; f)$ , $2 m - (m + 1) = m - 1$ to $2 n (t, \infty; f) - n (t, \infty; f^{'})$ , and, when $m \geq 2$ , exactly $m - 1$ to $n_{1} (t, \infty; f)$ .

1.3F1algebra

(Disjointness for a target set) Let $A$ be a finite set of distinct sphere targets. For $a \in A$ , $n_{1} (t, a; f)$ is a sum of weights $m_{b} - 1$ over points $b$ with $f (b) = a$ and $m_{b} \geq 2$ ; for distinct $a$ these point sets are disjoint, and each such $b$ is a ramification point of the sphere map with the same local degree $m_{b}$ , so its weight appears in $n_{1} (t, f)$ . Hence $n_{1} (t, a; f) \geq 0$ and $\sum_{a \in A} n_{1} (t, a; f) \leq n_{1} (t, f)$ for every $t > 0$ .

2.1F1F5step 1.1step 1.2algebra

(Weight identity) Every ramification point of the sphere map is either a non-pole point with local degree $m \geq 2$ , where step 1.1 makes the weight $m - 1$ equal to the order of the zero of $f^{'}$ , or a pole of order $m \geq 2$ , handled by step 1.2; conversely every zero of $f^{'}$ is a non-pole point of local degree $ν + 1 \geq 2$ with weight $ν$ . Therefore, for every $t > 0$ , $n_{1} (t, f) = n (t, 0; f^{'}) + 2 n (t, \infty; f) - n (t, \infty; f^{'}),$ both sides being finite sums of nonnegative weights.

3.1F2F5step 2.1algebra

(Integration) The identity of step 2.1 holds at $t = 0$ as well, since $t \mapsto n (t, \cdot)$ is a right-continuous step function and the centre value is included in each term. Multiplying by the centre-regularisation $n (0) \log r + \int_{0}^{r} (\cdot - n (0)) \frac{d t}{t}$ is linear, so $N_{1} (r, f) = N (r, 0; f^{'}) + 2 N (r, \infty; f) - N (r, \infty; f^{'}),$ and all terms are finite by [F5].

4.1F2F5step 1.3algebra∎

(Integrate the inequality) Each ramification point $b \neq 0$ contributes its nonnegative weight times $\log (r / ∣ b ∣)$ when $∣ b ∣ \leq r$ , while a point at $0$ contributes its weight times $\log r$ . For $r \geq 1$ all these coefficients are nonnegative, so the pointwise inclusion of step 1.3 yields $\sum_{a \in A} N_{1} (r, a; f) \leq N_{1} (r, f)$ .

LemmaStatement: Literature-sourcedProof: AI-adaptedaudited 2026-10-02Open item page →

The lemma on the logarithmic derivative

Statement

Assume Countable Choice. Let $f$ be a nonconstant meromorphic function on $C$ and $m_{0} (r, f^{'} / f) = \frac{1}{2 π} \int_{0}^{2 π} \log^{+} ∣ f^{'} (r e^{i t}) / f (r e^{i t}) ∣ d t$ the standard proximity of the logarithmic derivative. Then $m_{0} (r, f^{'} / f) = S (r, f),$ and the same bound holds for the normalized chordal proximity of $f^{'} / f$ to $\infty$ . If $f$ has finite order, then $m_{0} (r, f^{'} / f) = O_{f} (\log r)$ for every sufficiently large $r$ without exceptions; if $f$ is rational, then $m_{0} (r, f^{'} / f) = O_{f} (1)$ for every sufficiently large $r$ .

Facts & Assumptions

Given: A nonconstant meromorphic $f$ on $C$ ; Countable Choice is assumed.

[F1]

$S (r, f)$ denotes an error term bounded by $C (\log^{+} T (r, f) + \log r)$ for all large $r$ outside a measurable set of finite linear measure; the chordal proximity to infinity is $m (r, \infty; g) = \frac{1}{2 π} \int_{0}^{2 π} \frac{1}{2} \log (1 + ∣ g (r e^{i t}) ∣^{2}) d t$ , and $∣ m (r, \infty; g) - m_{0} (r, g) ∣ \leq \frac{1}{2} \log 2$ (Nevanlinna exceptional-radius error notation, Counting, chordal proximity and characteristic).

[F2]

Separated-radius Poisson–Jensen derivative bound: for $0 < α < 1$ and $2 \leq r < R$ , $m_{0} (r, f^{'} / f) \leq C_{f, α} + C_{α} (\log^{+} T (R, f) + \log R + \log^{+} \frac{1}{R - r})$ (Separated-radius Poisson–Jensen derivative bound).

[F3]

Finite-measure growth increment: applied to $u = T (\cdot, f)$ after increasing $r_{0}$ so that $T (r_{0}, f) \geq 1$ , for $ε = 1$ there is a measurable $E$ of finite linear measure with $T (r + T (r, f)^{- 2}, f) < T (r, f) + 1$ for every $r \notin E$ , $r \geq r_{0}$ (Finite-measure growth increment lemma).

[F4]

Ahlfors–Shimizu: $T (r, f) = T_{A S} (r, f) + C_{\infty} (f)$ with $T_{A S}$ nondecreasing and convex in $\log r$ , so $T (\cdot, f)$ is continuous and nondecreasing, and $T (r, f) > 1$ for all sufficiently large $r$ (Ahlfors–Shimizu area form of the characteristic).

[F6]

Order is $ρ (f) = {lim sup}_{r \to \infty} \log T (r, f) / \log r$ (Order and lower order from the Nevanlinna characteristic). If $ρ (f) < \infty$ , then for every $η > 0$ one has $T (r, f) \leq r^{ρ (f) + η}$ for all sufficiently large $r$ , by the definition of the upper limit. Consequently $f$ has finite order if and only if $\log^{+} T (r, f) = O (\log r)$ ; a bound $T (r, f) \leq r^{K}$ eventually yields only $ρ (f) \leq K$ .

[F7]

Every nonconstant complex polynomial has a complex root (Fundamental theorem of algebra by Liouville's theorem); repeated division by the corresponding linear factor gives a factorization into linear terms.

Proof

technique · apply the separated-radius derivative bound at $R=2r$ in finite order and at the Borel-increment radius $R=r+T^{-2}$ in infinite order, then handle rational functions by an explicit partial-fraction estimate

1.1F1algebra

(Reduction to the standard proximity) The two proximities differ pointwise by at most $\frac{1}{2} \log 2$ , so a bound of the form $C (\log^{+} T (r, f) + \log r)$ for $m_{0}$ transfers to $m (r, \infty; f^{'} / f)$ with the constant enlarged by $\frac{1}{2} \log 2$ , and conversely; it suffices to bound $m_{0}$ .

1.2F2F6algebra

(Finite order, all radii) Let $f$ have finite order. Apply [F2] with $α = \frac{1}{2}$ and $R = 2 r$ for $r \geq 2$ : $\log^{+} T (2 r, f) = O_{f} (\log r)$ by [F6], $\log R = \log 2 + \log r$ , and $\log^{+} \frac{1}{R - r} = \log^{+} \frac{1}{r} = 0$ . Hence $m_{0} (r, f^{'} / f) \leq C_{f} + C \log r = O_{f} (\log r)$ for every $r \geq 2$ , with no exceptional set.

1.3F3F4algebra

(Infinite order, off a finite-measure set) Let $f$ have infinite order. By [F4] the function $T (\cdot, f)$ is continuous, nondecreasing and (for nonconstant $f$ ) unbounded, so [F3] applies with $ε = 1$ : there is a measurable $E$ of finite linear measure and $r_{0}$ with $T (r, f) > 1$ and $T (r + T (r, f)^{- 2}, f) < T (r, f) + 1$ for every $r \geq r_{0}$ , $r \notin E$ . Put $R : = r + T (r, f)^{- 2}$ , so $r < R \leq 2 r$ and $\log^{+} \frac{1}{R - r} = 2 \log^{+} T (r, f)$ .

1.4F1F7algebra

(Rational case, all large radii) Let $f = P / Q$ with coprime polynomials. By [F7], factor the nonconstant polynomials into linear terms; the product rule gives $P^{'} / P = \sum_{j} m_{j} / (z - ζ_{j})$ and $Q^{'} / Q = \sum_{k} n_{k} / (z - ξ_{k})$ , with an empty sum for a constant polynomial. At least one polynomial is nonconstant, so the finite union of their root sets is nonempty. For $r \geq \max {2, 2 ∣ ζ_{j} ∣, 2 ∣ ξ_{k} ∣}$ each denominator satisfies $∣ z - ζ_{j} ∣ \geq r / 2$ on $∣ z ∣ = r$ , so $∣ f^{'} / f ∣ \leq 2 (\deg P + \deg Q) / r$ there. Consequently $m_{0} (r, f^{'} / f) \leq \log^{+} (2 (\deg P + \deg Q) / r) = O_{f} (1)$ at every sufficiently large radius, without exceptions.

2.1F2step 1.3algebra

(Infinite order, estimate) For $r \geq r_{0}$ , $r \notin E$ , [F2] with $α = \frac{1}{2}$ gives $m_{0} (r, f^{'} / f) \leq C_{f} + C (\log^{+} T (R, f) + \log R + 2 \log^{+} T (r, f))$ ; here $\log^{+} T (R, f) \leq \log^{+} (T (r, f) + 1) \leq \log^{+} T (r, f) + 1$ and $\log R \leq \log r + \log 2$ . Hence $m_{0} (r, f^{'} / f) \leq C_{f}^{'} + C^{'} (\log^{+} T (r, f) + \log r)$ for all $r \notin E$ .

3.1F1step 1.1step 1.2step 2.1

(The $S$ statement) Combining steps 1.2 and 1.3 (the finite-order case has $E = \emptyset$ ), $m_{0} (r, f^{'} / f) = S (r, f)$ in the sense of [F1]: in the infinite-order case the exceptional set has finite linear measure, in the finite-order case the bound holds at every sufficiently large radius. By step 1.1 the chordal proximity obeys the same bound.

4.1step 3.1step 1.4∎

(Conclusion) A nonconstant meromorphic function is either rational, with $m_{0} (r, f^{'} / f) = O_{f} (1)$ at all large radii, or transcendental, of finite or infinite order, with $m_{0} (r, f^{'} / f) = S (r, f)$ and the stated all-radius $O_{f} (\log r)$ refinement in the finite-order case.

LemmaStatement: Literature-sourcedProof: AI-adaptedaudited 2026-10-02Open item page →

Transcendental characteristic dominates logarithmic growth

Statement

Let $f$ be a nonconstant meromorphic function on $C$ . If $f$ is transcendental, then $\frac{T (r, f)}{\log r} ⟶ + \infty (r \to \infty) .$ Consequently, off the exceptional set belonging to any occurrence of $S (r, f)$ , the right-hand side $C (\log^{+} T (r, f) + \log r)$ is $o (T (r, f))$ .

If $f$ is rational of degree $d \geq 1$ , then $T (r, f) = d \log r + O (1)$ , and this $O (1)$ term is $o (T (r, f))$ .

Facts & Assumptions

Given: A nonconstant meromorphic function $f$ on $C$ , with chordal characteristic $T (r, f)$ as in Counting, chordal proximity and characteristic.

[F1]

Ahlfors–Shimizu: $T (r, f) = T_{A S} (r, f) + C_{\infty} (f)$ for a constant $C_{\infty} (f)$ , where $T_{A S}$ is finite and nondecreasing in $r$ and convex as a function of $\log r$ (Ahlfors–Shimizu area form of the characteristic).

[F2]

$f$ is rational if and only if $T (r, f) = O (\log r)$ ; more precisely, if $f$ is rational of degree $d \geq 1$ , then $T (r, f) = d \log r + O (1)$ (Rational functions are exactly those with logarithmic characteristic).

[F3]

$T$ is nondecreasing, and $T (r, f) > 1$ for all sufficiently large $r$ ; the characteristic is finite for every $r > 0$ (Counting, chordal proximity and characteristic).

Proof

technique · shift the convex Ahlfors–Shimizu potential to the logarithmic variable; a bounded ratio on an unbounded sequence and the convexity chord bound force $T=O(\log r)$, which the rational characterization converts into a contradiction with transcendence

1.1F1F3construct

Put $u (x) : = T (e^{x}, f)$ for $x \in R$ . By [F1], $u (x) - C_{\infty} (f)$ is convex and nondecreasing in $x$ ; hence $u$ itself is convex and nondecreasing. By [F3], $u (x) > 1$ for all sufficiently large $x$ .

1.2F2F3algebra

Since $T$ is nondecreasing by [F3], the limit $L : = \lim_{r \to \infty} T (r, f)$ exists in $(0, + \infty]$ . If $L < \infty$ , then $T (r, f) = O (1) = O (\log r)$ , so [F2] would make $f$ rational, contrary to transcendence; hence $L = + \infty$ , that is, $T (r, f) \to \infty$ .

2.1step 1.1algebra

(Convexity chord bound) Put $x_{0} : = 1$ . By convexity of $u$ from step 1.1, for all $x_{0} \leq x \leq y$ , $u (x) \leq u (x_{0}) + \frac{x - x_{0}}{y - x_{0}} (u (y) - u (x_{0})) .$

3.1step 1.1step 2.1algebra

Assume for contradiction that ${lim inf}_{r \to \infty} T (r, f) / \log r < \infty$ . Then there are a constant $C < \infty$ and a sequence $x_{n} \to + \infty$ with $u (x_{n}) \leq C x_{n}$ for every $n$ . Discard finitely many terms so that $x_{n} \geq 2 x_{0}$ for all $n$ ; applying the chord bound of step 2.1 with $y = x_{n}$ to each $x \in [x_{0}, x_{n}]$ gives $u (x) \leq u (x_{0}) + C x_{n} \frac{x - x_{0}}{x_{n} - x_{0}} \leq u (x_{0}) + 2 C (x - x_{0}),$ because $x_{n} \geq 2 x_{0}$ gives $x_{n} / (x_{n} - x_{0}) \leq 2$ . Thus $T (e^{x}, f) = u (x) \leq C^{'} x$ for all $x \geq 1$ , i.e. $T (r, f) = O (\log r)$ .

4.1F2step 3.1discharge-contradiction

By [F2] the bound $T (r, f) = O (\log r)$ makes $f$ rational, contradicting the hypothesis. Therefore ${lim inf}_{r \to \infty} T (r, f) / \log r = + \infty$ , which for a nonnegative function is the assertion $T (r, f) / \log r \to + \infty$ .

5.1step 1.2step 4.1algebra

By step 1.2, $T (r, f) \to \infty$ , so $\log^{+} T (r, f) = o (T (r, f))$ ; by step 4.1, $\log r = o (T (r, f))$ . Hence $\log^{+} T (r, f) + \log r = o (T (r, f))$ : for every $ε > 0$ the inequality $C (\log^{+} T (r, f) + \log r) \leq ε T (r, f)$ holds for all sufficiently large $r$ . In particular this applies to the right-hand side of any occurrence of $S (r, f)$ at every nonexceptional large radius.

6.1F2algebra∎

If $f$ is rational of degree $d \geq 1$ , then [F2] gives $T (r, f) = d \log r + O (1) \geq \frac{d}{2} \log r$ for all large $r$ , so $T (r, f) \to \infty$ and $O (1) = o (T (r, f))$ .

TheoremStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-6.1-sol)audited 2026-10-02Open item page →

Nevanlinna Second Main Theorem with ramification and truncation

Statement

Assume Countable Choice. Let $f$ be a nonconstant meromorphic function on $C$ and let $a_{1}, \dots, a_{q}$ be distinct sphere values with $q \geq 3$ . Then, outside a set of finite linear measure, $\sum_{j = 1}^{q} m (r, a_{j}; f) + N_{1} (r, f) \leq 2 T (r, f) + S (r, f),$ equivalently $(q - 2) T (r, f) \leq \sum_{j = 1}^{q} N (r, a_{j}; f) - N_{1} (r, f) + S (r, f),$ and consequently $(q - 2) T (r, f) \leq \sum_{j = 1}^{q} \overset{ˉ}{N} (r, a_{j}; f) + S (r, f) .$ If $f$ has finite order, the error terms are $O_{f} (\log r)$ for every sufficiently large $r$ without exception; if $f$ is rational, they are $O_{f} (1)$ for every sufficiently large $r$ .

Facts & Assumptions

Given: A nonconstant meromorphic $f$ on $C$ , distinct sphere values $a_{1}, \dots, a_{q}$ with $q \geq 3$ ; Countable Choice is assumed.

[F1]

The proximity $m (r, a; g)$ is the mean of $\log \frac{1}{δ (g (r e^{i t}), a)}$ , the standard proximity $\frac{1}{2 π} \int_{0}^{2 π} \log^{+} ∣ g ∣ d t$ differs from $m (r, \infty; g)$ by at most $\frac{1}{2} \log 2$ , and $T = m (\cdot, \infty) + N (\cdot, \infty)$ ; $N$ is the centre-regularized count (Counting, chordal proximity and characteristic, Nevanlinna exceptional-radius error notation).

[F2]

First Main Theorem: $m (r, a; g) + N (r, a; g) = T (r, g) + C (g, a)$ with a constant independent of $r$ (Nevanlinna’s First Main Theorem with exact centre constant).

[F3]

Characteristic laws: $T (r, g h) \leq T (r, g) + T (r, h) + O (1)$ , $T (r, g + h) \leq T (r, g) + T (r, h) + O (1)$ , $T (r, 1 / h) = T (r, h) + O_{h} (1)$ as $r \to \infty$ (Elementary characteristic laws and fixed rational composition).

[F4]

Logarithmic-derivative lemma: $m_{0} (r, g^{'} / g) = S (r, g)$ for nonconstant meromorphic $g$ , with $O_{g} (\log r)$ at all large radii when $g$ has finite order and $O_{g} (1)$ at all large radii when $g$ is rational; the chordal proximity obeys the same bounds (The lemma on the logarithmic derivative).

[F5]

Ramification identity: $N_{1} (r, g) = N (r, 0; g^{'}) + 2 N (r, \infty; g) - N (r, \infty; g^{'})$ for every $r > 0$ , and for every finite set of distinct targets $A$ , $\sum_{a \in A} N_{1} (r, a; g) \leq N_{1} (r, g)$ when $r \geq 1$ (Ramification count from the derivative divisor).

[F6]

$N (r, a; g) = \overset{ˉ}{N} (r, a; g) + N_{1} (r, a; g)$ , with $0 \leq N_{1} (r, a; g) \leq N (r, a; g)$ for $r \geq 1$ (Truncated value and ramification counts).

[F7]

$S (r, g)$ denotes a term bounded off a set of finite linear measure by $C (\log^{+} T (r, g) + \log r)$ , with $C$ and the threshold belonging to the occurrence; finitely many occurrences may share the union of their exceptional sets (Nevanlinna exceptional-radius error notation).

Proof

technique · separate the targets by a Möbius substitution, dominate the proximity sum by the proximity of $H=\sum_j1/(f-a_j)$, estimate $H$ through the logarithmic derivatives $f'/(f-a_j)$, and convert the derivative counts into $N_1$ by the ramification identity

1.1choosealgebra

(Reduction to finite targets) Among the $q + 1$ distinct sphere points $0, 1, \dots, q$ at most $q$ belong to ${a_{1}, \dots, a_{q}}$ ; let $m$ be the least one that does not, so $m \neq \infty$ , and put $g : = 1 / (f - m)$ . Then $g$ is nonconstant meromorphic. For finite $a_{j}$ set $a_{j}^{'} : = 1 / (a_{j} - m)$ , and for $a_{j} = \infty$ set $a_{j}^{'} : = 0$ ; these are distinct finite values.

1.2F1F6algebra

(Local computation for the substitution) The Möbius map $w \mapsto 1 / (w - m)$ has local degree one on the sphere, so composition preserves every local degree and ramification multiplicity of $f$ . For each finite target $a_{j}$ , the identity $g - a_{j}^{'} = \frac{a_{j} - f}{(f - m) (a_{j} - m)}$ shows that a zero of $g - a_{j}^{'}$ occurs exactly at $f = a_{j}$ with the same order. If $a_{j} = \infty$ , then $a_{j}^{'} = 0$ and $g = 1 / (f - m)$ has a zero of order $t$ exactly where $f$ has a pole of order $t$ . Thus the target counting functions agree, $N (r, a_{j}^{'}; g) = N (r, a_{j}; f)$ for every sphere target, and the preserved ramification multiplicities give $N_{1} (r, g) = N_{1} (r, f)$ .

1.3F1constructalgebra

(Finite-target setup) Henceforth $a_{1}, \dots, a_{q}$ are finite and distinct; put $δ : = \min_{i < j} ∣ a_{i} - a_{j} ∣ > 0$ and $H : = \sum_{j = 1}^{q} 1 / (f - a_{j})$ . For each fixed finite $a$ , the chordal proximity $m (r, a; f)$ differs from $m_{0} (r, 1 / (f - a))$ by at most a constant depending on $a$ : writing $w = f - a$ , the ratio $\sqrt{1 + ∣ w + a ∣^{2}} / \max (1, ∣ w ∣)$ is bounded above and below by positive constants depending only on $a$ . Thus the finite number of conversions below contributes only $O_{a_{1}, \dots, a_{q}} (1)$ .

1.4choosealgebra

(Target separation) At every point $z$ at most one index $j$ satisfies $∣ f (z) - a_{j} ∣ < δ / 2$ , since two such indices would give $∣ a_{i} - a_{j} ∣ < δ$ ; write $u_{j} : = 1 / (f (z) - a_{j})$ and $M : = \max_{j} ∣ u_{j} ∣ = ∣ u_{j_{*}} ∣$ . If $M \leq \max {1, 4 (q - 1) / δ}$ , then $\sum_{j} \log^{+} ∣ u_{j} ∣ \leq q \log^{+} \max {1, 4 (q - 1) / δ} \leq \log^{+} ∣ H (z) ∣ + q \log^{+} (4 (q - 1) / δ)$ . If $M > \max {1, 4 (q - 1) / δ}$ , then $∣ f (z) - a_{j_{*}} ∣ < δ / 2$ , so $∣ u_{j} ∣ \leq 2 / δ < M / 2$ for every $j \neq j_{*}$ , whence $∣ H (z) ∣ \geq M - \sum_{j \neq j_{*}} ∣ u_{j} ∣ > M / 2$ and $\sum_{j} \log^{+} ∣ u_{j} ∣ \leq \log M + (q - 1) \log^{+} (2 / δ) \leq \log^{+} ∣ H (z) ∣ + \log 2 + (q - 1) \log^{+} (2 / δ)$ . In both cases $\sum_{j = 1}^{q} \log^{+} ∣ \frac{1}{f (z) - a_{j}} ∣ \leq \log^{+} ∣ H (z) ∣ + C_{q, δ}$ with $C_{q, δ} : = \log 2 + \max {q \log^{+} (4 (q - 1) / δ), (q - 1) \log^{+} (2 / δ)}$ .

1.5algebra

(Reduction to logarithmic derivatives) Since $H = (f^{'} H) \cdot (1 / f^{'})$ and $f^{'} H = \sum_{j} f^{'} / (f - a_{j})$ , the pointwise inequalities $\log^{+} ∣ u v ∣ \leq \log^{+} ∣ u ∣ + \log^{+} ∣ v ∣$ and $\log^{+} ∣ \sum_{j = 1}^{q} u_{j} ∣ \leq \sum_{j = 1}^{q} \log^{+} ∣ u_{j} ∣ + \log q$ give $m (r, \infty; H) \leq m (r, \infty; 1 / f^{'}) + \sum_{j = 1}^{q} m (r, \infty; f^{'} / (f - a_{j})) + \log q$ for every $r > 0$ .

1.6F1F2F5algebra

(The term $m (1 / f^{'}) + N_{1}$ ) Since $f$ is nonconstant, $f^{'} \equiv̸ 0$ . If $f^{'}$ is nonconstant, [F2] gives $m (r, 0; f^{'}) = T (r, f^{'}) - N (r, 0; f^{'}) + O_{f} (1)$ ; if $f^{'} = c \neq 0$ is constant, the same relation follows directly from the definitions, since $N (r, 0; f^{'}) = 0$ and $m (r, 0; c) = T (r, c) - \log ∣ c ∣$ . In either case [F5] and $T (r, f^{'}) = m (r, \infty; f^{'}) + N (r, \infty; f^{'})$ give $m (r, 0; f^{'}) + N_{1} (r, f) = m (r, \infty; f^{'}) + 2 N (r, \infty; f) + O_{f} (1),$ using $N_{1} (r, f) = N (r, 0; f^{'}) + 2 N (r, \infty; f) - N (r, \infty; f^{'})$ .

2.1F2F3step 1.2suffices

(Characteristic transfer) $T (r, g) = T (r, 1 / (f - m)) = T (r, f - m) + O_{f} (1) = T (r, f) + O_{f} (1)$ by [F3]; consequently by [F2], $m (r, a_{j}^{'}; g) = T (r, g) - N (r, a_{j}^{'}; g) + C (g, a_{j}^{'}) = T (r, f) - N (r, a_{j}; f) + O_{f} (1) = m (r, a_{j}; f) + O_{f} (1)$ , and the finite sum of $O_{f} (1)$ errors is absorbed into $S (r, f)$ for all large $r$ ; hence it suffices to prove the inequalities for finite distinct targets.

2.2F1step 1.3step 1.4algebra

(Means) Taking angular means of step 1.4 and using the integrability of the logarithmic singularities and the finite-target comparison of step 1.3 gives $\sum_{j = 1}^{q} m (r, a_{j}; f) \leq m (r, \infty; H) + C_{a_{1}, \dots, a_{q}}$ for every $r > 0$ .

3.1F4F7step 2.2step 1.5algebra

(Logarithmic derivative of the shifted functions) For each $j$ the function $f - a_{j}$ is nonconstant meromorphic and $(f - a_{j})^{'} / (f - a_{j}) = f^{'} / (f - a_{j})$ , so [F4] gives $m (r, \infty; f^{'} / (f - a_{j})) = S (r, f - a_{j})$ ; since $T (r, f - a_{j}) \leq T (r, f) + O_{f} (1)$ by [F3], we have $S (r, f - a_{j}) \leq S (r, f) + O_{f} (1)$ , and likewise $m (r, f^{'} / f) = S (r, f)$ ; taking the union of the exceptional sets of these $q + 1$ occurrences gives a set $E$ of finite linear measure such that $\sum_{j = 1}^{q} m (r, a_{j}; f) \leq m (r, \infty; 1 / f^{'}) + q S (r, f) + O_{f} (1)$ for every $r \notin E$ .

4.1F4step 3.1algebra

(Bounding $m (f^{'})$ ) The pointwise bound $\log^{+} ∣ f^{'} ∣ \leq \log^{+} ∣ f ∣ + \log^{+} ∣ f^{'} / f ∣$ gives $m (r, \infty; f^{'}) \leq m (r, \infty; f) + m (r, f^{'} / f) \leq m (r, \infty; f) + S (r, f)$ for $r \notin E$ .

5.1step 3.1step 1.6step 4.1algebra

(Conclusion of the finite-target case) Combining steps 3.1, 1.6 and 4.1 for $r \notin E$ gives $\sum_{j} m (r, a_{j}; f) + N_{1} (r, f) \leq m (r, \infty; f) + 2 N (r, \infty; f) + q S (r, f) + O_{f} (1) = T (r, f) + N (r, \infty; f) + q S (r, f) + O_{f} (1) = 2 T (r, f) - m (r, \infty; f) + q S (r, f) + O_{f} (1) \leq 2 T (r, f) + q S (r, f) + O_{f} (1)$ , and the constant is absorbed into the error term, so $\sum_{j = 1}^{q} m (r, a_{j}; f) + N_{1} (r, f) \leq 2 T (r, f) + S (r, f)$ outside $E$ .

6.1F2F5F6F7step 5.1algebra

(Equivalent forms) By [F2], $\sum_{j = 1}^{q} m (r, a_{j}; f) = q T (r, f) - \sum_{j = 1}^{q} N (r, a_{j}; f) + O_{f} (1)$ ; substituting into step 5.1 and absorbing $O_{f} (1)$ yields $(q - 2) T (r, f) \leq \sum_{j = 1}^{q} N (r, a_{j}; f) - N_{1} (r, f) + S (r, f)$ outside $E$ . Conversely, rearranging this displayed bound using the same equality from [F2] recovers step 5.1 up to $O_{f} (1)$ ; [F7] absorbs that bounded term into an error of the same class, enlarging the finite-measure exceptional set if needed, so the first two displayed inequalities are equivalent. Moreover $N (r, a_{j}; f) = \overset{ˉ}{N} (r, a_{j}; f) + N_{1} (r, a_{j}; f)$ and $\sum_{j} N_{1} (r, a_{j}; f) \leq N_{1} (r, f)$ by [F5] and [F6], so $\sum_{j} N (r, a_{j}; f) - N_{1} (r, f) \leq \sum_{j} \overset{ˉ}{N} (r, a_{j}; f)$ and $(q - 2) T (r, f) \leq \sum_{j = 1}^{q} \overset{ˉ}{N} (r, a_{j}; f) + S (r, f)$ outside $E$ .

7.1F2F3F4step 3.1step 6.1

(Refinements) If $f$ has finite order then $g = 1 / (f - m)$ and every $f - a_{j}$ have finite order with characteristics $T (r, f) + O_{f} (1)$ , so the errors in step 3.1 are $O_{f} (\log r)$ at every large radius by [F4], and all other errors above are $O_{f} (1)$ by [F2] and [F3]; hence the inequalities hold with $O_{f} (\log r)$ at every sufficiently large $r$ , with no exceptional set in this case. If $f$ is rational the same argument gives $O_{f} (1)$ at every sufficiently large $r$ , again with no exceptional set.

8.1step 1.1step 1.2step 2.1step 6.1step 7.1∎

(Unwinding) Applying the finite-target argument of steps 1.3–7.1 to the transform of step 1.1 and transferring back by steps 1.2 and 2.1 proves the three displayed inequalities for the original targets, including the case in which some $a_{j}$ equals $\infty$ ; the finite union $E$ of the exceptional sets of the finitely many logarithmic-derivative applications still has finite linear measure, and all conversion constants are absorbed into $S (r, f)$ .

DefinitionDefinition: Literature-sourcedProof: AI-adaptedaudited 2026-10-02Open item page →

Nevanlinna deficiency and ramification index

Definition

Let $f$ be a nonconstant meromorphic function on $C$ . For a sphere target $a \in \hat{C}$ , the deficiency of $a$ is $δ (a, f) : = {lim inf}_{r \to \infty} \frac{m (r, a; f)}{T (r, f)} = 1 - {lim sup}_{r \to \infty} \frac{N (r, a; f)}{T (r, f)},$ and the ramification index of $a$ is $ε (a, f) : = {lim inf}_{r \to \infty} \frac{N_{1} (r, a; f)}{T (r, f)},$ with $N_{1} (r, a; f)$ the integrated ramification count at target $a$ , weighting each $a$ -point by its local degree minus one, as in Truncated value and ramification counts. Both indices are well-defined numbers in $[0, 1]$ (proved below).

For a set $S \subseteq \hat{C}$ of targets, the total deficiency sum is defined without choosing an enumeration by $\sum_{a \in S} (δ (a, f) + ε (a, f)) : = \sup {\sum_{a \in A} (δ (a, f) + ε (a, f)) : A \subseteq S, A finite} .$ For finite $S$ this is the ordinary finite sum. No countability of $S$ and no enumeration of $S$ is assumed.

Facts & Assumptions

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

[F1]

$m (r, a; f)$ , $N (r, a; f)$ and $T (r, f)$ are finite for every $r > 0$ , $T$ is nondecreasing, and $T (r, f) > 1$ for all sufficiently large $r$ (Counting, chordal proximity and characteristic).

[F2]

$m (r, a; f) + N (r, a; f) = T (r, f) + C (f, a)$ with a constant $C (f, a)$ independent of $r$ ; in particular $m \geq 0$ and $N \leq T + C (f, a)$ (Nevanlinna’s First Main Theorem with exact centre constant). Integrated counts are nonnegative for $r \geq 1$ ; their centre term can be negative when $r < 1$ .

[F3]

$N (r, a; f) = \overset{ˉ}{N} (r, a; f) + N_{1} (r, a; f)$ , and $0 \leq N_{1} (r, a; f) \leq N (r, a; f)$ for $r \geq 1$ , with $N_{1} (r, a; f)$ the integrated count of $a$ -points weighted by local degree minus one (Truncated value and ramification counts).

[F4]

If $f$ is transcendental then $T (r, f) / \log r \to \infty$ , and if $f$ is rational of degree $d \geq 1$ then $T (r, f) = d \log r + O (1)$ ; in both cases $T (r, f) \to \infty$ (Transcendental characteristic dominates logarithmic growth).

Proof

technique · divide the First Main Theorem by $T$ and use that $T\to\infty$, then bound nonnegative numerators by $T$

1.1F4

$T (r, f) \to \infty$ : this is [F4] in the transcendental case, and in the rational case of degree $d \geq 1$ the formula $T (r, f) = d \log r + O (1)$ diverges.

2.1F2step 1.1algebra

Since $C (f, a)$ is a constant and $T (r, f) \to \infty$ , [F2] gives $\frac{m}{T} = 1 + \frac{C (f, a)}{T} - \frac{N}{T} = 1 - \frac{N}{T} + o (1)$ , hence ${lim inf}_{r} \frac{m}{T} = {lim inf}_{r} (1 - \frac{N}{T}) = 1 - {lim sup}_{r} \frac{N}{T}$ ; the two expressions for $δ (a, f)$ agree.

2.2F1F2step 1.1algebra

$δ (a, f) \in [0, 1]$ : from [F2], $0 \leq m \leq T + C (f, a)$ and $0 \leq N \leq T + C (f, a)$ for $r \geq 1$ ; with $T (r, f) > 0$ for all large $r$ by [F1], dividing by $T$ and taking limits gives $0 \leq lim inf \frac{m}{T}$ and $lim sup \frac{N}{T} \leq 1$ .

3.1F3step 2.2algebra

$ε (a, f) \in [0, 1]$ : for $r \geq 1$ , [F3] gives $0 \leq N_{1} (r, a; f) \leq N (r, a; f) \leq T (r, f) + C (f, a)$ ; dividing by $T$ and taking the lower limit gives $0 \leq ε (a, f) \leq lim sup \frac{N}{T} \leq 1$ .

3.2F2step 2.1algebra

If $f$ omits $a$ , then $n (t, a; f) = 0$ for every $t$ , so $N (r, a; f) \equiv 0$ and $δ (a, f) = 1 - lim sup 0 = 1$ ; also $m (r, a; f) = T (r, f) + C (f, a)$ by [F2].

4.1given∎

The sum convention is well posed as an extended nonnegative supremum: the collection is nonempty because it contains the empty subsum $0$ , and if $S$ is finite the supremum is attained at $A = S$ . No enumeration or selection is used.

TheoremStatement: Literature-sourcedProof: AI-adaptedaudited 2026-10-02Open item page →

Nevanlinna deficiency and ramification defect relations

Statement

Assume Countable Choice. For every nonconstant meromorphic function $f$ on $C$ , $\sum_{a \in \hat{C}} (δ (a, f) + ε (a, f)) \leq 2, and hence \sum_{a \in \hat{C}} δ (a, f) \leq 2.$ Also $δ (a, f) + ε (a, f) \leq 1$ for every $a \in \hat{C}$ , and the set of targets at which either index is positive is at most countable. Sums over $\hat{C}$ mean suprema of finite subsums.

Facts & Assumptions

Given: A nonconstant meromorphic function $f$ on $C$ ; Countable Choice is assumed (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

Deficiency and ramification index: for every sphere target $a$ , $δ (a, f) = {lim inf}_{r \to \infty} \frac{m (r, a; f)}{T (r, f)} = 1 - {lim sup}_{r \to \infty} \frac{N (r, a; f)}{T (r, f)}$ and $ε (a, f) = {lim inf}_{r \to \infty} \frac{N_{1} (r, a; f)}{T (r, f)}$ , both in $[0, 1]$ ; the target sum is the supremum of finite subsums, and the identities rest on the First Main Theorem $m (r, a; f) + N (r, a; f) = T (r, f) + C (f, a)$ with $C (f, a)$ independent of $r$ (Nevanlinna deficiency and ramification index, Nevanlinna’s First Main Theorem with exact centre constant).

[F2]

Second Main Theorem: for every finite set $A$ of distinct sphere targets with $∣ A ∣ \geq 3$ , $\sum_{a \in A} m (r, a; f) + N_{1} (r, f) \leq 2 T (r, f) + S (r, f)$ outside a set of finite linear measure, where $S (r, f) \leq C (\log^{+} T (r, f) + \log r)$ off that set; when $f$ is rational the error is $O_{f} (1)$ at every sufficiently large radius. Moreover for every finite set $A$ of distinct sphere targets and $r \geq 1$ , $\sum_{a \in A} N_{1} (r, a; f) \leq N_{1} (r, f)$ (Nevanlinna Second Main Theorem with ramification and truncation, Ramification count from the derivative divisor).

[F3]

Growth separation input: $T (r, f) \to \infty$ , with $T (r, f) / \log r \to \infty$ when $f$ is transcendental and $T (r, f) = d \log r + O (1)$ when $f$ is rational of degree $d \geq 1$ (Transcendental characteristic dominates logarithmic growth).

[F4]

Countable unions: under Countable Choice, a countable union of at most countable sets is at most countable (Countable unions of at most countable sets, assuming ${A C}_{ω}$ ).

Proof

technique · bound each combined index by one, apply the ramified Second Main Theorem to finite target sets, divide by the characteristic and pass to the lower limit using growth separation, take the supremum over finite target sets, and finish the countability clause with a threshold union

1.1F1algebra

(Per-target bound) Since $N_{1} (r, a; f) \leq N (r, a; f)$ and $T (r, f) > 0$ for all large $r$ , $ε (a, f) = {lim inf}_{r} \frac{N_{1} (r, a; f)}{T (r, f)} \leq {lim inf}_{r} \frac{N (r, a; f)}{T (r, f)} \leq {lim sup}_{r} \frac{N (r, a; f)}{T (r, f)} = 1 - δ (a, f)$ , so $δ (a, f) + ε (a, f) \leq 1$ , and both indices are nonnegative by [F1].

1.2F2algebra

(Second Main Theorem bound for finite target sets) Let $A$ be a finite set of distinct sphere targets with $∣ A ∣ \geq 3$ . By [F2], $\sum_{a \in A} m (r, a; f) + N_{1} (r, f) \leq 2 T (r, f) + S (r, f)$ outside a set $E$ of finite linear measure; since $\sum_{a \in A} N_{1} (r, a; f) \leq N_{1} (r, f)$ by [F2], also $\sum_{a \in A} (m (r, a; f) + N_{1} (r, a; f)) \leq 2 T (r, f) + S (r, f)$ outside $E$ .

2.1step 1.1algebra

(Target sets of at most two points) If $∣ A ∣ \leq 2$ then $\sum_{a \in A} (δ (a, f) + ε (a, f)) \leq ∣ A ∣ \leq 2$ by step 1.1, so the asserted bound holds for every finite target set of at most two points.

2.2F1F2F3step 1.2algebra

(Growth separation) If $f$ is transcendental, [F3] gives $T (r, f) / \log r \to \infty$ and $T (r, f) \to \infty$ , so the general error bound in [F2] satisfies $S (r, f) / T (r, f) \to 0$ off $E$ . If $f$ is rational of degree $d \geq 1$ , [F2] supplies the stronger error $O_{f} (1)$ at every large radius, while [F3] gives $T (r, f) = d \log r + O (1) \to \infty$ ; thus this error divided by $T$ also tends to zero.

3.1step 2.1step 1.2step 2.2algebra

(Defect bound for finite target sets) For $∣ A ∣ \geq 3$ , dividing step 1.2 by $T (r, f)$ and using step 2.2 gives $\sum_{a \in A} (\frac{m (r, a; f)}{T (r, f)} + \frac{N_{1} (r, a; f)}{T (r, f)}) \leq 2 + o (1)$ along $r \notin E$ ; since $E$ has finite measure its complement is unbounded, so the lower limit of the left side is at most $2$ . As a finite sum of lower limits is at most the lower limit of the sum, $\sum_{a \in A} (δ (a, f) + ε (a, f)) \leq 2$ ; with step 2.1 this covers every finite target set $A$ .

4.1F1step 3.1algebra

(Supremum over finite sets) By [F1] the total deficiency sum is the supremum of the finite subsums, each of which is at most $2$ by step 3.1, so $\sum_{a} (δ (a, f) + ε (a, f)) \leq 2$ ; since $δ \geq 0$ , also $\sum_{a} δ (a, f) \leq 2$ .

5.1F4step 4.1algebra∎

(The positive set is at most countable) For every integer $k \geq 1$ put $F_{k} = {a \in \hat{C} : δ (a, f) + ε (a, f) > 1 / k}$ ; were $∣ F_{k} ∣ \geq 2 k + 1$ , then the finite subsum over any $2 k + 1$ points of $F_{k}$ would exceed $\frac{2 k + 1}{k} = 2 + \frac{1}{k} > 2$ , contradicting step 4.1, so each $F_{k}$ is finite and hence at most countable. Since $δ + ε \geq 0$ , the set where either index is positive equals $⋃_{k \geq 1} F_{k}$ , a countable union of at most countable sets, which is at most countable by [F4].

LemmaStatement: Literature-sourcedProof: AI-adaptedaudited 2026-10-02Open item page →

Three omitted values force exterior extension

Statement

Let $R > 0$ and let $g$ be meromorphic on $∣ w ∣ > R$ . Suppose there is $R_{1} > R$ such that $g$ omits three distinct values of the Riemann sphere on $∣ w ∣ > R_{1}$ . Then $g$ extends meromorphically across $w = \infty$ : the function $z \mapsto g (1 / z)$ has a meromorphic extension to a neighbourhood of $z = 0$ .

Facts & Assumptions

Given: A radius $R > 0$ , a radius $R_{1} > R$ , and a function $g$ meromorphic on $∣ w ∣ > R$ that omits three distinct sphere values on $∣ w ∣ > R_{1}$ .

[F1]

For any two ordered triples of distinct points of $\hat{C}$ there is a Möbius transformation carrying the first onto the second; in particular a triple can be normalized to $(0, 1, \infty)$ (A unique Möbius transformation carries any ordered triple of distinct sphere points to any other).

[F2]

Every Möbius transformation is a biholomorphism of the Riemann sphere with Möbius inverse, and composition with it preserves meromorphy holomorphically in the sphere charts (Every Möbius transformation is a biholomorphism of the Riemann sphere).

[F3]

Schottky: for all $R^{'} > 0$ , $0 < r < 1$ there is $C (R^{'}, r) > 0$ such that every holomorphic $F : D \to C ∖ {0, 1}$ with $∣ F (0) ∣ \leq R^{'}$ satisfies $∣ F (z) ∣ \leq C (R^{'}, r)$ for $∣ z ∣ \leq r$ (Schottky's theorem).

[F4]

Cauchy estimates on concentric subdiscs: if $f$ is holomorphic on $D (a, S)$ and $∣ f ∣ \leq M$ on $∣ z - a ∣ = R$ , then $∣ f^{(n)} (z) ∣ \leq n! R M / (R - r)^{n + 1}$ for $∣ z - a ∣ \leq r$ , $0 \leq r < R < S$ (Cauchy estimates on a smaller concentric disc).

[F5]

The chordal metric $χ$ on $\hat{C}$ is the Euclidean distance of stereographic images on the unit sphere; it induces the standard topology (The chordal metric on the Riemann sphere, The chordal metric induces the standard topology of the Riemann sphere).

[F6]

$Q^{2}$ is countable and dense in $R^{2}$ , and rational boxes form a countable basis of the topology ( $Q^{n}$ is a countable dense subset of $R^{n}$ , and rational open boxes form a countable basis).

[F7]

Closed boxes in $R^{n}$ are compact, and a subset of $R^{n}$ is compact exactly when it is closed and bounded (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

[F8]

A compact metric space is complete and totally bounded (A compact metric space is complete and totally bounded, and neither implication uses any choice principle).

[F9]

A continuous real-valued function on a nonempty compact metric space attains a maximum and a minimum (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[F10]

Peano recursion: for every set $A$ , $a \in A$ and $f : A \to A$ there is a unique $g : N \to A$ with $g (0) = a$ and $g (σ (n)) = f (g (n))$ (The recursion theorem).

[F11]

A chordally locally uniform limit of meromorphic functions on a plane domain is meromorphic or identically $\infty$ ; if all the approximants are holomorphic, the limit is holomorphic or identically $\infty$ (A chordally locally uniform meromorphic limit is meromorphic or identically infinity).

[F12]

If $Ω$ is a bounded complex domain and $f$ is continuous on $\overline{Ω}$ and holomorphic on $Ω$ , then $∣ f (z) ∣ \leq \max_{\partial Ω} ∣ f ∣$ for $z \in Ω$ (Boundary maximum modulus principle on a bounded domain).

[F13]

A holomorphic function on a punctured disc bounded near the centre has a removable singularity there (Characterizations of removable singularities).

[F14]

On a punctured disc, $a$ is a pole of $f$ if and only if $∣ f (z) ∣ \to \infty$ there, equivalently $1 / f$ extends holomorphically across $a$ and vanishes there (Characterizations of poles).

Proof

technique · reduce the exterior map to a holomorphic function on a punctured disc omitting $0$ and $1$; obtain uniform chordal equicontinuity on a fixed annulus from Schottky's theorem and Cauchy estimates; extract a deterministic diagonal subsequence converging on a dense subset; propagate a bound for the function or its reciprocal along shrinking circles by the maximum modulus principle; conclude with the removable-singularity and pole characterizations

1.1F1F2givenconstruct

Let $v_{1}, v_{2}, v_{3}$ be the three omitted sphere values. By [F1] choose a Möbius transformation $M$ with $M (v_{1}) = 0$ , $M (v_{2}) = 1$ , $M (v_{3}) = \infty$ , and put $h (z) : = M (g (1 / z))$ for $0 < ∣ z ∣ < 1 / R_{1}$ . Since $∣ 1 / z ∣ > R_{1}$ there, $g (1 / z)$ omits $v_{1}, v_{2}, v_{3}$ ; hence $h$ attains neither $\infty$ nor $0, 1$ , so $h$ is holomorphic on $0 < ∣ z ∣ < 1 / R_{1}$ and omits $0$ and $1$ .

1.2givenconstructalgebra

(Local setup) Let $h$ be holomorphic on $0 < ∣ z ∣ < r_{0}$ omitting $0$ and $1$ . Set $ρ : = r_{0} / 8$ , $ρ_{n} : = ρ 2^{- n}$ for $n \in N$ , $A : = {1 / 2 < ∣ ζ ∣ < 2}$ and $h_{n} (ζ) : = h (ρ_{n} ζ)$ for $ζ \in A$ . Since $0 < ρ_{n} ∣ ζ ∣ < 2 ρ = r_{0} / 4 < r_{0}$ for $ζ \in A$ , each $h_{n}$ is holomorphic on $A$ and omits $0$ and $1$ .

1.3F6F7algebra

(Dense set) Put $K : = {3 / 4 \leq ∣ ζ ∣ \leq 5 / 4}$ and let $Q : = (Q + i Q) \cap K$ . Since $Q^{2}$ is countable and dense in $R^{2}$ and $K$ is the closure of its nonempty interior ${3 / 4 < ∣ ζ ∣ < 5 / 4}$ , $Q$ is countable and dense in $K$ ; fix an enumeration $q_{0}, q_{1}, q_{2}, \dots$ of $Q$ .

1.4F5F6algebra

(Dyadic target boxes) Identify the sphere with $S^{2} \subset [- 1, 1]^{3}$ through the stereographic homeomorphism of [F5]. For each $m \geq 0$ the $8^{m}$ half-open dyadic boxes of side $2^{1 - m}$ partition $[- 1, 1]^{3}$ ; order each level lexicographically. Their diameters are $\sqrt{3} \cdot 2^{1 - m} \to 0$ .

2.1F2step 1.1suffices

It suffices to prove the following local claim: a function holomorphic on a punctured disc $0 < ∣ z ∣ < r_{0}$ that omits $0$ and $1$ extends meromorphically at $0$ . Indeed, applying the claim to $h$ produces a meromorphic extension of $h$ at $0$ ; by [F2] the composition $M^{- 1} \circ h$ is then meromorphic at $0$ , and on the punctured disc it equals $g (1 / z)$ , so $z \mapsto g (1 / z)$ is meromorphic near $0$ .

2.2F7step 1.2algebra

(Fixed band) Put $δ : = 1 / 16$ . The set $K$ of step 1.3 is closed and bounded, hence compact by [F7]. If $a \in K$ and $∣ ζ - a ∣ \leq 2 δ = 1 / 8$ , then $5 / 8 \leq ∣ ζ ∣ \leq 11 / 8$ , so $ζ \in A$ ; thus $\overline{D} (a, 2 δ) \subset A$ for every $a \in K$ .

2.3step 1.2algebra

(Center normalization) Fix $a \in K$ and $n \in N$ . If $∣ h_{n} (a) ∣ \leq 2$ put $t : = h_{n}$ ; otherwise put $t : = 1 / h_{n}$ . In both cases $t$ is holomorphic on $A$ , omits $0$ and $1$ , and $∣ t (a) ∣ \leq 2$ : in the first case this is step 1.2; in the second, $h_{n}$ has no zeros, $t = 0$ would force $h_{n} = \infty$ , and $t = 1$ would force $h_{n} = 1$ , while $∣ t (a) ∣ < 1 / 2$ .

2.4F7F8F10step 1.4construct

(Extraction at one point) Let $I \subset N$ be infinite and $q \in K$ . Define $I_{0} : = I$ and, recursively, for $m \geq 0$ : among the finitely many level- $(m + 1)$ dyadic boxes, at least one contains $Σ (h_{i} (q))$ for infinitely many $i \in I_{m}$ ; let $B_{m}$ be the first such box and $I_{m + 1} : = {i \in I_{m} : Σ (h_{i} (q)) \in B_{m}}$ . Let $s (m)$ be the least element of $I_{m}$ with $s (m) > s (m - 1)$ , where $s (- 1) : = - 1$ . Then every $I_{m}$ is infinite and nested, $s$ is strictly increasing with range in $I$ , and the values $Σ (h_{s (m)} (q))$ are eventually inside boxes of diameter tending to $0$ , so they form a Cauchy sequence; being contained in the compact metric space $[- 1, 1]^{3}$ , it converges, and the limit lies in the closed subset $S^{2}$ . Every selection above is a least element in a finite or well-ordered list, so no choice principle is used.

3.1F3step 2.2step 2.3

(Schottky bound) The map $F (ζ) : = t (a + 2 δ ζ)$ is holomorphic on the unit disc and omits $0, 1$ , with $∣ F (0) ∣ = ∣ t (a) ∣ \leq 2$ ; the disc $D (a, 2 δ)$ lies in $A$ by step 2.2. Applying [F3] with center bound $2$ and inner radius $1 / 2$ gives a constant $C_{0} = C (2, 1 / 2)$ , independent of $a$ and $n$ , with $∣ t (ζ) ∣ \leq C_{0}$ for $∣ ζ - a ∣ \leq δ$ .

3.2F10step 2.4construct

(Nested refinements) Let $s_{0}$ be the strictly increasing sequence produced by step 2.4 with $I = N$ and $q = q_{0}$ . Define states $(j, s_{j})$ by recursion [F10], taking $s_{j + 1}$ to be the sequence produced by step 2.4 from $I : = range (s_{j})$ and $q : = q_{j + 1}$ . Then each $s_{j}$ is strictly increasing, $range (s_{j + 1}) \subseteq range (s_{j})$ , and, since $s_{j}$ was extracted at $q_{j}$ , the values $h_{s_{j} (m)} (q_{j})$ converge in the chordal sphere as $m \to \infty$ for every $j$ .

4.1F4step 3.1algebra

(Lipschitz bound for $t$ ) By [F4] applied to $t$ on $D (a, 2 δ)$ with bound $M = C_{0}$ on the circle $∣ ζ - a ∣ = δ$ and $r = δ / 2$ , we get $∣ t^{'} (ζ) ∣ \leq \frac{δ C_{0}}{(δ / 2)^{2}} = \frac{4 C_{0}}{δ}$ for $∣ ζ - a ∣ \leq δ / 2$ . Hence $∣ t (z) - t (w) ∣ \leq \frac{4 C_{0}}{δ} ∣ z - w ∣$ for $z, w \in D (a, δ / 2)$ .

4.2step 3.2algebra

(Diagonal) Put $n_{i} : = s_{i} (i)$ for $i \in N$ . Then $n_{i + 1} = s_{i + 1} (i + 1) > s_{i + 1} (i) \geq s_{i} (i) = n_{i}$ , because $range (s_{i + 1}) \subseteq range (s_{i})$ forces $s_{i + 1} (i) \geq s_{i} (i)$ by induction on the position in the increasing enumeration. Hence $(n_{i})$ is strictly increasing. For fixed $j$ and $i \geq j$ we have $n_{i} \in range (s_{i}) \subseteq range (s_{j})$ , so $(n_{i})_{i \geq j}$ is a strictly increasing sequence of elements of $range (s_{j})$ , i.e. a subsequence of $s_{j}$ ; by step 3.2 the values $h_{n_{i}} (q_{j})$ converge to a point $H (q_{j})$ of the sphere.

5.1F5step 4.1algebra

(Chordal form) For finite $u, v$ the stereographic coordinates give $χ (u, v) = \frac{2 ∣ u - v ∣}{\sqrt{(1 + ∣ u ∣^{2}) (1 + ∣ v ∣^{2})}} \leq 2 ∣ u - v ∣$ , and $χ (1 / u, 1 / v) = χ (u, v)$ for $u, v \neq 0$ : substituting $1 / u, 1 / v$ in the formula clears the factors $∣ u ∣, ∣ v ∣$ . Therefore for $z, w \in D (a, δ / 2)$ , in the notation of step 2.3, $χ (h_{n} (z), h_{n} (w)) = χ (t (z), t (w)) \leq 2 ∣ t (z) - t (w) ∣ \leq \frac{8 C_{0}}{δ} ∣ z - w ∣$ , uniformly in $n$ and $a$ .

6.1step 5.1algebra

(Equicontinuity on $K$ ) For all $z, w \in K$ with $∣ z - w ∣ < δ / 2$ , apply step 5.1 with $a : = z \in K$ and $w \in D (z, δ / 2)$ : $χ (h_{n} (z), h_{n} (w)) \leq \frac{8 C_{0}}{δ} ∣ z - w ∣$ for every $n$ . Thus the family ${h_{n}}$ has the uniform chordal modulus of continuity $ω (s) : = \min {2, \frac{8 C_{0}}{δ} s}$ on $K$ , where the constant $2$ bounds the chordal distance because $χ$ is the chordal length on the unit sphere.

7.1F7F8step 6.1step 4.2

(Uniform convergence on $K$ ) Let $ε > 0$ and choose $η > 0$ with $ω (η) < ε / 3$ . The discs $D (q, η)$ , $q \in Q$ , cover $K$ ; by compactness [F7] a finite subcover exists, and we take the least one in a fixed enumeration of the finite subsets of $Q$ . For each of its finitely many centers $q_{ℓ}$ , step 4.2 gives $N_{ℓ}$ with $χ (h_{n_{i}} (q_{ℓ}), h_{n_{m}} (q_{ℓ})) < ε / 3$ for $i, m \geq N_{ℓ}$ . Let $N : = \max_{ℓ} N_{ℓ}$ . For $z \in K$ choose $ℓ$ with $∣ z - q_{ℓ} ∣ < η$ ; then for $i, m \geq N$ , $χ (h_{n_{i}} (z), h_{n_{m}} (z)) \leq χ (h_{n_{i}} (z), h_{n_{i}} (q_{ℓ})) + χ (h_{n_{i}} (q_{ℓ}), h_{n_{m}} (q_{ℓ})) + χ (h_{n_{m}} (q_{ℓ}), h_{n_{m}} (z)) < ε$ . Thus $(h_{n_{i}})$ is uniformly Cauchy on $K$ , and since the chordal sphere is compact, hence complete [F8], it converges uniformly on $K$ to a map $H : K \to \hat{C}$ .

8.1F11step 7.1

(Limit on the annulus) The chosen functions $h_{n_{i}}$ are holomorphic on the annulus $U : = {3 / 4 < ∣ ζ ∣ < 5 / 4} \subset A$ and converge chordally uniformly on $U$ by step 7.1. By [F11] the limit $H : U \to \hat{C}$ is meromorphic or identically $\infty$ ; since all approximants are holomorphic, $H$ is holomorphic on $U$ or identically $\infty$ .

8.2F5F9step 7.1algebra

(Finite case: a bound on the circle) Suppose $H$ is holomorphic on $U$ . By [F9] applied to $∣ H ∣$ on the compact circle ${∣ ζ ∣ = 1} \subset U$ there is $M$ with $∣ H (ζ) ∣ \leq M$ there, and the continuous positive function $ζ \mapsto χ (H (ζ), \infty)$ attains a positive minimum. So the image of the circle is a compact subset of $C$ and there is $c_{0} > 0$ with $χ (H (ζ), \infty) \geq c_{0}$ on it. Uniform chordal convergence (step 7.1) then gives, for all large $i$ , $χ (h_{n_{i}} (ζ), H (ζ)) < c_{0} / 2$ on $∣ ζ ∣ = 1$ , so $χ (h_{n_{i}} (ζ), \infty) \geq c_{0} / 2$ there; writing $χ (u, \infty) = 2 / \sqrt{1 + ∣ u ∣^{2}}$ , this means $∣ h_{n_{i}} (ζ) ∣ \leq M^{'}$ on $∣ ζ ∣ = 1$ for a constant $M^{'}$ independent of $i$ . Since $h_{n_{i}} (ζ) = h (ρ_{n_{i}} ζ)$ , the function $h$ satisfies $∣ h ∣ \leq M^{'}$ on each circle $∣ z ∣ = ρ_{n_{i}}$ with $i$ large.

8.3F5step 7.1algebra

(Infinite case: a bound for the reciprocal) Suppose $H \equiv \infty$ on $U$ . Uniform chordal convergence to $\infty$ gives, for all large $i$ , $χ (h_{n_{i}} (ζ), \infty) < \sqrt{2}$ on $∣ ζ ∣ = 1$ . Since $χ (u, \infty) = 2 / \sqrt{1 + ∣ u ∣^{2}}$ , this is exactly $∣ h_{n_{i}} (ζ) ∣ > 1$ , that is $∣ 1 / h (ρ_{n_{i}} ζ) ∣ < 1$ , on the circle $∣ ζ ∣ = 1$ . As $h$ omits $0$ , the reciprocal $1 / h$ is holomorphic on the punctured disc, and $∣ 1 / h ∣ \leq 1$ on each circle $∣ z ∣ = ρ_{n_{i}}$ with $i$ large.

9.1F12step 8.2algebra

(Propagation, finite case) For each large $i$ , the function $h$ is continuous on the closed annulus $ρ_{n_{i + 1}} \leq ∣ z ∣ \leq ρ_{n_{i}}$ and holomorphic in its interior, with $∣ h ∣ \leq M^{'}$ on both boundary circles by step 8.2; [F12] gives $∣ h ∣ \leq M^{'}$ throughout that annulus. Consecutive retained annuli cover ${0 < ∣ z ∣ \leq ρ_{n_{i_{0}}}}$ for a suitable $i_{0}$ , so $h$ is bounded on a punctured neighbourhood of $0$ .

9.2F12step 8.3algebra

(Propagation, infinite case) Likewise, in the setting of step 8.3 the reciprocal $1 / h$ is holomorphic on each such annulus and bounded by $1$ on both boundary circles, so [F12] gives $∣ 1 / h ∣ \leq 1$ throughout the annulus; hence $1 / h$ is bounded on a punctured neighbourhood of $0$ .

10.1F13F14step 9.1step 9.2

(Meromorphic extension at the centre) If $h$ is bounded near $0$ , then [F13] makes $0$ a removable singularity of $h$ and $h$ has a holomorphic extension across $0$ . If instead $1 / h$ is bounded near $0$ , then [F13] extends $1 / h$ holomorphically to a function $φ$ with $φ (0) = c$ : if $c \neq 0$ then $h = 1 / φ$ is holomorphic near $0$ , and if $c = 0$ then $φ$ has a zero of finite order $m \geq 1$ at $0$ , and the pole criterion of [F14], applied to $f : = h$ whose reciprocal $φ = 1 / h$ extends holomorphically across $0$ and vanishes there, shows that $h$ has a pole of order $m$ at $0$ . In every case $h$ extends meromorphically at $0$ .

11.1step 2.1step 10.1discharge-construct∎

The local claim of step 2.1 is proved, so by step 2.1 the function $z \mapsto g (1 / z)$ is meromorphic in a neighbourhood of $0$ ; equivalently, $g$ extends meromorphically across $w = \infty$ . Every selection above was the least element of a finite or well-ordered explicitly enumerated list, so no choice principle is used.

TheoremStatement: Literature-sourcedProof: AI-adaptedaudited 2026-10-02Open item page →

The local Second Main Theorem on a punctured disc

Statement

Assume Countable Choice. Let $f$ be nonconstant and meromorphic on the punctured disc $0 < ∣ z - z_{0} ∣ < r^{*}$ ; choose $0 < ρ < r^{*}$ so that the circle $∣ z - z_{0} ∣ = ρ$ contains no poles and no preimages of the finitely many distinct targets $a_{1}, \dots, a_{q}$ of $f$ in the sphere, and put $F (w) = f (z_{0} + ρ / w)$ for $∣ w ∣ > 1$ . Define

$m_{e x t} (R, \infty; F) = \frac{1}{2 π} \int_{0}^{2 π} \log^{+} ∣ F (R e^{i θ}) ∣ d θ, N_{e x t} (R, a; F) = \int_{1}^{R} n_{e x t} (t, a; F) \frac{d t}{t},$

where $n_{e x t} (t, a; F)$ counts the $a$ -points of $F$ in $1 < ∣ w ∣ \leq t$ with full multiplicity (poles when $a = \infty$ ); put $T_{e x t} (R, F) = m_{e x t} (R, \infty; F) + N_{e x t} (R, \infty; F)$ , and let ${\overset{ˉ}{N}}_{e x t}$ count each point once. Then there are constants $C, R_{0} > 0$ and a measurable set $E \subseteq [R_{0}, \infty)$ of finite linear measure such that for every $R \geq R_{0}$ with $R \notin E$ ,

$(q - 2) T_{e x t} (R, F) \leq \sum_{j = 1}^{q} {\overset{ˉ}{N}}_{e x t} (R, a_{j}; F) + C (\log^{+} T_{e x t} (R, F) + \log R) .$

The exact local radius is $s = ρ / R$ , and the image exceptional set ${ρ / R : R \in E}$ has finite linear measure, bounded by $ρ R_{0}^{- 2} ∣ E ∣$ .

Facts & Assumptions

Given: A nonconstant meromorphic $f$ on $D^{*} = {0 < ∣ z - z_{0} ∣ < r^{*}}$ , distinct sphere targets $a_{1}, \dots, a_{q}$ , a radius $0 < ρ < r^{*}$ whose circle $∣ z - z_{0} ∣ = ρ$ carries no pole and no $a_{j}$ -point of $f$ , and $F (w) = f (z_{0} + ρ / w)$ ; Countable Choice is assumed (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

Plane counting and proximity conventions: for meromorphic $g$ on a plane domain, $n (r, a; g)$ is the multiplicity sum of the $a$ -points in $∣ z ∣ \leq r$ , $N (r, a; g) = n (0, a; g) \log r + \int_{0}^{r} \frac{n (t, a; g) - n (0, a; g)}{t} d t$ , $N = \overset{ˉ}{N} + N_{1}$ with $\overset{ˉ}{n}$ the number of distinct points and $n_{1}$ the local-degree surplus, while $m (r, a; g) = \frac{1}{2 π} \int_{0}^{2 π} \log \frac{1}{δ (g (r e^{i t}), a)} d t$ and $T (r, g) = m (r, \infty; g) + N (r, \infty; g)$ (Counting, chordal proximity and characteristic, Truncated value and ramification counts).

[F2]

Ramification identity and target sum: for a nonconstant meromorphic $g$ on a plane domain, $N_{1} (r, g) = N (r, 0; g^{'}) + 2 N (r, \infty; g) - N (r, \infty; g^{'})$ , and for every finite set $A$ of distinct sphere targets $\sum_{a \in A} N_{1} (r, a; g) \leq N_{1} (r, g)$ when $r \geq 1$ ; both follow from the same local-degree calculation as Ramification count from the derivative divisor wherever the stated counting functions are defined.

[F3]

Argument principle and winding number: if $γ$ is a closed complex contour and $g$ is meromorphic on a neighbourhood of $γ^{*}$ with $g \neq 0$ on $γ^{*}$ , then $\frac{1}{2 π i} \int_{γ} \frac{g^{'}}{g} = n (g \circ γ, 0) \in Z$ ; when $g$ is meromorphic on a neighbourhood of a closed disc bounded by a positively oriented circle, the same integral is the winding-weighted preimage count of $g - a$ minus the pole count (The argument-principle integral is the winding number of the image cycle, The argument principle counts preimages of a target value).

[F4]

Möbius maps: every Möbius transformation is a biholomorphism of the Riemann sphere, and any ordered triple of distinct sphere points is carried to $(0, 1, \infty)$ by a unique Möbius transformation; a biholomorphism preserves local degrees, so composing a meromorphic map with it preserves the target divisors and their multiplicities (Every Möbius transformation is a biholomorphism of the Riemann sphere, A unique Möbius transformation carries any ordered triple of distinct sphere points to any other).

[F5]

Exterior logarithmic-derivative lemma (Lund and Ye, Theorem A2, printed p. 552; Definition A, printed p. 549): for nonconstant $g$ meromorphic in a neighbourhood of the closed exterior ${σ \leq ∣ w ∣ < \infty}$ , $σ > 0$ , the logarithmic-derivative mean is $O_{g, σ} (\max {\log^{+} T_{1} (R, g), \log R})$ outside a set of finite linear measure as $R \to \infty$ . In their convention $m_{1} (R, g) = \int_{0}^{2 π} \log^{+} ∣ g (R e^{i θ}) ∣ d θ$ , $N_{1} (R, \infty; g)$ integrates the pole count in $σ \leq ∣ w ∣ \leq t$ from $σ$ to $R$ , and $T_{1} = m_{1} + N_{1}$ . If the circle $∣ w ∣ = σ$ has no pole of $g$ , then $N_{1}$ equals the normalized exterior count based at $σ$ , and $m_{1} = 2 π m_{e x t}$ . For $σ > 1$ , that count is at most $N_{e x t} (R, \infty; g)$ based at $1$ , since it omits only the finitely many poles with $1 < ∣ w ∣ < σ$ . Hence $T_{1} (R, g) \leq 2 π T_{e x t} (R, g)$ for $R \geq σ$ , which gives the required normalized bound in terms of this item's characteristic. The regular inner circle is essential to this comparison.

[F6]

Structural facts: the poles of a meromorphic function on a plane domain form a closed discrete set and are at most countable; a nonzero holomorphic function has only isolated zeros; two holomorphic functions on a domain that agree on a set with an accumulation point in the domain agree everywhere; a holomorphic function on a domain with derivative identically zero is constant (Poles of a meromorphic function form a closed discrete set and are at most countable, Zeros of a nonzero holomorphic function are isolated, Identity theorem for holomorphic functions, A holomorphic function with zero derivative on a domain is constant).

[F7]

Under Countable Choice, a $C^{1}$ diffeomorphism between open subsets of $R$ maps Lebesgue measurable sets to Lebesgue measurable sets, and for a measurable set $B$ its image measure is $\int_{B} ∣ S^{'} (R) ∣ d R$ (A C^1 diffeomorphism maps Lebesgue measurable sets to Lebesgue measurable sets, A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions).

Proof

technique · choose the inner circle to avoid poles and target preimages; derive the annular Jensen identity with its fixed inner-circle winding term; normalise the targets by a Möbius map so that all are finite; reuse the partial-fraction separation estimate of the plane Second Main Theorem, estimate the logarithmic derivatives on the exterior domain by the exterior logarithmic-derivative lemma, and use an auxiliary divisor-regular circle when applying the exterior First Main Theorem to the derivative

1.1F6choose

(The regular radius exists) On $D^{*}$ the pole set of $f$ is closed and discrete, and for each finite $a_{j}$ the $a_{j}$ -points are isolated: near such a point $f$ is holomorphic, and the zero is isolated unless $f - a_{j}$ vanishes on a neighbourhood, which by [F6] would force $f \equiv a_{j}$ on the connected domain $D^{*}$ , contrary to nonconstancy. On each compact annulus $\frac{1}{k + 1} \leq ∣ z - z_{0} ∣ \leq r^{*} (1 - \frac{1}{k + 1})$ these sets have only finitely many points. Hence only countably many radii meet a pole or a preimage of one of the finitely many targets; using the countable-choice interface (The Axiom of Countable Choice ( ${A C}_{ω}$ )) to run through the compact annuli, some $0 < ρ < r^{*}$ avoids them.

2.1constructstep 1.1

(Exterior setup) The inversion $w \mapsto z_{0} + ρ / w$ is a biholomorphism of ${∣ w ∣ > 1}$ onto ${0 < ∣ z - z_{0} ∣ < ρ}$ , so $F$ is nonconstant and meromorphic on the neighbourhood ${∣ w ∣ > ρ / r^{*}} \supseteq {∣ w ∣ \geq 1}$ of the closed exterior, and the circle $∣ w ∣ = 1$ carries no pole and no $a_{j}$ -preimage of $F$ .

3.1F3step 2.1algebra

(Annular Jensen identity) Fix a finite value $a$ with $F - a \neq 0$ on $∣ w ∣ = 1$ , put $M_{a} (t) = \frac{1}{2 π} \int_{0}^{2 π} \log ∣ F (t e^{i θ}) - a ∣ d θ$ for $t > 1$ , and $k_{a} : = \frac{1}{2 π i} \int_{∣ w ∣ = 1} \frac{F^{'} (w)}{F (w) - a} d w \in Z$ ; then for every $R > 1$ , $M_{a} (R) - M_{a} (1) = k_{a} \log R + N_{e x t} (R, a; F) - N_{e x t} (R, \infty; F)$ . Differentiating under the integral gives $\frac{d}{d t} M_{a} (t) = \frac{1}{t} \cdot \frac{1}{2 π i} \int_{∣ w ∣ = t} \frac{F^{'} (w)}{F (w) - a} d w$ , an integer by [F3]; at a zero of $F - a$ of order $e$ the local factorisation $F - a = (w - p)^{e} u$ raises that winding number by $e$ as $t$ crosses $∣ p ∣$ , and at a pole of $F$ of order $e$ the factorisation $F - a = (w - p)^{- e} u$ lowers it by $e$ , so the integral equals $k_{a} + n_{e x t} (t, a; F) - n_{e x t} (t, \infty; F)$ for almost every $t$ and integration against $\frac{d t}{t}$ yields the identity, which extends to all $R > 1$ by continuity.

4.1F1step 3.1algebra

(Two-sided exterior First Main Theorem) Let $g$ be meromorphic on a neighbourhood of ${∣ w ∣ \geq 1}$ , and suppose its inner circle contains no pole of $g$ and no point with $g = a$ , where $a \in C$ . Put $m_{e x t} (R, a; g) = \frac{1}{2 π} \int_{0}^{2 π} \log^{+} \frac{1}{∣ g (R e^{i θ}) - a ∣} d θ$ . Then $m_{e x t} (R, a; g) + N_{e x t} (R, a; g) = T_{e x t} (R, g) + O_{a} (\log R)$ two-sidedly. Indeed step 3.1 applied to $g$ and the identity $\log ∣ g - a ∣ = \log^{+} ∣ g - a ∣ - \log^{+} \frac{1}{∣ g - a ∣}$ give $m_{e x t} (R, a; g) = m_{e x t}^{+} (R, a; g) - M_{a} (1) - k_{a} \log R - N_{e x t} (R, a; g) + N_{e x t} (R, \infty; g)$ , and by [F1] the comparison $∣ \log^{+} ∣ g - a ∣ - \log^{+} ∣ g ∣ ∣ \leq \log^{+} ∣ a ∣ + \log 2$ is two-sided, so substituting $m_{e x t} (R, \infty; g) - O_{a} (1) \leq m_{e x t}^{+} (R, a; g) \leq m_{e x t} (R, \infty; g) + O_{a} (1)$ proves the claim. The same Jensen calculation may be anchored at any regular circle $∣ w ∣ = σ > 1$ ; its integrated counts differ from those anchored at $1$ by $O (\log R)$ because only finitely many divisor points lie in $1 < ∣ w ∣ \leq σ$ .

5.1F4step 2.1step 4.1construct

(Möbius normalisation and characteristic comparison) If $q \leq 2$ the asserted inequality is trivial with $C = 0$ ; assume $q \geq 3$ . Choose any finite $b \notin {a_{1}, \dots, a_{q}}$ and let $M$ be the Möbius transformation with $M (b) = \infty$ , $M (a_{1}) = 0$ , $M (a_{2}) = 1$ [F4]; put $c_{j} : = M (a_{j})$ and $G : = M \circ F$ . Then each $c_{j}$ is finite and the $c_{j}$ are distinct; $G$ is nonconstant and meromorphic on a neighbourhood of ${∣ w ∣ \geq 1}$ , and the circle $∣ w ∣ = 1$ carries no $c_{j}$ -point of $G$ . By [F4] the $c_{j}$ -divisor of $G$ equals the $a_{j}$ -divisor of $F$ with multiplicities and the poles of $G$ are exactly the $b$ -points of $F$ in $∣ w ∣ > 1$ with equal orders, so ${\overset{ˉ}{N}}_{e x t} (R, c_{j}; G) = {\overset{ˉ}{N}}_{e x t} (R, a_{j}; F)$ and $N_{e x t} (R, \infty; G) = N_{e x t} (R, b; F)$ . Since $M (u) = A / (u - b) + D$ for constants $A \neq 0, D$ , $m_{e x t} (R, \infty; G) = m_{e x t} (R, b; F) + O (1)$ . Choose one $r_{1} \in (1, 2)$ whose circle avoids the poles and $b$ -points of $F$ , the poles and $c_{j}$ -points of $G$ , and the zeros and poles of $G^{'}$ . These divisors are locally finite in the compact annulus $1 \leq ∣ w ∣ \leq 2$ , so only finitely many radii are excluded. Applying step 4.1 at $r_{1}$ and using its base-radius observation gives $m_{e x t} (R, b; F) + N_{e x t} (R, b; F) = T_{e x t} (R, F) + O (\log R)$ . Therefore $T_{e x t} (R, G) = T_{e x t} (R, F) + O (\log R)$ two-sidedly.

6.1step 5.1algebra

(Target separation) Put $δ : = \min_{i < j} ∣ c_{i} - c_{j} ∣ > 0$ and $H : = \sum_{j = 1}^{q} \frac{1}{G - c_{j}}$ ; the pointwise separation estimate of the plane Second Main Theorem Nevanlinna Second Main Theorem with ramification and truncation, valid for an arbitrary meromorphic function and reproduced here in the exterior normalisation, gives $\sum_{j = 1}^{q} \log^{+} \frac{1}{∣ G (w) - c_{j} ∣} \leq \log^{+} ∣ H (w) ∣ + C_{q, δ}$ on every outer circle, with $C_{q, δ} = \log 2 + \max {q \log^{+} (4 (q - 1) / δ), (q - 1) \log^{+} (2 / δ)}$ ; points with $G (w) = c_{j}$ are covered by the convention $+ \infty \leq + \infty$ .

6.2F1F2step 5.1algebra

(Exterior ramification bookkeeping) Define $N_{1, e x t} (R, a; G) : = N_{e x t} (R, a; G) - {\overset{ˉ}{N}}_{e x t} (R, a; G)$ and $N_{1, e x t} (R, G) : = N_{e x t} (R, 0; G^{'}) + 2 N_{e x t} (R, \infty; G) - N_{e x t} (R, \infty; G^{'})$ . The pointwise computation of [F2] applied at each point $w$ of the annulus $1 < ∣ w ∣ \leq R$ with local degree $e_{w}$ of $G$ gives $N_{1, e x t} (R, a; G) = \sum_{G (w) = a} (e_{w} - 1) \log \frac{R}{∣ w ∣}$ , $N_{1, e x t} (R, G) = \sum_{e_{w} \geq 2} (e_{w} - 1) \log \frac{R}{∣ w ∣}$ , hence $N_{e x t} (R, a; G) = {\overset{ˉ}{N}}_{e x t} (R, a; G) + N_{1, e x t} (R, a; G)$ with $0 \leq N_{1, e x t} (R, a; G) \leq N_{e x t} (R, a; G)$ , and $\sum_{j = 1}^{q} N_{1, e x t} (R, c_{j}; G) \leq N_{1, e x t} (R, G)$ because each ramified point contributes to at most one of the disjoint target classes.

6.3F5step 5.1algebra

(Exterior logarithmic-derivative bounds) Apply [F5] to $G$ and each $G - c_{j}$ with inner radius $σ = r_{1}$ from step 5.1. All are nonconstant and meromorphic on a neighbourhood of that closed exterior; its inner circle has no pole or zero of these functions. Thus the source characteristics obey $T_{1} (R, G) \leq 2 π T_{e x t} (R, G)$ and $T_{1} (R, G - c_{j}) \leq 2 π T_{e x t} (R, G - c_{j})$ , with the right sides based at $1$ . Their pole divisors agree and $∣ \log^{+} ∣ G - c_{j} ∣ - \log^{+} ∣ G ∣ ∣ \leq \log 2 + \log^{+} ∣ c_{j} ∣$ , so $T_{e x t} (R, G - c_{j}) = T_{e x t} (R, G) + O (1)$ . Taking the finite union of the $q + 1$ source exceptional sets, we obtain a measurable $E$ of finite linear measure such that $m_{e x t} (R, \infty; G^{'} / G)$ and every $m_{e x t} (R, \infty; G^{'} / (G - c_{j}))$ are bounded by $C_{j} (\log^{+} T_{e x t} (R, G) + \log R)$ at all sufficiently large $R \notin E$ .

7.1step 6.1algebra

(Reduction to logarithmic derivatives) Since $H = (H G^{'}) \cdot \frac{1}{G^{'}}$ and $H G^{'} = \sum_{j = 1}^{q} \frac{G^{'}}{G - c_{j}}$ , the pointwise inequalities $\log^{+} ∣ u v ∣ \leq \log^{+} ∣ u ∣ + \log^{+} ∣ v ∣$ and $\log^{+} ∣ \sum_{j \leq q} u_{j} ∣ \leq \sum_{j \leq q} \log^{+} ∣ u_{j} ∣ + \log q$ give $m_{e x t} (R, \infty; H) \leq m_{e x t} (R, 0; G^{'}) + \sum_{j = 1}^{q} m_{e x t} (R, \infty; G^{'} / (G - c_{j})) + \log q$ for every $R > 0$ .

7.2step 4.1step 6.2F6algebra

(The term $m_{e x t} (0; G^{'}) + N_{1, e x t}$ ) By the choice in step 5.1, $∣ w ∣ = r_{1}$ contains no zero or pole of $G^{'}$ . Apply the annular Jensen identity of step 4.1 to $G^{'}$ with inner circle $∣ w ∣ = r_{1}$ ; its counts anchored at $r_{1}$ differ from $N_{e x t} (R, \cdot; G^{'})$ , anchored at $1$ , by $O (\log R)$ , since only finitely many zeros and poles lie in $1 < ∣ w ∣ \leq r_{1}$ . Thus $m_{e x t} (R, 0; G^{'}) = m_{e x t} (R, \infty; G^{'}) + N_{e x t} (R, \infty; G^{'}) - N_{e x t} (R, 0; G^{'}) + O (\log R) .$ Adding the definition of $N_{1, e x t} (R, G)$ from step 6.2 yields $m_{e x t} (R, 0; G^{'}) + N_{1, e x t} (R, G) = m_{e x t} (R, \infty; G^{'}) + 2 N_{e x t} (R, \infty; G) + O (\log R)$ .

7.3step 6.3algebra

(Bounding $m_{e x t} (\infty; G^{'})$ ) The pointwise bound $\log^{+} ∣ G^{'} ∣ \leq \log^{+} ∣ G ∣ + \log^{+} ∣ G^{'} / G ∣$ gives $m_{e x t} (R, \infty; G^{'}) \leq m_{e x t} (R, \infty; G) + m_{e x t} (R, \infty; G^{'} / G) \leq m_{e x t} (R, \infty; G) + C_{0} (\log^{+} T_{e x t} (R, G) + \log R)$ for $R$ large outside the exceptional set of step 6.3.

8.1step 6.1step 7.1step 6.3step 7.2step 7.3algebra

(Ramified exterior Second Main Theorem) Combining steps 6.1, 7.1, 6.3, 7.2 and 7.3, for all large $R$ outside the finite-measure exceptional set $E$ one has $\sum_{j = 1}^{q} m_{e x t} (R, c_{j}; G) + N_{1, e x t} (R, G) \leq 2 T_{e x t} (R, G) + C_{1} (\log^{+} T_{e x t} (R, G) + \log R)$ : the separation and logarithmic-derivative steps bound the proximity sum by $m_{e x t} (R, 0; G^{'}) + C$ , and steps 7.2 and 7.3 bound $m_{e x t} (R, 0; G^{'})$ by $2 T_{e x t} (R, G) - N_{1, e x t} (R, G) + C_{1} (\log^{+} T_{e x t} + \log R)$ .

9.1step 4.1step 5.1step 6.2step 8.1algebra

(Truncated exterior Second Main Theorem) Step 4.1 at the regular radius $r_{1}$ of step 5.1 gives $\sum_{j = 1}^{q} m_{e x t} (R, c_{j}; G) = q T_{e x t} (R, G) - \sum_{j = 1}^{q} N_{e x t} (R, c_{j}; G) + O (\log R)$ ; the base-radius observation in step 4.1 accounts for the divisor terms between radii $1$ and $r_{1}$ . Substituting into step 8.1 and using $N_{e x t} (c_{j}) = {\overset{ˉ}{N}}_{e x t} (c_{j}) + N_{1, e x t} (c_{j})$ together with $\sum_{j} N_{1, e x t} (R, c_{j}; G) \leq N_{1, e x t} (R, G)$ from step 6.2 gives $(q - 2) T_{e x t} (R, G) \leq \sum_{j = 1}^{q} {\overset{ˉ}{N}}_{e x t} (R, c_{j}; G) + C_{2} (\log^{+} T_{e x t} (R, G) + \log R)$ for all large $R \notin E$ .

10.1step 5.1step 9.1algebra

(Transfer back to $F$ ) Using ${\overset{ˉ}{N}}_{e x t} (R, c_{j}; G) = {\overset{ˉ}{N}}_{e x t} (R, a_{j}; F)$ , the two-sided comparison $T_{e x t} (R, G) = T_{e x t} (R, F) + O (\log R)$ of step 5.1, and $\log^{+} T_{e x t} (R, G) \leq \log^{+} T_{e x t} (R, F) + O (\log R)$ for large $R$ , the inequality of step 9.1 becomes $(q - 2) T_{e x t} (R, F) \leq \sum_{j = 1}^{q} {\overset{ˉ}{N}}_{e x t} (R, a_{j}; F) + C (\log^{+} T_{e x t} (R, F) + \log R)$ for all large $R$ outside $E$ , with a suitably enlarged constant $C$ .

11.1F7step 10.1algebra∎

(The exceptional set in the puncture radius) The substitution $s = ρ / R$ maps $[R_{0}, \infty)$ bijectively onto $(0, ρ / R_{0}]$ with $∣ \frac{d s}{d R} ∣ = ρ R^{- 2} \leq ρ R_{0}^{- 2}$ , so by the change-of-variables formula for a measurable set the image ${ρ / R : R \in E}$ of the exceptional set $E$ of step 6.3 has linear measure at most $ρ R_{0}^{- 2} ∣ E ∣ < \infty$ .

CorollaryStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-6.1-sol)audited 2026-10-02Open item page →

Little and Great Picard consequences of Nevanlinna theory

Statement

Assume Countable Choice.

A nonconstant meromorphic function on $C$ omits at most two values of the Riemann sphere. Consequently a nonconstant entire function omits at most one finite value.
Let $f$ be meromorphic on a punctured disc $0 < ∣ z - z_{0} ∣ < r^{*}$ with an isolated essential singularity at $z_{0}$ , that is, $f$ admits no meromorphic extension across $z_{0}$ . Then in every punctured neighbourhood of $z_{0}$ every sphere value is assumed infinitely often, with at most two exceptions. If in addition $f$ is holomorphic on the punctured disc, then at most one finite value is exceptional in this sense.

Facts & Assumptions

Given: A nonconstant meromorphic plane function for clause (1), and a meromorphic function on a punctured disc with an isolated essential singularity for clause (2). Assume Countable Choice.

[F1]

For three distinct sphere targets omitted by a nonconstant meromorphic plane function $h$ , the truncated Second Main Theorem gives $T (r, h) \leq C (\log^{+} T (r, h) + \log r)$ outside a set of finite linear measure (Nevanlinna Second Main Theorem with ramification and truncation).

[F2]

If $h$ is transcendental, then $T (r, h) / \log r \to \infty$ and $T (r, h) \to \infty$ (Transcendental characteristic dominates logarithmic growth).

[F3]

A meromorphic function on an exterior domain that omits three fixed distinct sphere values outside a larger circle extends meromorphically across infinity (Three omitted values force exterior extension).

[F4]

Every nonconstant complex polynomial has a complex root (Fundamental theorem of algebra by Liouville's theorem).

Proof

technique · direct, with contradiction arguments for three omitted values

1.1F4algebra

A nonconstant rational function $P / Q$ , with coprime polynomials and $d = \max (\deg P, \deg Q) \geq 1$ , omits at most one sphere value. If $\deg Q < d$ , then $\deg (P - a Q) = d$ for every finite $a$ , so [F4] makes every finite value attained; $\infty$ is omitted only when $Q$ is constant. If $\deg Q = d$ , then $Q$ has a root, so $\infty$ is attained. When $\deg P = d$ , the polynomial $P - a Q$ has degree $d$ except possibly for the single value $a$ that cancels its leading term. When $\deg P < d$ , every $a \neq 0$ gives a polynomial $P - a Q$ of degree $d$ , and $a = 0$ is attained unless $P$ is a nonzero constant. Thus at most one finite value can be omitted in this case.

1.2F3givendischarge-contradiction

Let $f$ be meromorphic on $0 < ∣ z - z_{0} ∣ < r^{*}$ with an isolated essential singularity. If three distinct sphere values are omitted on $0 < ∣ z - z_{0} ∣ < ρ$ for some $ρ < r^{*}$ , then $G (w) : = f (z_{0} + ρ / w)$ is meromorphic on $∣ w ∣ > 1$ and omits those values there. Apply [F3] with $R = 1$ and $R_{1} = 2$ : $G$ extends meromorphically across infinity. Inversion then extends $f$ meromorphically across $z_{0}$ , a contradiction. Thus no three distinct values are omitted on any punctured neighbourhood.

2.1F1F2step 1.1discharge-contradiction

Suppose a nonconstant meromorphic plane function $h$ omits three distinct sphere values. By step 1.1 it is transcendental. [F1] gives $T (r, h) \leq C (\log^{+} T (r, h) + \log r)$ outside a set $E$ of finite linear measure, while [F2] makes the right side $o (T (r, h))$ as $r \to \infty$ . The complement of $E$ is unbounded, so this inequality is impossible at sufficiently large $r \notin E$ . Hence a nonconstant meromorphic plane function omits at most two sphere values.

2.2step 1.2choosecases

If three distinct sphere values each had only finitely many preimages in some punctured neighbourhood, choose one radius smaller than all three neighbourhood radii. Their combined preimage set inside it is finite. Choose a still smaller radius below the distance from $z_{0}$ to every point of that finite set; if the set is empty, any smaller radius works. All three values are then omitted on that smaller punctured disc, contrary to step 1.2. Hence at most two sphere values fail to occur infinitely often in every punctured neighbourhood.

3.1step 2.1step 2.2algebra∎

An entire function omits $\infty$ , so step 2.1 leaves at most one omitted finite value. A function holomorphic on the punctured disc also omits $\infty$ , so step 2.2 leaves at most one finite value that fails to occur infinitely often near the puncture.

TheoremStatement: Literature-sourcedProof: AI-adaptedaudited 2026-10-02Open item page →

Nevanlinna five-value uniqueness theorem

Statement

Assume Countable Choice. Let $f$ and $g$ be nonconstant meromorphic functions on $C$ . Suppose that $f$ and $g$ share five distinct sphere values ignoring multiplicity: there are distinct $a_{1}, \dots, a_{5} \in \hat{C}$ such that for each $j$ the preimage sets ${z : f (z) = a_{j}}$ and ${z : g (z) = a_{j}}$ agree. Then $f = g$ identically.

Facts & Assumptions

Given: Nonconstant meromorphic functions $f, g$ on $C$ sharing the distinct sphere values $a_{1}, \dots, a_{5}$ ; Countable Choice is assumed (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

First Main Theorem: for nonconstant meromorphic $h$ and $a \in \hat{C}$ , $m (r, a; h) + N (r, a; h) = T (r, h) + C (h, a)$ with $C (h, a)$ independent of $r$ ; in particular $N (r, a; h) \leq T (r, h) + C (h, a)$ (Nevanlinna’s First Main Theorem with exact centre constant).

[F2]

Characteristic laws: $T (r, h_{1} + h_{2}) \leq T (r, h_{1}) + T (r, h_{2}) + O (1)$ , $T (r, 1 / h) = T (r, h) + O_{h} (1)$ for $h \equiv̸ 0$ , and for a fixed rational map $R = P / Q$ of degree $d = \max (\deg P, \deg Q) \geq 1$ and nonconstant meromorphic $h$ , $T (r, R (h)) = d T (r, h) + O_{R, h} (1)$ ; a Möbius transformation is such an $R$ with $d = 1$ (Elementary characteristic laws and fixed rational composition).

[F3]

Truncated Second Main Theorem: for nonconstant meromorphic $h$ on $C$ and distinct sphere targets $b_{1}, \dots, b_{q}$ with $q \geq 3$ , $(q - 2) T (r, h) \leq \sum_{j = 1}^{q} \overset{ˉ}{N} (r, b_{j}; h) + S (r, h)$ outside a set of finite linear measure, where $S (r, h) \leq C (\log^{+} T (r, h) + \log r)$ off that set; when $h$ is rational the error is $O_{h} (1)$ , and for $h$ of finite order it is $O_{h} (\log r)$ , in both cases at every sufficiently large radius (Nevanlinna Second Main Theorem with ramification and truncation).

[F4]

Truncated counts: $\overset{ˉ}{N} (r, b; h)$ counts the distinct $b$ -points of $h$ once, and $N (r, a; h) = \overset{ˉ}{N} (r, a; h) + N_{1} (r, a; h)$ with $N_{1} (r, a; h) \geq 0$ for $r \geq 1$ ; each zero of $h$ contributes its multiplicity to $N (r, 0; h)$ (Truncated value and ramification counts).

[F5]

Growth: every nonconstant meromorphic $h$ on $C$ has $T (r, h) \to \infty$ ; $T (r, h) / \log r \to \infty$ when $h$ is transcendental, and $T (r, h) = d \log r + O (1)$ when $h$ is rational of degree $d$ (Transcendental characteristic dominates logarithmic growth).

Proof

technique · normalise the five values to finite values by a Möbius map, compare the common value counts with the zeros of $F-G$, apply the truncated Second Main Theorem to both normalised functions, and use the characteristic growth to reach a contradiction unless $F-G\equiv0$

1.1F2construct

(Möbius normalisation) Pick $b \in C ∖ {a_{1}, \dots, a_{5}}$ and put $R (z) : = 1 / (z - b)$ , a Möbius transformation with $R (b) = \infty$ ; set $F : = R \circ f$ , $G : = R \circ g$ and $c_{j} : = R (a_{j})$ . Then each $c_{j}$ is finite (it is $0$ when $a_{j} = \infty$ ) and the $c_{j}$ are distinct; $F$ and $G$ are nonconstant meromorphic, their preimage sets of $c_{j}$ agree for every $j$ , and [F2] gives $T (r, F) = T (r, f) + O (1)$ and $T (r, G) = T (r, g) + O (1)$ as $r \to \infty$ .

2.1F1F2F4step 1.1

(Common value count versus zeros of the difference) Put $h : = F - G$ , a meromorphic function, and $C (r) : = \sum_{j = 1}^{5} \overset{ˉ}{N} (r, c_{j}; F)$ . The sets ${F = c_{j}}$ are pairwise disjoint because the $c_{j}$ are distinct, and each is contained in ${h = 0}$ , since $F (z) = c_{j}$ forces $G (z) = c_{j}$ by the sharing hypothesis. If $h \equiv 0$ there is nothing to prove. If $h$ is a nonzero constant, then $C (r) = 0$ , since no common $c_{j}$ -point can be a zero of $h$ . Otherwise $h$ is nonconstant, so for $r \geq 1$ the distinct common zeros have nonnegative integrated weights and [F1] applied at target $0$ , together with [F2], gives $C (r) \leq N (r, 0; h) \leq T (r, h) + O (1) \leq T (r, F) + T (r, G) + O (1) = T (r, f) + T (r, g) + O (1)$ . Thus the count bound holds for all large $r$ when $h \equiv̸ 0$ , which is the range used below; from here on assume $h \equiv̸ 0$ .

3.1F3step 1.1step 2.1algebra

(Second Main Theorem bounds) Apply [F3] with $q = 5$ to the nonconstant functions $F$ and $G$ and the distinct finite targets $c_{1}, \dots, c_{5}$ : outside sets $E_{F}$ and $E_{G}$ of finite linear measure, $3 T (r, F) \leq \sum_{j = 1}^{5} \overset{ˉ}{N} (r, c_{j}; F) + S (r, F)$ and $3 T (r, G) \leq \sum_{j = 1}^{5} \overset{ˉ}{N} (r, c_{j}; G) + S (r, G)$ ; by the shared preimage sets, $\sum_{j} \overset{ˉ}{N} (r, c_{j}; F) = \sum_{j} \overset{ˉ}{N} (r, c_{j}; G) = C (r)$ , so adding gives $3 (T (r, F) + T (r, G)) \leq 2 C (r) + S (r, F) + S (r, G)$ outside $E : = E_{F} \cup E_{G}$ .

4.1F3F5step 3.1algebra

(Growth separation) Off $E$ , both errors are negligible compared with $T (r, F) + T (r, G)$ : if $F$ is transcendental then $S (r, F) = O (\log^{+} T (r, F) + \log r) = o (T (r, F))$ because $T (r, F) / \log r \to \infty$ and $T (r, F) \to \infty$ by [F5], while if $F$ is rational then $S (r, F) = O (1) = o (T (r, F))$ ; in either case $S (r, F) = o (T (r, F) + T (r, G))$ , and the same argument applies to $G$ , so $S (r, F) + S (r, G) = o (T (r, F) + T (r, G))$ along $r \notin E$ , large $r$ .

5.1F5step 2.1step 3.1step 4.1algebra

(Contradiction unless the difference vanishes) Substituting the count bound of step 2.1 into step 3.1 and using step 4.1 gives $3 (T (r, F) + T (r, G)) \leq 2 (T (r, F) + T (r, G)) + o (T (r, F) + T (r, G)) + O (1)$ , hence $T (r, F) + T (r, G) \leq o (T (r, F) + T (r, G)) + O (1)$ for all large $r \notin E$ . Since $E$ has finite measure its complement is unbounded, and along it $T (r, F) + T (r, G) \to \infty$ by [F5] because $F$ and $G$ are nonconstant; choosing $r \notin E$ so large that the $o (1)$ term is below $\frac{1}{2}$ makes the inequality impossible. Hence $h \equiv 0$ , that is, $F \equiv G$ .

6.1step 1.1step 5.1algebra∎

(Conclusion) From $F \equiv G$ and $F = R \circ f$ , $G = R \circ g$ with $R$ injective on the sphere, $f = R^{- 1} \circ F = R^{- 1} \circ G = g$ identically.

5 · Examples, counterexamples and false statements

None yet.

Nevanlinna's Second Main Theorem and Defects

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

Nevanlinna exceptional-radius error notation

Definition

Remarks

Truncated value and ramification counts

Definition

Facts & Assumptions

Proof

Finite-measure growth increment lemma

Statement

Facts & Assumptions

Proof

Separated-radius Poisson–Jensen derivative bound

Statement

Facts & Assumptions

Proof

Ramification count from the derivative divisor

Statement

Facts & Assumptions

Proof

The lemma on the logarithmic derivative

Statement

Facts & Assumptions

Proof

Transcendental characteristic dominates logarithmic growth

Statement

Facts & Assumptions

Proof

Nevanlinna Second Main Theorem with ramification and truncation

Statement

Facts & Assumptions

Proof

Nevanlinna deficiency and ramification index

Definition

Facts & Assumptions

Proof

Nevanlinna deficiency and ramification defect relations

Statement

Facts & Assumptions

Proof

Three omitted values force exterior extension

Statement

Facts & Assumptions

Proof

The local Second Main Theorem on a punctured disc

Statement

Facts & Assumptions

Proof

Little and Great Picard consequences of Nevanlinna theory

Statement

Facts & Assumptions

Proof

Nevanlinna five-value uniqueness theorem

Statement

Facts & Assumptions

Proof

5 · Examples, counterexamples and false statements

Sources