Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29
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.

Jensen's formula on a disc

Statement

Let f be holomorphic on a neighbourhood of the closed disc {∣z∣≤R}, assume f(0)≠0, and let a1,…,aN be the zeros of f in ∣z∣<R, counted with multiplicity. If f has no zero on ∣z∣=R, then

log⁡∣f(0)∣=12π∫02πlog⁡∣f(Reit)∣ dt−∑k=1Nlog⁡R∣ak∣.

For a radius meeting boundary zeros, the same identity is recovered by taking r↑R through radii that avoid zeros on ∣z∣=r.

Facts & Assumptions

Given: A holomorphic function f on a neighbourhood of the closed disc {∣z∣≤R}, with f(0)≠0.

[F1]

Cauchy's integral formula on a circle recovers the value at the centre (Cauchy's integral formula on a circle compactly contained in a disc of holomorphy).

[F2]

A zero of multiplicity m can be factored as (z−a)m times a holomorphic nonvanishing factor (The order of a zero is the exponent in its local holomorphic factorization).

[F3]

A nowhere-zero holomorphic function on a disc has a holomorphic logarithm, because discs are star-shaped and homologically simply connected (Star-shaped plane domains are homologically simply connected, A nonvanishing holomorphic function on a homologically simply connected domain has a holomorphic logarithm).

Proof

technique · direct
1.1F2givenalgebra

Assume first that f has no zero on ∣z∣=R. Because the closed disc is compact, f has only finitely many zeros in ∣z∣<R; applying [F2] repeatedly gives f(z)=∏k=1N(z−ak)g(z) on a neighbourhood of the closed disc, where g is holomorphic and zero-free there.

2.1F1F3step 1.1algebra

By [F3], choose a holomorphic logarithm L of g on ∣z∣<R. Applying [F1] to L on the circle ∣z∣=R and taking real parts yields log⁡∣g(0)∣=12π∫02πlog⁡∣g(Reit)∣ dt.

3.1F1F3step 2.1algebra

For each zero ak with ∣ak∣<R, write Reit−ak=Reit(1−akR−1e−it). The factor 1−akR−1z is zero-free on the closed unit disc, so the same argument as in step 2.1 shows 12π∫02πlog⁡∣1−akR−1e−it∣ dt=0; hence 12π∫02πlog⁡∣Reit−ak∣ dt=log⁡R.

4.1step 1.1step 2.1step 3.1algebra

Taking logarithms of the factorization in step 1.1 on the boundary circle and averaging, step 2.1 gives the mean for g and step 3.1 contributes one log⁡R for each zero. Rearranging yields log⁡∣f(0)∣=12π∫02πlog⁡∣f(Reit)∣ dt−∑k=1Nlog⁡(R/∣ak∣).

5.1step 4.1algebra∎

If f has zeros on ∣z∣=R, apply step 4.1 to radii r<R with no zero on ∣z∣=r; as r↑R, the zero list inside ∣z∣<r stabilizes except when r crosses one of finitely many zero moduli, and the boundary integral converges to the stated radial limit.

Depends on

Used by

Dependency tree · two levels

46 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