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.

Properties of the singular functions $S_{μ}$

Statement

Assume countable choice, as in the defining circle and singular-function conventions. Let $μ$ be a finite positive Borel measure on $T$ and let $S_{μ} (z) = \exp (- \int_{T} K (z, ζ) d μ (ζ))$ . Then $S_{μ}$ is holomorphic and zero-free on $D$ , $\log ∣ S_{μ} ∣ = - P [μ]$ , $∣ S_{μ} ∣ \leq 1$ , and $S_{μ} (0) = e^{- μ (T)} \in (0, 1]$ . Moreover $S_{μ}$ has finite nontangential limits $S_{μ}^{*} (ζ)$ for $m$ -almost every $ζ \in T$ , with $∣ S_{μ}^{*} ∣ = e^{- \lim_{r ↑ 1} P [μ] (r ζ)}$ , and the following are equivalent:

(i) $μ ⊥ m$ ; (ii) $∣ S_{μ}^{*} ∣ = 1$ $m$ -almost everywhere; (iii) $P [μ] (r ζ) \to 0$ for $m$ -almost every $ζ \in T$ .

Consequently $S_{μ}$ is a singular inner function exactly when $μ ⊥ m$ .

Facts & Assumptions

Given: Countable choice and a finite positive Borel measure $μ$ on the torus $T$ with normalized Haar measure $m$ , the kernel $K (z, ζ) = (ζ + z) / (ζ - z)$ and the function $S_{μ} = e^{- H}$ with $H (z) : = \int_{T} K (z, ζ) d μ (ζ)$ .

[L1]

$K$ is continuous and bounded on $T$ for fixed $z$ , $Re K (z, ζ) = P (z, ζ)$ is the Poisson kernel, and $\int_{T} P (z, ζ) d m (ζ) = 1$ ; the Poisson integral $P [μ] (z) = \int P (z, ζ) d μ$ is harmonic with $P [μ] \geq 0$ and $P [μ] (0) = μ (T)$ (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, The Poisson integral of a finite complex boundary measure).

[L2]

The expansion $K (z, ζ) = 1 + 2 \sum_{n \geq 1} z^{n} ζ^{- n}$ converges absolutely and locally uniformly for $∣ z ∣ < 1$ , $∣ ζ ∣ = 1$ , so termwise integration against the finite measure $μ$ exhibits $H$ as a locally uniform limit of holomorphic polynomials, hence holomorphic on $D$ ; $\exp$ of a holomorphic function is holomorphic, and the exponential is never zero (A complex power series converges absolutely and uniformly on every closed subdisc strictly inside its disc of convergence, Inner, singular inner and outer functions, The complex exponential by its power series).

[L3]

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)

[L4]

Under countable choice every finite positive Borel circle measure has a decomposition $μ = h m + μ_{s}$ with integrable Borel $h \geq 0$ and $μ_{s}$ carried by a Haar-null Borel set. (Finite positive circle measures admit a Lebesgue decomposition under countable choice, A positive, signed, or complex measure concentrated on a measurable set)

[L5]

The Poisson integral of $h \in L^{1} (T, m)$ converges to $h (ζ)$ at $m$ -almost every $ζ$ within every cone $Γ_{A} (ζ)$ , $A > 1$ (Fatou limits for Poisson extensions of L1 boundary data).

[L6]

For a finite positive singular circle measure, its Poisson integral tends nontangentially to zero almost everywhere under countable choice. The proof uses compact approximation of its singular carrier and the weak maximal estimate; no small-closure assertion for an open set is used. (Singular circle measures have Poisson integral tending nontangentially to zero almost everywhere)

Proof

technique · direct

1.1givenL1L2algebra

Holomorphy, modulus and value at the origin. By [L2] the function $H$ is holomorphic on $D$ with $Re H = P [μ]$ by [L1]; hence $S_{μ} = e^{- H}$ is holomorphic and zero-free, $∣ S_{μ} (z) ∣ = e^{- Re H (z)} = e^{- P [μ] (z)} \leq 1$ because $P [μ] \geq 0$ , and $S_{μ} (0) = e^{- H (0)} = e^{- μ (T)} \in (0, 1]$ . Also $\log ∣ S_{μ} ∣ = - P [μ]$ .

2.1step 1.1L1L3L4L5L6algebra

Nontangential limits. By step 1.1, $S_{μ}$ is bounded holomorphic, so [L3] gives finite nontangential limits $S_{μ}^{*}$ almost everywhere. To identify their modulus, decompose $μ = h m + μ_{s}$ by [L4]. The Poisson integral is the sum $P [h] + P [μ_{s}]$ by [L1]; [L5] gives $P [h] \to h$ nontangentially almost everywhere, and [L6] gives $P [μ_{s}] \to 0$ . On their common full-measure set, $P [μ] \to h$ , so continuity of the real exponential in the identity of step 1.1 gives $∣ S_{μ}^{*} ∣ = e^{- h} = e^{- \lim_{r ↑ 1} P [μ] (r ζ)}$ . The radial limit agrees with the cone limits.

2.2step 1.1L6

(i) implies (iii). If $μ ⊥ m$ , [L6] gives $P [μ] (z) \to 0$ within every cone at almost every circle point, hence in particular along radii. Thus (iii) holds, including $μ = 0$ .

3.1step 2.1algebra

(iii) implies (ii). If $P [μ] (r ζ) \to 0$ for $m$ -almost every $ζ$ , then step 2.1 gives $∣ S_{μ}^{*} (ζ) ∣ = e^{0} = 1$ for $m$ -almost every $ζ$ , which is (ii).

3.2step 2.1L4L5algebra

(ii) implies (i). Assume (ii) and decompose $μ = h m + μ_{s}$ as in [L4]. Since $h \geq 0$ , one has $P [h] \leq P [μ]$ pointwise, and by [L5], $P [h] (r ζ) \to h (ζ)$ for $m$ -almost every $ζ$ . By step 2.1, (ii) says $P [μ] (r ζ) \to 0$ a.e.; hence $0 \leq h (ζ) \leq {lim inf}_{r} P [μ] (r ζ) = 0$ a.e., so $h = 0$ $m$ -almost everywhere. Therefore $μ = μ_{s}$ is concentrated on an $m$ -null set, that is, $μ ⊥ m$ , which is (i).

4.1step 1.1step 2.1step 2.2step 3.2algebra∎

Assembly. Step 1.1 gives holomorphy, zero-freeness, the modulus identity and the value at $0$ ; step 2.1 gives the a.e. nontangential limits and the displayed modulus formula; steps 2.2, 3.1 and 3.2 prove (i) $\Rightarrow$ (iii) $\Rightarrow$ (ii) $\Rightarrow$ (i), so the three conditions are equivalent. By the definition of singular inner function, $S_{μ}$ is a singular inner function exactly when $μ ⊥ m$ , i.e. exactly when the equivalent conditions hold.

Depends on

Used by

Cited to discharge well-definedness by Inner, singular inner and outer functions.

Dependency tree · two levels

126 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)

Properties of the singular functions SμSμ​