TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

Zero-free inner functions are unimodular multiples of singular inner functions

Statement

Assume the Axiom of Choice. Let $S$ be holomorphic and zero-free on $D$ with $∣ S ∣ \leq 1$ , and suppose that its boundary function satisfies $∣ S^{*} ∣ = 1$ $m$ -almost everywhere (equivalently, $S$ is an inner function without zeros). Then there are a unique $λ \in T$ and a unique finite positive measure $μ ⊥ m$ with $S = λ S_{μ}, S_{μ} (z) = \exp (- \int_{T} K (z, ζ) d μ (ζ)) .$ With the normalizations $S_{μ} (0) = e^{- μ (T)} > 0$ and $λ = S (0) / S_{μ} (0)$ , the pair $(λ, μ)$ is unique. In particular $S_{μ}$ is the singular inner function of $μ$ , and every inner function is, up to a unimodular constant, the product of a Blaschke product and a singular inner function.

Facts & Assumptions

Given: The Axiom of Choice, hence countable choice (The Axiom of Choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )); a zero-free holomorphic $S$ on $D$ with $∣ S ∣ \leq 1$ and $∣ S^{*} ∣ = 1$ $m$ -almost everywhere; and, where asserted, an inner function $θ$ .

[L1]

$S$ zero-free means $\log ∣ S ∣$ is harmonic on $D$ , so $u : = - \log ∣ S ∣ = - Re \log S$ is a nonnegative harmonic function with $u (0) = - \log ∣ S (0) ∣ < + \infty$ ; the kernel $K (z, ζ) = (ζ + z) / (ζ - z)$ is holomorphic in $z$ with $Re K = P$ (A nonvanishing holomorphic function on a homologically simply connected domain has a holomorphic logarithm, Holomorphic functions are real analytic and smooth in their two real coordinates, The $C^{2}$ real and imaginary parts of a holomorphic function satisfy Laplace's equation and form a harmonic-conjugate pair, Star-shaped plane domains are homologically simply connected, Inner, singular inner and outer functions, Plane harmonic functions).

[L2]

Herglotz representation: every nonnegative harmonic $u$ on $D$ is $u = P [μ]$ for a unique finite nonnegative regular Borel measure $μ$ with $μ (T) = u (0)$ , and conversely $P [μ]$ is nonnegative harmonic (Positive harmonic boundary measures and compact normalized families).

[L3]

The functions $H (z) : = \int_{T} K (z, ζ) d μ (ζ)$ are holomorphic on $D$ with $Re H = P [μ]$ , and $S_{μ} = e^{- H}$ is holomorphic, zero-free, with $∣ S_{μ} ∣ = e^{- P [μ]}$ and $S_{μ} (0) = e^{- μ (T)}$ ; $S_{μ}$ is a singular inner function exactly when $μ ⊥ m$ (Properties of the singular functions $S_{μ}$ , Inner, singular inner and outer functions).

[L4]

Maximum modulus: a holomorphic function on a domain with constant modulus is constant; a holomorphic function on a domain whose modulus has an interior maximum is constant (Local maximum modulus principle).

[L5]

For $θ \in H^{\infty}$ with $∣ θ^{*} ∣ = 1$ a.e. (an inner function), one has $∣ θ ∣ \leq 1$ on $D$ and $∥ θ ∥_{\infty} = 1$ , by the boundary-norm identity of the Fatou theorem for analytic $H^{\infty}$ ; the zero sequence of $θ$ satisfies the Blaschke condition, and $θ / B$ for the Blaschke product of its zeros is holomorphic and zero-free with nontangential boundary modulus $1$ a.e., while its modulus is bounded by $1$ by the maximum principle on expanding discs $∣ z ∣ < R$ with $∣ B_{N} (R ζ) ∣ \to 1$ (Fatou's boundary theorem for analytic Hardy spaces, The zero set of a Hardy function satisfies the Blaschke condition, Boundary values and zeros of a Blaschke product, F. Riesz factorization of a Hardy-space function, Blaschke factors and Blaschke products, Local maximum modulus principle).

Proof

technique · direct

1.1givenL1L2

The measure of the modulus. By [L1] the function $u = - \log ∣ S ∣$ is nonnegative harmonic with $u (0) < + \infty$ , so [L2] provides a unique finite nonnegative regular Borel measure $μ$ with $u = P [μ]$ , $μ (T) = u (0)$ .

2.1step 1.1L3L4algebra

$S$ is a unimodular constant times $S_{μ}$ . Let $H$ be the holomorphic function with $Re H = P [μ] = u$ from [L3]. Then $∣ S (z) e^{H (z)} ∣ = ∣ S (z) ∣ e^{Re H (z)} = e^{- u (z)} e^{u (z)} = 1 (z \in D),$ so the holomorphic function $S e^{H}$ has constant modulus $1$ ; by [L4] it is a constant $λ$ with $∣ λ ∣ = 1$ , that is, $S = λ e^{- H} = λ S_{μ}$ .

3.1step 2.1L3algebra

Singularity of $μ$ . Since $∣ S^{*} ∣ = 1$ a.e. and $∣ λ ∣ = 1$ , the relation $S = λ S_{μ}$ passes to the a.e. boundary values: $∣ S_{μ}^{*} ∣ = 1$ a.e. By the equivalence of [L3], this forces $μ ⊥ m$ .

4.1step 2.1step 3.1L2L3algebra

Uniqueness. If $S = λ S_{μ} = λ^{'} S_{μ^{'}}$ with unimodular $λ, λ^{'}$ and finite positive $μ, μ^{'} ⊥ m$ , then taking moduli gives $\log ∣ S ∣ = - P [μ] = - P [μ^{'}]$ , so $P [μ] = P [μ^{'}]$ and the uniqueness clause of the Herglotz representation [L2] gives $μ = μ^{'}$ ; then $λ = S (0) / S_{μ} (0) = λ^{'}$ .

4.2step 2.1step 3.1L5algebra

Every inner function factors. Let $θ$ be an inner function. The inner function cannot be identically zero, because its boundary modulus is $1$ almost everywhere. Let $(a_{n})$ be its zero sequence with multiplicity and $B$ its Blaschke product. By [L5] the sequence is a Blaschke sequence, and $S : = θ / B$ is holomorphic, zero-free, satisfies $∣ S ∣ \leq 1$ and has $∣ S^{*} ∣ = 1$ a.e. By steps 1.1, 2.1 and 3.1 there are $λ \in T$ and $μ ⊥ m$ with $S = λ S_{μ}$ , so $θ = B \cdot S = λ B S_{μ}$ : up to the unimodular constant $λ$ , $θ$ is the product of the Blaschke product $B$ and the singular inner function $S_{μ}$ .

5.1step 2.1step 3.1step 4.1step 4.2∎

Assembly. Steps 1.1, 2.1 and 3.1 produce the representation $S = λ S_{μ}$ with $μ ⊥ m$ for a zero-free $S$ , step 4.1 proves the asserted uniqueness, and step 4.2 gives the factorisation of a general inner function.

Depends on

Used by

Inner-outer factorisation of a Hardy-space function Theorem

Dependency tree · two levels

150 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

J. B. Garnett, Bounded Analytic Functions, revised first edition, Chapter II §6 (standard reference, not scraped)
R. K. Srivastava, Lecture Notes on Hardy Spaces (MA650, IIT Guwahati), §5.10 (standard reference, not scraped)