TheoremStatement: 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.

Poisson–Jensen formula for a meromorphic function on a disc

Statement

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

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

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

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

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

Facts & Assumptions

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

[F1]

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

[F2]

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

[F3]

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

[F4]

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

[F5]

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

[F6]

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

[F7]

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

Proof

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

1.1F1F2F4given

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

1.2algebra

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

1.3

Form

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

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

2.1F6F7step 1.3

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

3.1F5step 1.2step 1.3step 2.1algebra

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

4.1F3F4step 3.1algebra∎

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

Depends on

Used by

Dependency tree · two levels

43 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

Alexandre Eremenko, Lectures on Nevanlinna Theory, §1 (standard reference, not scraped)
Goldberg–Ostrovskii, Value Distribution of Meromorphic Functions, Ch. 1 §§1–2 (standard reference, not scraped)