Alphabeta Math
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.

An unbounded domain with trivial Bergman space

Statement

Assume ACω (The Axiom of Countable Choice (ACω)) and let m≥1. The preceding definition The Bergman space A2(Ω) and the Bergman kernel gives A2(Cm)={0} and KCm≡0. Also, A2(D×C)={0} and KD×C≡0. Thus neither unbounded domain has a nontrivial Bergman kernel, and the kernel-derived Bergman metric is unavailable there because log⁡K(z,z)=log⁡0 is undefined. In contrast, the bounded unit disc has KD(0,0)>0.

Facts & Assumptions

[A1]

The only choice principle is ACω, inherited through the Bergman-space, mean-value and disc-integral suppliers; no full Axiom of Choice is used (The Axiom of Countable Choice (ACω)).

[F1]

For every m≥1, A2(Cm)={0} and KCm≡0 (The Bergman space A2(Ω) and the Bergman kernel).

[F2]

Open and closed polydiscs are defined coordinatewise, and open polydiscs are open sets (Balls, polydiscs and the distinguished boundary in Cm).

[F3]

If f is holomorphic on an open neighborhood of a closed polydisc Δ‾r(a)⊆Ω⊆C2, then ∣f(a)∣2≤1π2r02r12∫Δr(a)∣f∣2 dλ4 (The mean-value L2 bound for holomorphic functions on a polydisc).

[F4]

If 0≤g≤h are measurable, then ∫g≤∫h (Monotonicity and nonnegative homogeneity of the nonnegative integral).

[F5]

The unit disc has area λ2(D)=π (Weighted monomial integrals and monomial norms for the disc, ball and polydisc, with m=1 and α=0).

[F6]

Each class in A2(Ω) has a unique holomorphic representative that is square-integrable (The Bergman space A2(Ω) and the Bergman kernel).

[F7]

Every point evaluation on A2(Ω) has a unique Riesz representer kw satisfying f(w)=⟨f,kw⟩, and KΩ(z,w)=kw(z) (The Bergman space A2(Ω) and the Bergman kernel).

Proof

technique · direct, using a growing polydisc in the unbounded coordinate

Given: ACω, m≥1, and the definitions of A2(Ω) and KΩ from [F1], [F6] and [F7].

1.1A1F1given

The conclusion A2(Cm)={0} and KCm≡0 is already proved in The Bergman space A2(Ω) and the Bergman kernel, so this example uses that earlier result without repeating its large-polydisc argument.

1.2A1F2F3F4F6given

Let a=(z,w)∈D×C and set ρ=(1−∣z∣)/2>0. For every R>0, the closed polydisc Δ‾(ρ,R)(a) lies in D×C, since ∣z∣+ρ=(1+∣z∣)/2<1 and the second coordinate is unrestricted. These polydiscs show that the product set is open. Let f be the unique holomorphic representative of any class in A2(D×C), as in [F6]. The mean bound [F3] and integral monotonicity [F4] give ∣f(a)∣2≤(π2ρ2R2)−1∫Δ(ρ,R)(a)∣f∣2 dλ4≤∥[f]∥L2(D×C)2/(π2ρ2R2). Letting R→∞ gives f(a)=0. Since a was arbitrary, every holomorphic representative is identically zero, hence A2(D×C)={0}.

2.1A1F7step 1.2

By [F7], each point evaluation on the zero space A2(D×C) has the unique representer kw=0, so KD×C(z,w)=0 for all z,w. Its diagonal is zero, making the logarithm in the kernel-derived Bergman metric undefined.

3.1A1F5F7given∎

By [F5], the constant function 1 is in A2(D). Its evaluation at 0 is 1, so its Riesz representer k0 is nonzero by [F7]. Reproduction with f=k0 gives KD(0,0)=k0(0)=⟨k0,k0⟩=∥k0∥2>0, proving the claimed contrast with the two unbounded examples.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

65 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