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 upper half-plane Bergman kernel by biholomorphic transport

Example

Let $H = {z \in C : Im z > 0}$ and let $φ : H \to D$ , $φ (z) = \frac{z - i}{z + i}$ , be the Möbius biholomorphism. Then

$K_{H} (z, w) = \frac{- 1}{π (z - \overline{w})^{2}},$

and in particular $K_{H} (z, z) = \frac{1}{4 π (Im z)^{2}}$ ; the reproducing property and the diagonal positivity are transported from the disc.

Facts & Assumptions

[A1]

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

[F1]

For complex $a, b, c, d$ with $a d - b c \neq 0$ , the associated Möbius transformation $z \mapsto \frac{a z + b}{c z + d}$ is defined on the finite plane away from its pole and is a biholomorphism of the Riemann sphere whose inverse is again a Möbius transformation (Möbius transformations of the Riemann sphere, Every Möbius transformation is a biholomorphism of the Riemann sphere).

[F2]

The unit disc and the upper half-plane are $D = {∣ z ∣ < 1}$ and $H = {Im z > 0}$ (The unit disc, the upper half-plane, and Blaschke factors).

[F3]

For $z = x + i y$ one has $∣ z \pm i ∣^{2} = ∣ z ∣^{2} + 1 \pm 2 Im z$ , because $∣ z ∣^{2} = z \overline{z}$ and $Im z = \frac{z - \overline{z}}{2 i}$ (Real and imaginary parts, complex conjugation, and modulus, $C = R [x] / (x^{2} + 1)$ is a field, every element is uniquely $a + b i$ , and every nonzero element has inverse $(a - b i) / (a^{2} + b^{2})$ , Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F4]

A biholomorphism $F : Ω \to Ω^{'}$ of domains satisfies $K_{Ω} (z, w) = J_{F} (z) K_{Ω^{'}} (F (z), F (w)) \overline{J_{F} (w)}$ with $J_{F} = \det_{C} D F \neq 0$ , and pullback along $F$ is a unitary isomorphism of the Bergman spaces (Transformation law of the Bergman kernel under a biholomorphism).

[F5]

The disc Bergman kernel is $K_{D} (ζ, η) = \frac{1}{π (1 - ζ \overline{η})^{2}}$ , it reproduces the corresponding $A^{2}$ space, and it is the unique such kernel (Bergman kernels of the disc, ball and polydisc, and Szegő kernels of the disc and ball).

[F6]

A biholomorphism is a bijective holomorphic map whose inverse is holomorphic (Biholomorphic maps between open sets in $C^{m}$ ).

Verification

technique · direct, transporting the disc kernel along an explicit Möbius map

Given: ${A C}_{ω}$ , the unit disc $D$ , the upper half-plane $H$ , and $φ (z) = \frac{z - i}{z + i}$ .

1.1A1F1F3givenalgebra

The map $φ$ has the Möbius form $\frac{1 z - i}{1 z + i}$ with $a d - b c = 1 \cdot i - (- i) \cdot 1 = 2 i \neq 0$ , so by [F1] it is holomorphic away from its pole $z = - i$ and is a bijection of the sphere with Möbius inverse. Its inverse is $ψ (u) = \frac{i (1 + u)}{1 - u}$ : indeed $ψ (u) + i = \frac{2 i}{1 - u}$ and $ψ (u) - i = \frac{2 i u}{1 - u}$ , so $φ (ψ (u)) = u$ , and $1 + φ (z) = \frac{2 z}{z + i}$ , $1 - φ (z) = \frac{2 i}{z + i}$ give $ψ (φ (z)) = z$ .

2.1F1F2F3F6step 1.1

For $z \neq - i$ , [F3] gives $∣ φ (z) ∣ < 1 ⟺ ∣ z - i ∣^{2} < ∣ z + i ∣^{2} ⟺ - 2 Im z < 2 Im z ⟺ Im z > 0$ ; thus $φ (H) \subseteq D$ . Likewise, for $∣ u ∣ < 1$ the real part $(1 - ∣ u ∣^{2}) / ∣ 1 - u ∣^{2}$ of $\frac{1 + u}{1 - u}$ is positive, so $Im ψ (u) = \frac{1 - ∣ u ∣^{2}}{∣ 1 - u ∣^{2}} > 0$ and $ψ (D) \subseteq H$ . Since the two maps are inverse bijections by step 1.1 and both are holomorphic on these domains, [F6] makes $φ : H \to D$ a biholomorphism with $J_{φ} (z) = φ^{'} (z) = \frac{2 i}{(z + i)^{2}}$ .

3.1F3F4F5step 2.1algebra

By [F4] applied to $φ$ , $K_{H} (z, w) = K_{D} (φ (z), φ (w)) φ^{'} (z) \overline{φ^{'} (w)}$ . By [F5] and [F3], $1 - φ (z) \overline{φ (w)} = 1 - \frac{(z - i) (\overline{w} + i)}{(z + i) (\overline{w} - i)} = \frac{(z + i) (\overline{w} - i) - (z - i) (\overline{w} + i)}{(z + i) (\overline{w} - i)} = \frac{- 2 i (z - \overline{w})}{(z + i) (\overline{w} - i)} .$ Substituting this and $φ^{'} (z) = \frac{2 i}{(z + i)^{2}}$ , $\overline{φ^{'} (w)} = \frac{- 2 i}{(\overline{w} - i)^{2}}$ into the transformation law gives $K_{H} (z, w) = \frac{(z + i)^{2} (\overline{w} - i)^{2}}{π (- 2 i (z - \overline{w}))^{2}} \cdot \frac{2 i}{(z + i)^{2}} \cdot \frac{- 2 i}{(\overline{w} - i)^{2}} = \frac{- 1}{π (z - \overline{w})^{2}},$ since $(2 i) (- 2 i) = 4$ and $(- 2 i)^{2} = - 4$ .

4.1F4F5step 3.1∎

Setting $w = z$ in step 3.1 and using $z - \overline{z} = 2 i Im z$ gives $(z - \overline{z})^{2} = - 4 (Im z)^{2}$ , hence $K_{H} (z, z) = \frac{1}{4 π (Im z)^{2}} > 0$ for $z \in H$ . This is transport of the disc's diagonal: $K_{H} (z, z) = ∣ φ^{'} (z) ∣^{2} K_{D} (φ (z), φ (z))$ by [F4], and by [F4] the pullback along the biholomorphism $φ$ carries the disc reproducing property to the reproducing property of $K_{H}$ on $A^{2} (H)$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

70 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

Zbigniew Błocki, The Bergman Kernel and Metric (lecture notes) (standard reference, not scraped)