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 (The Axiom of Countable Choice ()) and let . The preceding definition The Bergman space and the Bergman kernel gives and . Also, and . Thus neither unbounded domain has a nontrivial Bergman kernel, and the kernel-derived Bergman metric is unavailable there because is undefined. In contrast, the bounded unit disc has .
Facts & Assumptions
The only choice principle is , inherited through the Bergman-space, mean-value and disc-integral suppliers; no full Axiom of Choice is used (The Axiom of Countable Choice ()).
For every , and (The Bergman space and the Bergman kernel).
Open and closed polydiscs are defined coordinatewise, and open polydiscs are open sets (Balls, polydiscs and the distinguished boundary in ).
If is holomorphic on an open neighborhood of a closed polydisc , then (The mean-value bound for holomorphic functions on a polydisc).
If are measurable, then (Monotonicity and nonnegative homogeneity of the nonnegative integral).
The unit disc has area (Weighted monomial integrals and monomial norms for the disc, ball and polydisc, with and ).
Each class in has a unique holomorphic representative that is square-integrable (The Bergman space and the Bergman kernel).
Every point evaluation on has a unique Riesz representer satisfying , and (The Bergman space and the Bergman kernel).
Proof
Given: , , and the definitions of and from [F1], [F6] and [F7].
The conclusion and is already proved in The Bergman space and the Bergman kernel, so this example uses that earlier result without repeating its large-polydisc argument.
Let and set . For every , the closed polydisc lies in , since and the second coordinate is unrestricted. These polydiscs show that the product set is open. Let be the unique holomorphic representative of any class in , as in [F6]. The mean bound [F3] and integral monotonicity [F4] give . Letting gives . Since was arbitrary, every holomorphic representative is identically zero, hence .
By [F7], each point evaluation on the zero space has the unique representer , so for all . Its diagonal is zero, making the logarithm in the kernel-derived Bergman metric undefined.
By [F5], the constant function is in . Its evaluation at is , so its Riesz representer is nonzero by [F7]. Reproduction with gives , proving the claimed contrast with the two unbounded examples.
Depends on
- Balls, polydiscs and the distinguished boundary in $\mathbb{C}^m$
- The Bergman space $A^2(\Omega)$ and the Bergman kernel
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- The mean-value $L^2$ bound for holomorphic functions on a polydisc
- Weighted monomial integrals and monomial norms for the disc, ball and polydisc
- Monotonicity and nonnegative homogeneity of the nonnegative integral
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
- Jiří Lebl, Tasty Bits of Several Complex Variables (book) (standard reference, not scraped)