ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

Finite Blaschke products

Example

For $a_{1}, \dots, a_{N} \in D$ let $B (z) = \prod_{j = 1}^{N} b_{a_{j}} (z)$ be the finite Blaschke product of the normalized factors $b_{a}$ of Blaschke factors and Blaschke products. Then $B$ is a rational function holomorphic on an open neighbourhood of $\overline{D}$ , $∣ B (ζ) ∣ = 1$ for every $ζ \in T$ , $B (0) = \prod_{j = 1}^{N} ∣ a_{j} ∣$ , and the zeros of $B$ in $D$ are exactly $a_{1}, \dots, a_{N}$ with multiplicity; in particular $∣ B (z) ∣ < 1$ for every $z \in D$ when $N \geq 1$ (a nonconstant finite Blaschke product has no interior point of modulus one).

For $a_{1} = 1 / 2$ , $a_{2} = - 1 / 2$ one computes $b_{1 / 2} (z) = \frac{1 / 2 - z}{1 - z / 2}$ and $b_{- 1 / 2} (z) = \frac{1 / 2 + z}{1 + z / 2}$ (the normalization $\overline{a} / ∣ a ∣$ of the second factor is $- 1$ ), so $B (z) = b_{1 / 2} (z) b_{- 1 / 2} (z) = \frac{1 / 4 - z^{2}}{1 - z^{2} / 4},$ with $B (0) = 1 / 4$ and $B (1) = B (- 1) = - 1$ (the latter values illustrate $∣ B ∣ = 1$ on the boundary).

Facts & Assumptions

Given: Points $a_{1}, \dots, a_{N} \in D$ and the finite product $B = \prod_{j = 1}^{N} b_{a_{j}}$ of normalized Blaschke factors.

[F1]

Each normalized factor is $b_{a} = \frac{\overline{a}}{∣ a ∣} φ_{a}$ for $a \neq 0$ and $b_{0} (z) = z$ , with $φ_{a} (z) = \frac{a - z}{1 - \overline{a} z}$ holomorphic on a neighbourhood of $\overline{D}$ ; $∣ b_{a} (z) ∣ \leq 1$ on $D$ , $∣ b_{a} (ζ) ∣ = 1$ on $T$ , $b_{a} (0) = ∣ a ∣$ , and $b_{a}$ has the unique zero $a$ in $D$ (Blaschke factors and Blaschke products, The unit disc, the upper half-plane, and Blaschke factors, Boundary values and zeros of a Blaschke product).

[F2]

If a holomorphic function on a domain has a local maximum of its modulus at an interior point, it is constant there; equivalently $∣ f ∣$ attains no strict interior maximum unless $f$ is constant (Local maximum modulus principle).

[F3]

For $∣ ζ ∣ = 1$ one has $∣ a_{j} - ζ ∣ = ∣ 1 - \overline{a_{j}} ζ ∣$ , and moduli multiply over finite products (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive, Real and imaginary parts, complex conjugation, and modulus).

Verification

1.1F1algebra

Rationality and holomorphy near the closed disc. Each factor $b_{a}$ is a quotient of the linear functions $a - z$ and $1 - \overline{a} z$ times the constant $\overline{a} / ∣ a ∣$ (with $b_{0} (z) = z$ ), and its denominator is zero-free on $\overline{D}$ because $∣ \overline{a} z ∣ \leq ∣ a ∣ < 1$ . Hence each $b_{a_{j}}$ is holomorphic on a neighbourhood of $\overline{D}$ , and the finite product $B$ is a rational function holomorphic on such a neighbourhood.

1.2F1F3algebra

Boundary modulus and value at the origin. By [F1] and [F3], $∣ B (ζ) ∣ = \prod_{j} ∣ b_{a_{j}} (ζ) ∣ = 1$ for $ζ \in T$ , and $B (0) = \prod_{j} b_{a_{j}} (0) = \prod_{j} ∣ a_{j} ∣$ .

1.3F1algebra

Zeros. The zeros of a finite product are the union of the zeros of its factors with multiplicity; by [F1] the zero of $b_{a_{j}}$ in $D$ is exactly $a_{j}$ , and $b_{a_{j}}$ has no other zero in $D$ . Hence the zeros of $B$ in $D$ are exactly $a_{1}, \dots, a_{N}$ with multiplicity.

2.1step 1.2F1F2algebra

Strict decrease of the modulus when $N \geq 1$ . Assume $N \geq 1$ and suppose $∣ B (z_{0}) ∣ = 1$ for some $z_{0} \in D$ . Since $∣ B ∣ \leq \prod_{j} \sup_{D} ∣ b_{a_{j}} ∣ \leq 1$ on $D$ , $∣ B ∣$ has at $z_{0}$ a maximum equal to $1$ , so $B$ is constant by [F2]; a constant value of modulus $1$ would give $∣ B (0) ∣ = 1$ , but $∣ B (0) ∣ = \prod_{j} ∣ a_{j} ∣ < 1$ because $N \geq 1$ and every $∣ a_{j} ∣ < 1$ , a contradiction. Hence $∣ B (z) ∣ < 1$ for every $z \in D$ whenever $N \geq 1$ .

3.1F1algebra∎

The explicit case $a_{1} = 1 / 2$ , $a_{2} = - 1 / 2$ . Here $\overline{(1 / 2)} / ∣ 1 / 2 ∣ = 1$ , so $b_{1 / 2} (z) = φ_{1 / 2} (z) = \frac{1 / 2 - z}{1 - z / 2}$ , while $\overline{(- 1 / 2)} / ∣ - 1 / 2 ∣ = - 1$ , so $b_{- 1 / 2} (z) = - \frac{- 1 / 2 - z}{1 + z / 2} = \frac{1 / 2 + z}{1 + z / 2}$ . Multiplying and expanding $(1 / 2 - z) (1 / 2 + z) = 1 / 4 - z^{2}$ and $(1 - z / 2) (1 + z / 2) = 1 - z^{2} / 4$ gives $B (z) = \frac{1 / 4 - z^{2}}{1 - z^{2} / 4}$ , whence $B (0) = 1 / 4$ , $B (1) = \frac{- 3 / 4}{3 / 4} = - 1$ and $B (- 1) = - 1$ , in agreement with $∣ B (1) ∣ = ∣ B (- 1) ∣ = 1$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

28 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

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