Alphabeta Math
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.

Boundary values and zeros of a Blaschke product

Statement

Let (an)n≥1 be a Blaschke sequence with Blaschke product B=∏nban and partial products BN=∏n≤Nban. Then:

(i) ∣B(z)∣≤1 for every z∈D, and the zeros of B are exactly the points an, with multiplicity;

(ii) for every N, B/BN is the Blaschke product of the tail (an)n>N; it is holomorphic on D, satisfies ∣(B/BN)(z)∣≤1, and (B/BN)(0)=∏n>N∣an∣, a product that is eventually positive and tends to 1 as N→∞;

(iii) B has finite nontangential limits B∗(ζ) for m-almost every ζ∈T, and ∣B∗(ζ)∣=1 for m-almost every ζ. In particular B≢0.

Facts & Assumptions

Given: Countable choice and a Blaschke sequence (an)n≥1 with ∑n(1−∣an∣)<+∞, its Blaschke product B, and the partial products BN.

[L1]

The product converges normally: B is holomorphic on D with zeros exactly the an counted with multiplicity, and ∣B(z)∣≤1; for each N the quotient B/BN is the Blaschke product of the tail and is holomorphic with ∣B/BN∣≤1, while BN is holomorphic on a neighbourhood of the closed disc with ∣BN(ζ)∣=1 for every ζ∈T; also ba(0)=∣a∣ and ∣ba∣≤1 for every a∈D (Blaschke factors and Blaschke products, Normally convergent products define holomorphic functions with the expected zeros).

[L2]

Radii R and moduli: for the tail products, (B/BN)(0)=∏n>N∣an∣; since ∑n(1−∣an∣)<+∞ we have ∣an∣→1, so all but finitely many an have ∣an∣≥1/2, and for those log⁡(1/∣an∣)≤2(1−∣an∣); hence ∏n>N∣an∣=exp⁡(−∑n>Nlog⁡(1/∣an∣)) is eventually positive and tends to 1 as N→∞ (The zero set of a Hardy function satisfies the Blaschke condition, Blaschke factors and Blaschke products).

[L3]

If w is holomorphic on a neighbourhood of the closed disc of radius r<1, then ∣w(0)∣≤∫T∣w(rζ)∣ dm(ζ): ∣w∣ is subharmonic by Positive powers of the modulus of a holomorphic function are subharmonic with p=1, its Poisson modification on D(0,r) majorizes it and has the mean value of ∣w∣ on the circle at its centre, and for r=R this is the mean inequality for holomorphic functions of Radial p-means of a holomorphic function are nondecreasing (Poisson modification on a compactly contained disc, Poisson modification is subharmonic and majorizes the original function, Radial p-means of a holomorphic function are nondecreasing).

[L4]

Under countable choice every bounded holomorphic disc function has finite nontangential limits almost everywhere. (Bounded holomorphic disc functions have Poisson boundary data and Fatou limits under countable choice, The Axiom of Countable Choice (ACω))

[L5]

Domination and convergence: if ∣gr∣≤1 for all r and gr→g m-almost everywhere as r↑1, then ∫gr dm→∫g dm; the kernel has unit mass in the torus normalization and m is a probability measure (Dominated convergence, The Poisson kernel is positive, has total mass one, and concentrates at a boundary point, The one-dimensional torus and its normalized Haar integral).

Proof

technique · direct
1.1givenL1L2

Items (i) and (ii). [L1] gives ∣B∣≤1 with the stated zeros and the holomorphy and bound for B/BN. For each N the value at the origin is (B/BN)(0)=∏n>N∣an∣, whose factors are all nonzero once N exceeds the largest index with an=0. The tail need not be empty. By [L2] its product is eventually positive and tends to 1; for a finite sequence the empty tail equals 1.

2.1step 1.1L4

Nontangential limits exist and are bounded. Since ∣B∣≤1 and B is holomorphic, [L4] gives finite nontangential limits almost everywhere; hence B∗(ζ):=lim⁡Γ∋z→ζB(z) exists and satisfies ∣B∗(ζ)∣≤1 for m-almost every ζ.

2.2step 1.1L1L3algebra

The mean inequality for each tail. Fix N and 0<r<1. The function wN:=B/BN is holomorphic on a neighbourhood of the closed disc of radius r by [L1], so [L3] gives ∏n>N∣an∣=∣(B/BN)(0)∣≤∫T∣(B/BN)(rζ)∣ dm(ζ).

3.1step 1.1step 2.1step 2.2L1L5algebra

Letting the radius tend to the boundary. For m-almost every ζ one has B(rζ)→B∗(ζ) as r↑1, and BN extends continuously to D‾ with ∣BN(ζ)∣=1 on T by [L1], so (B/BN)(rζ)→B∗(ζ)/BN(ζ) along these radii, a limit of modulus ∣B∗(ζ)∣. Since ∣B/BN∣≤1, [L5] applies and gives ∏n>N∣an∣≤∫T∣B∗(ζ)∣ dm(ζ)≤1.

4.1step 3.1L2algebra∎

Conclusion. Letting N→∞ in step 3.1 and using that ∏n>N∣an∣→1 by [L2] gives 1≤∫T∣B∗∣ dm≤1, so ∫T∣B∗∣ dm=1; since ∣B∗∣≤1 m-almost everywhere, the nonnegative function 1−∣B∗∣ has integral 0, hence vanishes m-almost everywhere by A nonnegative measurable function has integral 0 exactly when it vanishes almost everywhere, that is, ∣B∗∣=1 m-almost everywhere. In particular the boundary function is not identically zero, so B≢0.

Depends on

Used by

Cited to discharge well-definedness by Blaschke factors and Blaschke products.

Dependency tree · two levels

115 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