PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-30

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.

Entire-function order agrees with maximum-modulus order

Statement

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

Facts & Assumptions

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

[F1]

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

[F2]

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

[F3]

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

[F4]

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

[F5]

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

[F6]

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

Proof

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

1.1F1algebra

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

1.2F4F5F6givenalgebra

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

2.1F1step 1.1algebra

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

2.2F1F2step 1.1algebra

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

3.1F1F3step 1.1step 1.2step 2.1step 2.2algebra∎

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

Depends on

Used by

Rational functions are exactly those with logarithmic characteristic 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, Ch. 1 §7, Theorem 7.1; Ch. 2 §1, Theorem 1.3 (standard reference, not scraped)