TheoremStatement: 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.

The Bergman metric is positive definite on bounded domains and biholomorphically invariant

Statement

Assume the Axiom of Countable Choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )) and let $m \geq 1$ . Let $Ω \subseteq C^{m}$ be a bounded domain with Bergman kernel $K_{Ω}$ , Bergman metric form $g_{Ω}$ , and quadratic form $B_{Ω}^{2} (z; X) = g_{Ω} (z) (X, X)$ as in The Bergman metric form on a bounded domain, and use the one-based coordinate aliases of The Levi form and strict plurisubharmonicity.

For every $z \in Ω$ and every $X \in C^{m} ∖ {0}$ , $B_{Ω}^{2} (z; X) = \frac{1}{K_{Ω} (z, z)} \sup {∣ \partial_{X} f (z) ∣^{2} : f \in A^{2} (Ω), ∥ f ∥_{L^{2}} \leq 1, f (z) = 0},$ where $\partial_{X} f = \sum_{j = 1}^{m} X_{j} \frac{\partial f}{\partial z_{j}}$ . The supremum is finite, positive, and attained. In particular $B_{Ω}^{2} (z; X) > 0$ , so the Hermitian form $g_{Ω} (z)$ is positive definite.
If $F : Ω \to Ω^{'}$ is a biholomorphism of bounded domains, then for all $z \in Ω$ and all $X, Y \in C^{m}$ , $g_{Ω} (z) (X, Y) = g_{Ω^{'}} (F (z)) (D F (z) X, D F (z) Y) .$ Equivalently, $B_{Ω}^{2} (z; X) = B_{Ω^{'}}^{2} (F (z); D F (z) X)$ for every $X$ .

Facts & Assumptions

[A1]

The only choice principle assumed is ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )): it enters through the Bergman Hilbert/Riesz structure and the orthogonal projection. No full Axiom of Choice is used.

[F1]

For a nonempty open $Ω \subseteq C^{m}$ , $A^{2} (Ω)$ is a closed complex Hilbert subspace of $L^{2} (Ω)$ for the first-variable-linear pairing, each class has a unique holomorphic representative, point evaluation has a unique Riesz section $k_{w} = K_{Ω} (\cdot, w)$ with $f (w) = ⟨ f, k_{w} ⟩$ , and $K_{Ω} (z, w) = ⟨ k_{w}, k_{z} ⟩ = \overline{K_{Ω} (w, z)}$ (The Bergman space $A^{2} (Ω)$ and the Bergman kernel, $A^{2} (Ω)$ is closed, and the Bergman kernel is the sum over any complete orthonormal system).

[F2]

For a bounded domain $Ω$ , $K_{Ω} \in C^{\infty} (Ω \times Ω)$ , the diagonal is smooth with $K_{Ω} (z, z) \geq 1 / λ_{Ω} (Ω) > 0$ , and $K_{Ω}$ is holomorphic in its first and antiholomorphic in its second variable (Smoothness of the Bergman kernel and positivity of its diagonal on bounded domains, $A^{2} (Ω)$ is closed, and the Bergman kernel is the sum over any complete orthonormal system).

[F3]

For every nonempty compact $K \subseteq Ω$ there are finite constants with $\sup_{K} ∣ f ∣ \leq C_{K} ∥ f ∥_{2}$ and $\sup_{K} ∣ \partial_{z}^{α} f ∣ \leq C_{K, α} ∥ f ∥_{2}$ for every multi-index $∣ α ∣ \leq 1$ (Sup-norm and first-derivative bounds by the $L^{2}$ norm on compact subsets).

[F4]

Every bounded linear functional on a real or complex Hilbert space has a unique representing vector, isometrically; in the first-variable-linear convention $f (x) = ⟨ x, y ⟩$ (Riesz representation for Hilbert spaces).

[F5]

A closed linear subspace $M$ of a Hilbert space satisfies $H = M \oplus M^{⊥}$ uniquely, and the orthogonal projection onto $M$ is defined by that decomposition (Orthogonal decomposition by a closed subspace, The Hilbert orthogonal projection onto a closed subspace).

