LemmaStatement: Literature-sourcedProof: 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.

Smoothness of the Bergman kernel and positivity of its diagonal on bounded domains

Statement

Assume the Axiom of Countable Choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $m \geq 1$ and let $Ω \subseteq C^{m}$ be a nonempty open set. Then $K_{Ω} \in C^{\infty} (Ω \times Ω)$ and $z \mapsto K_{Ω} (z, z)$ is $C^{\infty}$ on $Ω$ . If $Ω$ is bounded, its Lebesgue measure satisfies $0 < λ_{Ω} (Ω) < \infty$ , and for every $z \in Ω$ ,

$K_{Ω} (z, z) \geq \frac{1}{λ_{Ω} (Ω)} > 0.$

In particular, on a bounded domain $z \mapsto \log K_{Ω} (z, z)$ is $C^{\infty}$ .

Facts & Assumptions

[A1]

The only choice principle assumed is ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )). It is inherited through the Bergman Hilbert-space and Riesz setup, and is used by the Borel and Euclidean-ball measure suppliers below; no full Axiom of Choice is used.

[F1]

Under ${A C}_{ω}$ , $A^{2} (Ω)$ is a closed complex Hilbert subspace of $L^{2} (Ω)$ with the first-variable-linear pairing. Point evaluation has Riesz section $k_{w} = K_{Ω} (\cdot, w)$ and reproduces evaluation. The definition also gives $A^{2} (C^{m}) = {0}$ and $K_{C^{m}} \equiv 0$ , so no positivity is asserted for every unbounded open set (The Bergman space $A^{2} (Ω)$ and the Bergman kernel, The complex $L^{2}$ pairing on equivalence classes, $L^{2}$ with the integral pairing is a Hilbert space).

[F2]

The definition $K_{Ω} (z, w) = k_{w} (z)$ makes $z \mapsto K_{Ω} (z, w)$ holomorphic. Reproduction gives $K_{Ω} (z, w) = ⟨ k_{w}, k_{z} ⟩$ , so conjugate symmetry of the first-variable-linear $L^{2}$ pairing gives $K_{Ω} (w, z) = \overline{K_{Ω} (z, w)}$ ; hence the kernel is antiholomorphic in $w$ (The Bergman space $A^{2} (Ω)$ and the Bergman kernel, The complex $L^{2}$ pairing on equivalence classes, $L^{2}$ with the integral pairing is a Hilbert space).

[F3]

On every nonempty compact $K \subseteq Ω$ , $\sup_{K} ∣ f ∣ \leq C_{K} ∥ f ∥_{2}$ . The diagonal extremal identity is $K_{Ω} (w, w) = ∥ k_{w} ∥_{2}^{2} = \sup_{∥ f ∥_{2} \leq 1} ∣ f (w) ∣^{2}$ (Sup-norm and first-derivative bounds by the $L^{2}$ norm on compact subsets, Reproducing property, Bergman projection and the extremal characterization).

[F4]

The first-variable-linear Hilbert pairing satisfies $∣ ⟨ f, g ⟩ ∣ \leq ∥ f ∥_{2} ∥ g ∥_{2}$ (Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs).

[F5]

A separately holomorphic, locally bounded function on an open subset of $C^{n}$ is jointly holomorphic there (Locally bounded and separately holomorphic implies holomorphic).

[F6]

A holomorphic function on an open subset of complex Euclidean space is $C^{\infty}$ in the underlying real coordinates (Holomorphic functions of several variables are smooth and their complex derivatives are holomorphic).

[F7]

Complex conjugation is a real-linear coordinate map, and finite-order smooth maps are closed under composition (Real and imaginary parts, complex conjugation, and modulus, $C^{k}$ Euclidean maps and diffeomorphisms, $C^{k}$ Euclidean maps are closed under componentwise algebra and composition).

[F8]

The complex Euclidean metric is the real Euclidean metric under $C^{m} ≅ R^{2 m}$ . An open nonempty set contains a positive-radius ball, a bounded set is contained in some ball, and Euclidean balls have finite positive Lebesgue measure. Open sets are Borel and Lebesgue measurable, and measure is monotone (The Bergman space $A^{2} (Ω)$ and the Bergman kernel, Complex $m$ -space and its real coordinate dictionary, Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Open ball, closed ball and sphere in a metric space, Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, For $n \geq 1$ , every Euclidean closed ball and every Euclidean sphere of positive radius is compact, Euclidean balls have positive finite Lebesgue measure, Assuming countable choice, every Borel subset of $R^{n}$ is Lebesgue measurable, Measures are monotone).

[F9]

