LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-10-02

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.

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.

Depends on

Used by

Nevanlinna Second Main Theorem with ramification and truncation Theorem

Dependency tree · two levels

37 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Goldberg–Ostrovskii, Value Distribution of Meromorphic Functions (standard reference, not scraped)
I. Laine, Complex Analysis III lecture notes (standard reference, not scraped)
Alexandre Eremenko, Lectures on Nevanlinna Theory, §6 (standard reference, not scraped)