[F6]

Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for linearly dependent pairs (Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs).

[F7]

If real $C^{2}$ functions satisfy $u \geq v$ near $a$ with $u (a) = v (a)$ , then $L_{u} (a; X) \geq L_{v} (a; X)$ for every $X$ (The complex Hessian of a $C^{2}$ function dominates that of a minorant at a common minimum).

[F8]

The Bergman metric form is the Levi form of $u_{Ω} = \log K_{Ω} (z, z)$ , and $B_{Ω}^{2} (z; X) = L_{u_{Ω}} (z; X) = \sum_{j, k = 1}^{m} \frac{\partial^{2} u_{Ω}}{\partial z_{j} \partial {\overline{z}}_{k}} (z) X_{j} \overline{X_{k}}$ for the one-based coordinate aliases (The Bergman metric form on a bounded domain, The Levi form and strict plurisubharmonicity).

[F9]

Wirtinger operators are $\partial_{z_{j}} = \frac{1}{2} (\partial_{x_{j}} - i \partial_{y_{j}})$ , $\partial_{{\overline{z}}_{j}} = \frac{1}{2} (\partial_{x_{j}} + i \partial_{y_{j}})$ , for holomorphic functions the real-coordinate derivative identities in [F12] give $\partial_{{\overline{z}}_{j}} f = 0$ , real mixed partials commute by Clairaut--Schwarz theorem for continuous second partial derivatives, $\log^{'} (x) = 1 / x$ for $x > 0$ by The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t, and the product and chain rules hold for these first-order operators (Wirtinger operators in $C^{m}$ , Complex $m$ -space and its real coordinate dictionary, $C^{k}$ maps and multi-index derivative notation in Euclidean space, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[F10]

A holomorphic map is complex differentiable with complex-linear derivative $D F (z)$ , the chain rule holds (Holomorphic functions on an open subset of $C^{m}$ , Holomorphic maps $C^{m} \to C^{n}$ and the complex Jacobian matrix, The composite of holomorphic maps is holomorphic and its complex Jacobian is the product).

[F11]

A biholomorphism $F : Ω \to Ω^{'}$ 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 $U_{F} g = (g \circ F) J_{F}$ is a unitary isomorphism $A^{2} (Ω^{'}) \to A^{2} (Ω)$ (Transformation law of the Bergman kernel under a biholomorphism).

[F12]

A holomorphic function on an open set is of class $C^{n}$ in the real coordinates for every natural $n$ , hence smooth (Holomorphic functions of several variables are smooth and their complex derivatives are holomorphic).

[F13]

The complex plane is complete, hence Banach for its modulus norm. A continuous differentiable complex-valued curve whose derivative is bounded by $C$ changes by at most $C$ times the parameter distance (The complex plane is complete, and convergence is equivalent to convergence of real and imaginary parts, Mean value inequality for a differentiable Banach-valued curve).

Proof

technique · direct, using the reduced Riesz kernel of the subspace $\{f(z)=0\}$ and a second-order comparison with $\log K_\Omega$

Given: ${A C}_{ω}$ , the bounded domain $Ω$ , a point $z \in Ω$ , and a direction $X \in C^{m}$ .

1.1A1F1F2F3F4F5

