Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27
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 logarithm of the modulus of a holomorphic function is subharmonic

Statement

Let Ω⊆C be a complex domain and let f be holomorphic on Ω, not identically zero on any connected component. Define u(z)=log⁡∣f(z)∣, with the convention u(z)=−∞ at the zeros of f. Then u is subharmonic on Ω.

Facts & Assumptions

Given: A holomorphic function f on a complex domain Ω, not identically zero on any connected component.

[L1]

A C2 real function is subharmonic exactly when its Laplacian is nonnegative (A C^2 function is subharmonic exactly when its Laplacian is nonnegative).

[L2]

Near a zero a of order m, the function f factors as f(z)=(z−a)mg(z) with g holomorphic and g(a)≠0 (The order of a zero is the exponent in its local holomorphic factorization).

[L3]

A holomorphic nonvanishing function on a disc has a holomorphic logarithm there (A nonvanishing holomorphic function on a disc has a holomorphic logarithm).

[L4]

Holomorphic functions are smooth, so their real and imaginary parts admit the second derivatives used in [L1] (Holomorphic functions are real analytic and smooth in their two real coordinates).

Proof

technique · direct
1.1L1L3L4

Let D⊆Ω be a disc on which f has no zeros. By [L3], there is a holomorphic function L on D with exp⁡L=f. Writing L=α+iβ, one has α=log⁡∣f∣ on D. Since L is holomorphic and smooth by [L4], the Cauchy-Riemann equations imply Δα=0, so [L1] makes log⁡∣f∣ subharmonic on every zero-free disc.

2.1L2step 1.1

Fix a zero a of f, and let m=ord⁡a(f). By [L2], on a small disc about a one has f(z)=(z−a)mg(z) with g(a)≠0. Shrinking if necessary, g has no zeros there, so step 1.1 makes log⁡∣g∣ harmonic and hence subharmonic on that disc.

3.1step 2.1algebra

On the punctured disc around a, [step 2.1, algebra] u(z)=mlog⁡∣z−a∣+log⁡∣g(z)∣. The function log⁡∣z−a∣ is harmonic on the punctured disc, and at the center a its value is −∞ while every circle average is finite; hence it is subharmonic there. Therefore the right-hand side is subharmonic on the whole disc, agreeing with u away from a and with u(a)=−∞ at the center.

4.1step 1.1step 3.1∎

Every point of Ω lies either on a zero-free disc covered by step 1.1 or on a zero-containing disc covered by step 3.1. So u is subharmonic throughout Ω.

Depends on

Used by

Dependency tree · two levels

29 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