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.

The disc Bergman kernel from its monomial basis, with a reproducing check

Example

In $A^{2} (D)$ with Lebesgue area measure the functions $e_{k} (z) = \sqrt{(k + 1) / π} z^{k}$ , $k \geq 0$ , form a complete orthonormal system, and

$K_{D} (z, w) = \sum_{k \geq 0} \frac{k + 1}{π} z^{k} {\overline{w}}^{k} = \frac{1}{π (1 - z \overline{w})^{2}} .$

The reproducing property is checked directly on the monomials: for every $k \geq 0$ and $w \in D$ ,

$\int_{D} e_{k} (z) \overline{K_{D} (z, w)} d λ (z) = e_{k} (w) .$

Facts & Assumptions

[A1]

The only choice assumption is ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )), inherited through the Bergman Hilbert-space, kernel and expansion suppliers; no full Axiom of Choice is used.

[F1]

The monomials $z^{k}$ , $k \geq 0$ , have squared norms $∥ z^{k} ∥_{A^{2} (D)}^{2} = π / (k + 1)$ and the normalized monomials form a complete orthonormal system of $A^{2} (D)$ (Weighted monomial integrals and monomial norms for the disc, ball and polydisc, Monomials form complete orthogonal systems of the Bergman spaces of the disc, the ball and the polydisc).

[F2]

For every complete orthonormal system $(e_{j})$ of $A^{2} (Ω)$ one has $K_{Ω} (z, w) = \sum_{j} e_{j} (z) \overline{e_{j} (w)}$ , the finite-subset sums converge in $A^{2} (Ω)$ to $K_{Ω} (\cdot, w)$ , and the series converges absolutely and uniformly on compact subsets ( $A^{2} (Ω)$ is closed, and the Bergman kernel is the sum over any complete orthonormal system).

[F3]

The disc Bergman kernel is $K_{D} (z, w) = \frac{1}{π (1 - z \overline{w})^{2}}$ and it satisfies the reproducing identity $⟨ f, K_{D} (\cdot, w) ⟩ = f (w)$ for every $f \in A^{2} (D)$ (Bergman kernels of the disc, ball and polydisc, and Szegő kernels of the disc and ball, Reproducing property, Bergman projection and the extremal characterization).

[F4]

The integral pairing is continuous in its second variable: $∣ ⟨ f, g ⟩ ∣ \leq ∥ f ∥_{2} ∥ g ∥_{2}$ (Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs, The Bergman space $A^{2} (Ω)$ and the Bergman kernel).

[F5]

Natural powers are defined recursively, so $z^{k}$ and $∣ z ∣^{2 k} = z^{k} {\overline{z}}^{k}$ have their stated meanings (Integer powers in the complex field).

Verification

technique · direct, using the complete orthonormal monomial system

Given: ${A C}_{ω}$ , the unit disc with Lebesgue area measure, and $k \geq 0$ , $w \in D$ .

1.1A1F1F5given

By [F1] the family $e_{k} (z) = \sqrt{(k + 1) / π} z^{k}$ is a complete orthonormal system of $A^{2} (D)$ , with $∥ z^{k} ∥_{2}^{2} = π / (k + 1)$ ; since $z, w \in D$ we have $∣ z \overline{w} ∣ < 1$ for the geometric series.

2.1A1F1F2F3step 1.1

By [F2] applied to this complete orthonormal system, $K_{D} (z, w) = \sum_{k \geq 0} e_{k} (z) \overline{e_{k} (w)} = \frac{1}{π} \sum_{k \geq 0} (k + 1) (z \overline{w})^{k}$ , and by [F3] this sum equals $\frac{1}{π (1 - z \overline{w})^{2}}$ ; this is the displayed series identity.

3.1A1F1F2F4step 2.1

Fix $k$ and $w$ . The holomorphic Fourier sums $T_{N} : = \sum_{j \leq N} \overline{e_{j} (w)} e_{j}$ converge in $A^{2} (D)$ to $K_{D} (\cdot, w)$ by [F2]. Continuity of the pairing [F4] gives $\int_{D} e_{k} (z) \overline{K_{D} (z, w)} d λ (z) = \lim_{N} ⟨ e_{k}, T_{N} ⟩$ . For $N \geq k$ , conjugate-linearity in the second variable and orthonormality give $⟨ e_{k}, T_{N} ⟩ = \sum_{j \leq N} e_{j} (w) ⟨ e_{k}, e_{j} ⟩ = e_{k} (w)$ . This proves the reproducing integral.

4.1A1F1F2F3F4step 2.1step 3.1∎

Step 2.1 identifies the displayed series with the disc Bergman kernel of [F3], and step 3.1 verifies the reproducing identity on every monomial. Since the monomial span is dense by [F1] and both sides of the reproducing identity are continuous in the first variable by [F4], the check extends to all of $A^{2} (D)$ and agrees with the general reproducing theorem.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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