Put $M : = K_{Ω} (z, z)$ . By [F2], $M > 0$ , so $k_{z} \neq 0$ and the subspace $H^{'} : = {f \in A^{2} (Ω) : f (z) = 0} = {f : ⟨ f, k_{z} ⟩ = 0} = (C k_{z})^{⊥}$ is closed; by [F5], $A^{2} (Ω) = C k_{z} \oplus H^{'}$ . By [F3] with the singleton $K = {ζ}$ the evaluation $ε_{ζ} (f) : = f (ζ)$ is bounded on $A^{2} (Ω)$ and hence on $H^{'}$ for every $ζ \in Ω$ ; [F4] gives a unique $h_{ζ} \in H^{'}$ with $f (ζ) = ⟨ f, h_{ζ} ⟩$ for all $f \in H^{'}$ . Define $E (ζ) : = ∥ h_{ζ} ∥_{2}^{2}$ .

1.2F1F2F5F6algebra

By [F5] the projection of $k_{ζ}$ onto $H^{'}$ is $h_{ζ} = k_{ζ} - \frac{⟨ k_{ζ}, k_{z} ⟩}{M} k_{z}$ , and $⟨ k_{ζ}, k_{z} ⟩ = K_{Ω} (z, ζ)$ by [F1]. Hence, pointwise in $η$ , $h_{ζ} (η) = K_{Ω} (η, ζ) - \frac{K_{Ω} (z, ζ)}{M} K_{Ω} (η, z)$ , and reproducing on $h_{ζ}$ gives $E (ζ) = ∥ h_{ζ} ∥_{2}^{2} = K_{Ω} (ζ, ζ) - \frac{∣ K_{Ω} (z, ζ) ∣^{2}}{M} .$ By [F2] the function $E$ is $C^{\infty}$ on $Ω$ ; by [F6] it satisfies $E (ζ) \geq 0$ with $E (z) = 0$ , and $E (ζ) > 0$ for $ζ \neq z$ , since then some coordinate satisfies $ζ_{j} \neq z_{j}$ and the bounded function $η \mapsto η_{j} - z_{j}$ lies in $H^{'}$ with nonzero value at $ζ$ .

1.3F2F8F9algebra

Compute the Levi form of $E$ . Write $D (ζ) : = K_{Ω} (ζ, ζ)$ and $A (ζ) : = K_{Ω} (ζ, z)$ , so that $E = D - \frac{∣ A ∣^{2}}{M}$ , $D (z) = A (z) = M$ and $∣ A (z) ∣^{2} = M^{2}$ , and $D$ is $C^{\infty}$ near $z$ . Set $a_{j} : = \partial_{j} A (z)$ and $c_{j k} : = \partial_{j} \partial_{\overline{k}} D (z)$ . Since $K_{Ω}$ is holomorphic in the first and antiholomorphic in the second variable [F2, F9], the Wirtinger derivatives $\partial_{\overline{ζ}} K_{Ω}$ and $\partial_{η} K_{Ω}$ vanish identically, and the product and chain rules give $\partial_{j} D (z) = a_{j}$ , $\partial_{\overline{k}} D (z) = \overline{a_{k}}$ , $\partial_{j} ∣ A ∣^{2} (z) = a_{j} M$ , $\partial_{\overline{k}} ∣ A ∣^{2} (z) = M \overline{a_{k}}$ , and $\partial_{j} \partial_{\overline{k}} ∣ A ∣^{2} (z) = a_{j} \overline{a_{k}}$ ; consequently $\partial_{j} E (z) = \partial_{\overline{j}} E (z) = 0$ , $\partial_{j} \partial_{k} E (z) = \partial_{\overline{j}} \partial_{\overline{k}} E (z) = 0$ , and $\partial_{j} \partial_{\overline{k}} E (z) = c_{j k} - \frac{a_{j} \overline{a_{k}}}{M} .$ Since $D (z) = M > 0$ , the same rules applied to $\log D$ give $\partial_{j} \partial_{\overline{k}} \log D (z) = \frac{c_{j k}}{M} - \frac{a_{j} \overline{a_{k}}}{M^{2}}$ , so $M \partial_{j} \partial_{\overline{k}} \log D (z) = \partial_{j} \partial_{\overline{k}} E (z)$ ; summing against $X_{j} \overline{X_{k}}$ and using [F8] yields $L_{E} (z; X) = M L_{\log D} (z; X) = M B_{Ω}^{2} (z; X) .$

2.1A1F5F6F7F8F12step 1.2

Let $f \in H^{'}$ with $∥ f ∥_{2} \leq 1$ . By [F6] and the reproducing identity of step 1.1, $∣ f (ζ) ∣^{2} = ∣ ⟨ f, h_{ζ} ⟩ ∣^{2} \leq ∥ f ∥_{2}^{2} E (ζ) \leq E (ζ)$ for every $ζ \in Ω$ , with equality at $ζ = z$ . Both $E$ and $∣ f ∣^{2}$ are $C^{2}$ : $E$ was shown $C^{\infty}$ in step 1.2, and $f$ is holomorphic, hence smooth in the real coordinates by [F12]. So [F7] gives $L_{E} (z; X) \geq L_{∣ f ∣^{2}} (z; X) = ∣ \partial_{X} f (z) ∣^{2}$ ; hence $\sup {∣ \partial_{X} f (z) ∣^{2} : f \in H^{'}, ∥ f ∥_{2} \leq 1} \leq L_{E} (z; X)$ .

