ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08

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.

Bergman versus Szegő normalization on the disc

Example

Let $D \subseteq C$ be the unit disc with Lebesgue area measure $λ_{2}$ , and let $T = \partial D$ carry the normalized Haar probability $m$ of The one-dimensional torus and its normalized Haar integral. The diagonal Bergman and Szegő kernels of Bergman kernels of the disc, ball and polydisc, and Szegő kernels of the disc and ball are

$K_{D} (z, z) = \frac{1}{π (1 - ∣ z ∣^{2})^{2}}, S_{D} (z, z) = \frac{1}{1 - ∣ z ∣^{2}}, z \in D,$

the first relative to Lebesgue area measure on $D$ and the second relative to $m$ . In particular $K_{D} (0, 0) = 1 / π$ while $S_{D} (0, 0) = 1$ . The two kernels are reproducing kernels of different Hilbert spaces — $A^{2} (D)$ for the area pairing, and the disc Hardy space of boundary traces for the Haar pairing — and their boundary blow-up exponents are $2$ and $1$ : the two normalizations are comparable only after the measure is declared.

Facts & Assumptions

[A1]

The only choice assumption is ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )), inherited from the model-kernel theorem and from the Bergman and Szegő definitions; no full Axiom of Choice is used.

[F1]

Under ${A C}_{ω}$ , $A^{2} (D)$ is the space of $L^{2}$ classes with a holomorphic representative for the area pairing, and its first-variable-linear kernel $K_{D}$ is the Riesz kernel of evaluation; for a Szegő-regular pair $(Ω, σ)$ the Szegő kernel is built from the Riesz representers of the extended boundary evaluations (The Bergman space $A^{2} (Ω)$ and the Bergman kernel, The Hardy boundary space, Szegő projection and Szegő kernel on a smoothly bounded domain).

[F2]

The disc pair $(D, μ_{T})$ is Szegő-regular, and the model theorem gives $K_{D} (z, w) = \frac{1}{π (1 - z \overline{w})^{2}}$ and $S_{D} (z, w) = \frac{1}{1 - z \overline{w}}$ (Bergman kernels of the disc, ball and polydisc, and Szegő kernels of the disc and ball).

[F3]

The classical disc Hardy class $H^{2} (D)$ consists of the holomorphic functions whose radial $L^{2}$ means are bounded, and $m$ is the normalized Haar probability carried by the boundary torus of the disc pair (Analytic Hardy spaces on the unit disc, The one-dimensional torus and its normalized Haar integral).

Verification

technique · direct substitution in the model formulas

Given: ${A C}_{ω}$ , the unit disc with its area measure, and the torus with normalized Haar measure.

1.1A1F2givenalgebra

Set $w = z$ in the two formulas of [F2]. Since $1 - z \overline{z} = 1 - ∣ z ∣^{2} > 0$ on $D$ , the diagonal values are $K_{D} (z, z) = \frac{1}{π (1 - ∣ z ∣^{2})^{2}}$ and $S_{D} (z, z) = \frac{1}{1 - ∣ z ∣^{2}}$ ; at $z = 0$ these are $1 / π$ and $1$ .

1.2A1F1F2F3

By [F1] the first kernel reproduces point evaluations in $A^{2} (D)$ for the area pairing, while the second reproduces the extended evaluations of the Szegő-regular pair $(D, μ_{T})$ , whose Hardy space is its boundary-trace closure; [F3] records the classical radial-mean form of the disc Hardy class against the same normalized Haar boundary measure.

2.1F1F2step 1.1∎

As $∣ z ∣ \to 1$ , the formulas of step 1.1 show $K_{D} (z, z) = \frac{1}{π} (1 - ∣ z ∣^{2})^{- 2}$ and $S_{D} (z, z) = (1 - ∣ z ∣^{2})^{- 1}$ , so the boundary blow-up exponents are $2$ and $1$ . Their ratio $K_{D} (z, z) / S_{D} (z, z) = \frac{1}{π (1 - ∣ z ∣^{2})}$ is unbounded on $D$ ; in particular the two diagonal kernels are not equal, so neither normalization may be read off the other without declaring which measure is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

107 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

Jiří Lebl, Tasty Bits of Several Complex Variables (book) (standard reference, not scraped)