For $x > 0$ , $\log^{'} (x) = 1 / x$ and $\log$ is continuous. For each integer $n \geq 1$ , $\frac{d}{d x} x^{- n} = - n x^{- n - 1}$ ; products and quotients of continuous functions are continuous where their denominators are nonzero (The natural logarithm as the inverse of the exponential function, The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm, Integer powers $a^{m}$ , For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ). A real function is $C^{\infty}$ when all iterated coordinate partial derivatives of every finite order exist and are continuous ( $C^{k}$ maps and multi-index derivative notation in Euclidean space).

Proof

technique · direct, using the Riesz sections, compact evaluation bounds and the constant-function extremal witness

Given: ${A C}_{ω}$ , $m \geq 1$ , a nonempty open $Ω \subseteq C^{m}$ , its Bergman space $A^{2} (Ω)$ , and its Bergman kernel $K_{Ω}$ .

1.1A1F1F2given

For each $w \in Ω$ , $K_{Ω} (z, w) = k_{w} (z)$ is holomorphic in $z$ by [F1, F2]. Reproducing evaluation at $z$ on $k_{w}$ gives $K_{Ω} (z, w) = ⟨ k_{w}, k_{z} ⟩$ . Conjugate symmetry then gives $K_{Ω} (w, z) = ⟨ k_{z}, k_{w} ⟩ = \overline{K_{Ω} (z, w)}$ . Thus $K_{Ω}$ is antiholomorphic in $w$ , and $F (z, η) : = K_{Ω} (z, \overline{η})$ is separately holomorphic on $Ω \times Ω^{*}$ , where $Ω^{*} : = {η : \overline{η} \in Ω}$ .

1.2A1F1F8given

Suppose $Ω$ is bounded. Choose $a \in Ω$ ; openness gives $r > 0$ with $B (a, r) \subseteq Ω$ . Boundedness supplies $c \in C^{m}$ and $R_{0} > 0$ with $Ω \subseteq B (c, R_{0})$ . The Euclidean triangle inequality then gives $Ω \subseteq B (0, ∥ c ∥ + R_{0} + 1)$ . By [F8], $Ω$ is measurable and $0 < λ (B (a, r)) \leq λ_{Ω} (Ω) \leq λ (B (0, ∥ c ∥ + R_{0} + 1)) < \infty$ . Hence $0 < λ_{Ω} (Ω) < \infty$ .

2.1A1F3F4F8step 1.1

Let $K, L \subseteq Ω$ be nonempty compact sets. The evaluation estimate [F3] and the diagonal extremal identity [F3] give $K_{Ω} (z, z) \leq C_{K}^{2}$ for $z \in K$ and $K_{Ω} (w, w) \leq C_{L}^{2}$ for $w \in L$ . Since $K_{Ω} (z, w) = ⟨ k_{w}, k_{z} ⟩$ , Cauchy–Schwarz [F4] gives $∣ K_{Ω} (z, w) ∣ \leq C_{K} C_{L}$ on $K \times L$ . Around any $z_{0}, w_{0} \in Ω$ choose closed Euclidean ball neighborhoods $K, L$ contained in $Ω$ ; they are compact by [F8]. This proves that $F$ is locally bounded on $Ω \times Ω^{*}$ .

2.2A1F1F3step 1.2

Suppose $Ω$ is bounded. For $z \in Ω$ let $f_{0} : = λ_{Ω} (Ω)^{- 1 / 2}$ be the constant function. By step 1.2 it lies in $A^{2} (Ω)$ and has norm one. The extremal identity [F3] gives $K_{Ω} (z, z) \geq ∣ f_{0} (z) ∣^{2} = 1 / λ_{Ω} (Ω) > 0$ .

3.1F5F7F8step 1.1step 2.1

The set $Ω^{*}$ is open because complex conjugation is a Euclidean isometry, so $Ω \times Ω^{*}$ is an open subset of $C^{2 m}$ . By [F5], the separately holomorphic, locally bounded function $F$ is jointly holomorphic.

4.1F6F7step 3.1

By [F6], $F$ is $C^{\infty}$ in real coordinates. The map $(z, w) \mapsto (z, \overline{w})$ and the diagonal map $z \mapsto (z, z)$ are real-linear coordinate maps, hence smooth; [F7] makes their compositions with $F$ smooth. Therefore $K_{Ω} (z, w) = F (z, \overline{w})$ is $C^{\infty}$ on $Ω \times Ω$ , and $z \mapsto K_{Ω} (z, z)$ is $C^{\infty}$ on $Ω$ .

5.1F7F9step 4.1step 2.2

Let $D (z) : = K_{Ω} (z, z)$ . On a bounded $Ω$ , steps 4.1 and 2.2 give $D \in C^{\infty} (Ω)$ with $D > 0$ . Set $ℓ (x) : = \log x$ for $x > 0$ . By [F9], $ℓ^{'} (x) = x^{- 1}$ , and induction using the negative-power derivative in [F9] gives $ℓ^{(n)} (x) = (- 1)^{n - 1} (n - 1)! x^{- n}$ for every $n \geq 1$ . These derivatives are continuous on $(0, \infty)$ by [F9], and $ℓ$ itself is continuous there; hence $ℓ \in C^{\infty} ((0, \infty))$ . The composition theorem [F7] now gives $\log K_{Ω} (z, z) = ℓ (D (z)) \in C^{\infty} (Ω)$ .

6.1step 2.1step 4.1step 1.2step 2.2step 5.1∎

Steps 2.1 and 4.1 establish joint $C^{\infty}$ smoothness and the smooth diagonal for every nonempty open $Ω$ ; steps 1.2, 2.2 and 5.1 establish the positive diagonal bound and smooth logarithmic potential whenever $Ω$ is bounded. These are the two claims.

Depends on

Used by

Dependency tree · two levels

165 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 (standard reference, not scraped)
Jiří Lebl, Tasty Bits of Several Complex Variables (standard reference, not scraped)