2.2F2F9F13step 1.2step 1.3

Fix $X \neq 0$ and $δ > 0$ such that $z + τ X \in Ω$ for real $∣ τ ∣ < δ$ . Set $H (τ, σ) : = h_{z + τ X} (z + σ X)$ . The explicit formula in step 1.2 makes $H$ smooth, with $H (τ, 0) = H (0, σ) = 0$ . Differentiating that formula gives $\partial_{τ} \partial_{σ} H (0, 0) = \sum_{j, k} X_{j} \overline{X_{k}} (c_{j k} - a_{j} \overline{a_{k}} / M) = b$ , where $b : = L_{E} (z; X)$ by step 1.3. Put $R (τ, σ) : = H (τ, σ) - b τ σ$ . For every $ε > 0$ , continuity makes $∣ \partial_{τ} \partial_{σ} R ∣ < ε$ on a small rectangle about $(0, 0)$ . Since $\partial_{σ} R (0, σ) = 0$ and $R (τ, 0) = 0$ , applying [F13] first to $τ \mapsto \partial_{σ} R (τ, σ)$ and then to $σ \mapsto R (τ, σ)$ yields $∣ R (τ, σ) ∣ \leq ε ∣ τ σ ∣$ . Thus $H (τ, σ) / (τ σ) \to b$ as both nonzero real parameters tend to $0$ , and in particular $E (z + τ X) / τ^{2} = H (τ, τ) / τ^{2} \to b$ .

3.1A1F4F8step 2.1step 1.3

