ExampleConstruction: Literature-sourcedVerification: 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.

Inner-outer factorization of a rational function with one interior zero

Example

Fix $a \in D$ , $a \neq 0$ , and put $f (z) : = \frac{z - a}{1 - \overline{a} z} \cdot \frac{1 + z}{2} .$ Then $f$ is a rational function holomorphic on a neighbourhood of $\overline{D}$ ; its only zero in $D$ is $a$ (simple), its only pole is $1 / \overline{a}$ outside the closed disc, and $∣ f^{*} ∣ = \frac{∣ 1 + ζ ∣}{2}$ on $T$ . In the normalized inner-outer factorization of Inner-outer factorisation of a Hardy-space function one has $B = b_{a}, μ = 0 (S_{μ} = 1), F (z) = \frac{1 + z}{2}, λ = - \frac{a}{∣ a ∣},$ because $\frac{z - a}{1 - \overline{a} z} = - \frac{a}{∣ a ∣} b_{a} (z)$ and $F$ is outer with $F (0) = \frac{1}{2} > 0$ and $∣ F^{*} ∣ = \frac{∣ 1 + ζ ∣}{2}$ . Thus $f = λ B F$ , a pure Blaschke-times-outer factorization with trivial singular factor, and $∥ f ∥_{H^{\infty}} = 1$ , while $∥ B ∥_{H^{\infty}} = 1$ and $∥ F ∥_{H^{\infty}} = 1$ .

Facts & Assumptions

