Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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)=logf(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)=(za)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.1

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

L1L3L4
2.1

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

L2step 1.1
3.1

On the punctured disc around a, [step 2.1, algebra] u(z)=mlogza+logg(z). The function logza 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.

step 2.1algebra
4.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 Ω.

step 1.1step 3.1

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