Assume $X \neq 0$ . The function $f_{0} (η) : = ⟨ η - z, X ⟩ = \sum_{j = 1}^{m} (η_{j} - z_{j}) \overline{X_{j}}$ is holomorphic on $Ω$ and bounded there because $Ω$ is bounded, so $f_{0} \in H^{'}$ ; also $\partial_{X} f_{0} (z) = \sum_{j = 1}^{m} X_{j} \overline{X_{j}} = ∣ X ∣^{2}$ . Applying step 2.1 to $f_{0} / ∥ f_{0} ∥_{2}$ gives $L_{E} (z; X) \geq ∣ X ∣^{4} / ∥ f_{0} ∥_{2}^{2} > 0$ for $X \neq 0$ . Hence by step 1.3, $B_{Ω}^{2} (z; X) = L_{E} (z; X) / M > 0$ : the quadratic form of $g_{Ω} (z)$ is positive on every nonzero vector, so the Hermitian form is positive definite.

4.1A1F1F4F5F6F10step 1.1step 3.1step 2.2

For real $τ \neq 0$ put $g_{τ} : = h_{z + τ X} / τ \in H^{'}$ . Reproduction gives $⟨ g_{τ}, g_{σ} ⟩ = H (τ, σ) / (τ σ)$ , so step 2.2 implies $∥ g_{τ} - g_{σ} ∥_{2}^{2} \to 0$ as $τ, σ \to 0$ . Choose, for example, $τ_{n} = δ / (n + 2)$ . The closed subspace $H^{'}$ is complete by [F1, F5], so $g_{τ_{n}} \to g \in H^{'}$ ; the same Cauchy estimate gives $g_{τ} \to g$ for all real $τ \to 0$ . By step 2.2, $∥ g ∥_{2}^{2} = b$ . For every $f \in H^{'}$ , continuity of the pairing and holomorphic differentiability give $⟨ f, g ⟩ = \lim_{τ \to 0} f (z + τ X) / τ = \partial_{X} f (z)$ . Hence $g$ represents the derivative functional, and Cauchy–Schwarz gives $\sup_{f \in H^{'}, ∥ f ∥_{2} \leq 1} ∣ \partial_{X} f (z) ∣^{2} = ∥ g ∥_{2}^{2} = b$ , attained at $g / ∥ g ∥_{2}$ because $b > 0$ by step 3.1.

5.1step 2.1step 1.3step 3.1step 4.1

Combining steps 1.3, 2.1 and 4.1 yields $\sup {∣ \partial_{X} f (z) ∣^{2} : f \in A^{2} (Ω), ∥ f ∥_{2} \leq 1, f (z) = 0} = L_{E} (z; X) = K_{Ω} (z, z) B_{Ω}^{2} (z; X)$ , which is the displayed formula, with the supremum attained; step 3.1 gives its strict positivity for $X \neq 0$ . This proves the two assertions of part 1.

6.1A1F8F10F11step 5.1

For part 2, let $F : Ω \to Ω^{'}$ be a biholomorphism, $J : = J_{F} = \det_{C} D F$ , and let $U_{F} g = (g \circ F) J$ be the unitary isomorphism of [F11], so that $U_{F}$ maps the closed unit ball of $A^{2} (Ω^{'})$ onto that of $A^{2} (Ω)$ and ${g : g (F (z)) = 0}$ onto $H^{'} = {f : f (z) = 0}$ (because $J (z) \neq 0$ ). If $f = U_{F} g$ , then the product rule and [F10] give $\partial_{X} f (z) = J (z) \partial_{D F (z) X} g (F (z)) + g (F (z)) \partial_{X} J (z)$ , and for $f \in H^{'}$ the second term vanishes; hence the supremum identity of part 1 applied on both domains, together with the diagonal kernel law $K_{Ω} (z, z) = ∣ J (z) ∣^{2} K_{Ω^{'}} (F (z), F (z))$ from [F11], gives $K_{Ω} (z, z) B_{Ω}^{2} (z; X) = ∣ J (z) ∣^{2} K_{Ω^{'}} (F (z), F (z)) B_{Ω^{'}}^{2} (F (z); D F (z) X) .$ Since $K_{Ω} (z, z) > 0$ and $∣ J (z) ∣^{2} K_{Ω^{'}} (F (z), F (z)) = K_{Ω} (z, z)$ , dividing by the positive number $K_{Ω} (z, z)$ yields $B_{Ω}^{2} (z; X) = B_{Ω^{'}}^{2} (F (z); D F (z) X)$ for every nonzero $X$ ; when $X = 0$ , both quadratic forms are zero by definition.

7.1F10step 6.1∎

The quadratic forms of the Hermitian forms agree under the complex-linear map $D F (z)$ . For all $X, Y$ , applying step 6.1 to the four directions $X + Y, X - Y, X + i Y, X - i Y$ and using complex linearity of $D F (z)$ plus the polarization identity $g (X, Y) = \frac{1}{4} (q (X + Y) - q (X - Y) + i q (X + i Y) - i q (X - i Y))$ for the quadratic form $q (Z) = g (Z, Z)$ gives $g_{Ω} (z) (X, Y) = g_{Ω^{'}} (F (z)) (D F (z) X, D F (z) Y)$ .

Remarks

The supremum in part 1 is taken over all of $A^{2} (Ω)$ with the single constraint $f (z) = 0$ ; since $f (z) = ⟨ f, k_{z} ⟩$ , this is exactly the closed subspace $H^{'}$ of the proof. In the orthonormal-system proof of the source, the reduced kernel of $H^{'}$ plays the role of the element $g$ of step 4.1. The constant hidden in the formula is carried by $K_{Ω} (z, z)$ ; the Bergman metric is normalized so that on the disc at the origin one obtains $B_{D}^{2} (0; X) = 2 ∣ X ∣^{2}$ .

Depends on

Used by

The determinant quotient det g_Ω/K_Ω is a biholomorphic invariant Lemma

Dependency tree · two levels

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