Given: A point $a \in D$ , $a \neq 0$ , and the rational function $f (z) = \frac{z - a}{1 - \overline{a} z} \cdot \frac{1 + z}{2}$ . The countable-choice regime of Analytic Hardy spaces on the unit disc and Inner, singular inner and outer functions is in force (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

The Blaschke factor $φ_{a} (z) = \frac{a - z}{1 - \overline{a} z}$ is holomorphic on a neighbourhood of $\overline{D}$ , $φ_{a}$ is a biholomorphic self-map of $D$ with $φ_{a} (a) = 0$ and $∣ φ_{a} (ζ) ∣ = 1$ for $ζ \in T$ ; the normalized factor is $b_{a} = \frac{\overline{a}}{∣ a ∣} φ_{a}$ , so $\frac{z - a}{1 - \overline{a} z} = - \frac{a}{∣ a ∣} b_{a} (z)$ because $∣ a ∣ / \overline{a} = a / ∣ a ∣$ (Blaschke factors and Blaschke products, The unit disc, the upper half-plane, and Blaschke factors, Boundary values and zeros of a Blaschke product, Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F2]

Outer functions: an outer function with prescribed boundary modulus $H$ and positive value at the origin is unique; $(1 + z) / 2$ is outer because $\log ∣ (1 + z) / 2 ∣ = P [\log ∣ (1 + ζ) / 2 ∣]$ , the computation of the preceding example with $ζ$ replaced by $- ζ$ , and $(1 + z) / 2$ is holomorphic and zero-free on $D$ with $(1 + 0) / 2 = 1 / 2 > 0$ and $∣ (1 + ζ) / 2 ∣ = ∣ 1 + ζ ∣ / 2$ on $T$ (An outer function with a prescribed power of a vanishing modulus, Properties of outer functions, Inner, singular inner and outer functions).

[F3]

The rational function $f$ is holomorphic on a neighbourhood of $\overline{D}$ : the denominator $1 - \overline{a} z$ does not vanish for $∣ z ∣ \leq 1$ because $∣ \overline{a} z ∣ \leq ∣ a ∣ < 1$ ; the numerator $z - a$ vanishes exactly at $z = a \in D$ ; and the second factor $(1 + z) / 2$ vanishes at $z = - 1 \notin D$ and is nonzero on $D$ (Complex polynomials are entire with the power-rule derivative, and rational functions are holomorphic wherever their denominator is nonzero).

[F4]

In a normalized factorization $f = λ B S_{ν} G$ , the normalized Blaschke product $B$ is prescribed by the zeros, $G = [∣ f^{*} ∣]$ is prescribed by the boundary modulus and $G (0) > 0$ , and $S_{ν} (0) = e^{- ν (T)} > 0$ for a finite positive singular measure $ν$ . These are the normalization conventions used in the Example, not an invocation of the general AC-qualified existence or uniqueness theorem. For this explicit function, existence and uniqueness are proved directly in step 3.1 from Blaschke factors and Blaschke products and Inner, singular inner and outer functions.

Verification

1.1givenF3algebra

Basic properties of $f$ . By [F3], $f$ is rational and holomorphic on a neighbourhood of $\overline{D}$ ; its only zero in $D$ is the simple zero $a$ of the first factor (the second factor $(1 + z) / 2$ has its zero at $- 1 \notin D$ ), and its only pole is at $z = 1 / \overline{a}$ , which lies outside the closed disc because $∣ 1 / \overline{a} ∣ = 1 / ∣ a ∣ > 1$ .

2.1step 1.1F1algebra

Boundary modulus. On $T$ , $∣ φ_{a} (ζ) ∣ = 1$ by [F1] and $∣ 1 + ζ ∣$ is the modulus of the second numerator, so $∣ f^{*} (ζ) ∣ = 1 \cdot \frac{∣ 1 + ζ ∣}{2} = \frac{∣ 1 + ζ ∣}{2}$ .

3.1step 2.1F1F2F4algebra

The factors and their direct uniqueness. Write $f = (- \frac{a}{∣ a ∣} b_{a}) \cdot \frac{1 + z}{2}$ by [F1]. The factor $F (z) : = \frac{1 + z}{2}$ is outer with $F (0) = \frac{1}{2} > 0$ and $∣ F^{*} ∣ = ∣ f^{*} ∣$ by [F2] and step 2.1. Thus the displayed factors $λ = - a / ∣ a ∣$ , $B = b_{a}$ , $μ = 0$ and $S_{μ} = 1$ give a normalized factorization directly. For uniqueness, let $f = \tilde{λ} \tilde{B} S_{ν} G$ be any factorization with the normalizations [F4]. Its zero data force $\tilde{B} = b_{a}$ , and its outer normalization forces $G = [∣ f^{*} ∣] = F$ by [F2]. After holomorphic cancellation at $a$ , $\tilde{λ} S_{ν} = f / (b_{a} F) = - a / ∣ a ∣$ , so $∣ S_{ν} ∣ = 1$ throughout the disc. At zero, $e^{- ν (T)} = S_{ν} (0) = 1$ gives $ν (T) = 0$ ; positivity gives $ν (E) = 0$ for every Borel $E$ , hence $ν = 0$ , $S_{ν} = 1$ and $\tilde{λ} = - a / ∣ a ∣$ . This proves the asserted normalized uniqueness without the general AC representation theorem.

4.1step 3.1F1algebra∎

Norms. For $z \in D$ one has $∣ b_{a} (z) ∣ \leq 1$ and $∣ 1 + z ∣ \leq 2$ , so $∣ f (z) ∣ = ∣ b_{a} (z) ∣ \frac{∣ 1 + z ∣}{2} \leq 1$ ; and $∥ B ∥_{H^{\infty}} = 1$ , $∥ F ∥_{H^{\infty}} = \sup_{z \in D} \frac{∣ 1 + z ∣}{2} = 1$ , with both suprema approached as $z \to 1$ , where also $∣ b_{a} (z) ∣ \to ∣ b_{a} (1) ∣ = 1$ . Hence $∥ f ∥_{H^{\infty}} = 1 = ∥ B ∥_{H^{\infty}} ∥ F ∥_{H^{\infty}}$ , consistent with the general bound $∥ f ∥_{\infty} \leq ∥ B ∥_{\infty} ∥ S_{μ} ∥_{\infty} ∥ F ∥_{\infty}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

67 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 §5, Corollary 5.7 (standard reference, not scraped)
R. K. Srivastava, Lecture Notes on Hardy Spaces (MA650, IIT Guwahati), §5.10, Theorem 5.32-5.33 (standard reference, not scraped)