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.

A singular inner function generated by a point mass

Example

Let $μ = δ_{1}$ be the Dirac mass at the point $1 \in T$ . Then $μ$ is a finite positive measure singular with respect to $m$ and the associated function is the singular inner function $S (z) = \exp (- \frac{1 + z}{1 - z}) (z \in D),$ because $K (z, 1) = \frac{1 + z}{1 - z}$ . One has $∣ S (z) ∣ = e^{- P (z, 1)} = e^{- (1 - ∣ z ∣^{2}) / ∣ 1 - z ∣^{2}} \leq 1$ , $S (0) = e^{- 1} > 0$ , $S$ has no zeros in $D$ , and $∣ S^{*} (ζ) ∣ = 1$ for every $ζ \neq 1$ ; in particular $∣ S^{*} ∣ = 1$ $m$ -almost everywhere. The nontangential limit of $S$ at $ζ = 1$ is $0$ , because $P (z, 1) \to + \infty$ along every cone at $1$ . Thus $S$ is inner, nonconstant, and its boundary modulus fails to be $1$ only on the null set ${1}$ .

Facts & Assumptions

Given: The point $1 \in T$ , the Dirac measure $μ = δ_{1}$ , and the associated function $S = \exp (- H)$ with $H (z) = \int_{T} K (z, ζ) d δ_{1} (ζ) = K (z, 1)$ .

[F1]

The Dirac measure $δ_{1}$ is a probability measure and a finite positive Borel measure with $δ_{1} ({1}) = 1$ , and $m ({1}) = 0$ , so $δ_{1} ⊥ m$ (The Dirac set function at a point, A Dirac set function is a probability measure, The one-dimensional torus and its normalized Haar integral).

[F2]

$K (z, ζ) = (ζ + z) / (ζ - z)$ and $Re K (z, ζ) = P (z, ζ) = (1 - ∣ z ∣^{2}) / ∣ ζ - z ∣^{2}$ ; for $z = r e^{i ϕ}$ and $ζ = e^{i t}$ one has $P (z, ζ) = P_{r} (t - ϕ) > 0$ with $\frac{1}{2 π} \int_{0}^{2 π} P_{r} (θ) d θ = 1$ (Inner, singular inner and outer functions, The Poisson kernel on the unit disc, The Poisson kernel is positive, has total mass one, and concentrates at a boundary point).

[F3]

For a finite positive measure $ν$ , the function $S_{ν} = \exp (- \int K d ν)$ is holomorphic and zero-free with $∣ S_{ν} ∣ = e^{- P [ν]} \leq 1$ and $S_{ν} (0) = e^{- ν (T)}$ ; it is a singular inner function exactly when $ν ⊥ m$ , and then $∣ S_{ν}^{*} ∣ = 1$ $m$ -almost everywhere with nontangential limits existing a.e. (Properties of the singular functions $S_{μ}$ , Inner, singular inner and outer functions).

[F4]

The nontangential region at $1$ : for $A > 1$ , $Γ_{A} (1) = {z \in D : ∣ z - 1 ∣ < A (1 - ∣ z ∣)}$ , so along $Γ_{A} (1)$ one has $∣ 1 - z ∣ \leq A (1 - ∣ z ∣)$ (The circle maximal function and nontangential approach regions).

Verification

1.1givenF1F2algebra

The measure and the kernel value. By [F1], $δ_{1}$ is a finite positive measure singular with respect to $m$ ; evaluating the kernel at $ζ = 1$ gives $K (z, 1) = \frac{1 + z}{1 - z}$ , so $S (z) = \exp (- K (z, 1)) = \exp (- \frac{1 + z}{1 - z})$ .

2.1step 1.1F2algebra

Modulus, value at the origin, zero-freeness. By [F2], $Re K (z, 1) = P (z, 1) = \frac{1 - ∣ z ∣^{2}}{∣ 1 - z ∣^{2}}$ , hence $∣ S (z) ∣ = e^{- P (z, 1)} \leq 1$ and $S (0) = e^{- P (0, 1)} = e^{- 1} > 0$ ; $S$ is an exponential, hence zero-free.

3.1step 1.1step 2.1F3F4algebra∎

Cones at $1$ . Let $A > 1$ and $z \in Γ_{A} (1)$ . By [F4], $∣ 1 - z ∣ \leq A (1 - ∣ z ∣)$ , so $P (z, 1) = \frac{1 - ∣ z ∣^{2}}{∣ 1 - z ∣^{2}} \geq \frac{(1 - ∣ z ∣) (1 + ∣ z ∣)}{A^{2} (1 - ∣ z ∣)^{2}} = \frac{1 + ∣ z ∣}{A^{2} (1 - ∣ z ∣)} ⟶ + \infty$ as $∣ z ∣ \to 1$ ; therefore $∣ S (z) ∣ = e^{- P (z, 1)} \to 0$ and hence $S (z) \to 0$ along every cone at $1$ . Combined with the a.e. boundary values of [F3] (which give $∣ S^{*} ∣ = 1$ a.e. because $δ_{1} ⊥ m$ ) and the fact that $S^{*} (ζ) = 1$ -modulus for every $ζ \neq 1$ (where the exponent $- \frac{1 + z}{1 - z}$ has a finite limit), the boundary modulus of $S$ fails to be $1$ exactly on the null set ${1}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

80 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, example after Theorem 5.29 (standard reference, not scraped)