LemmaStatement: AI-adaptedProof: 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.

Determinants and kernel quotients of the model Bergman metrics

Statement

Assume the Axiom of Countable Choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )), let $m \geq 1$ , and use the one-based coordinate aliases of The Bergman metric form on a bounded domain. For the unit ball and the unit polydisc in $C^{m}$ ,

$\det g_{B^{m}} (z) = \frac{(m + 1)^{m}}{(1 - ∣ z ∣^{2})^{m + 1}}, \det g_{D^{m}} (z) = 2^{m} \prod_{j = 1}^{m} \frac{1}{(1 - ∣ z_{j} ∣^{2})^{2}} .$

Consequently the invariant quotients are the constants

$\frac{\det g_{B^{m}}}{K_{B^{m}}} = \frac{(m + 1)^{m} π^{m}}{m!}, \frac{\det g_{D^{m}}}{K_{D^{m}}} = 2^{m} π^{m},$

and these constants are distinct for every $m \geq 2$ .

Facts & Assumptions

[A1]

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

[F1]

The model kernels are $K_{B^{m}} (z, z) = \frac{m!}{π^{m} (1 - ∣ z ∣^{2})^{m + 1}}$ and $K_{D^{m}} (z, z) = \frac{1}{π^{m}} \prod_{j = 1}^{m} \frac{1}{(1 - ∣ z_{j} ∣^{2})^{2}}$ (Bergman kernels of the disc, ball and polydisc, and Szegő kernels of the disc and ball).

[F2]

The Bergman metric form is $g_{Ω} = \partial \overline{\partial} \log K_{Ω} (z, z)$ , its matrix has entries $(g_{Ω})_{j \overset{ˉ}{k}} = \partial_{j} \partial_{\overset{ˉ}{k}} \log K_{Ω} (z, z)$ , and $\log K_{Ω} (z, z)$ is real $C^{\infty}$ on a bounded domain (The Bergman metric form on a bounded domain, Smoothness of the Bergman kernel and positivity of its diagonal on bounded domains).

[F3]

For $x > 0$ , $\log^{'} (x) = 1 / x$ , and the usual product, quotient and chain rules hold; Wirtinger operators are the first-order operators of Wirtinger operators in $C^{m}$ (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, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[F4]

Under the complex Euclidean dictionary, $∣ z ∣^{2} = \sum_{j = 1}^{m} ∣ z_{j} ∣^{2} = \sum_{j = 1}^{m} z_{j} \overline{z_{j}}$ , and $\partial_{{\overline{z}}_{k}} \overline{z_{j}} = δ_{j k}$ for these first-order operators (Complex $m$ -space and its real coordinate dictionary, Wirtinger operators in $C^{m}$ ).

[F5]

For a commutative ring, $A \in M_{n} (R)$ and columns $u, v$ , $\det (A + u v^{T}) = \det (A) + v^{T} adj (A) u$ ; the adjugate is the transpose of the cofactor matrix, and a diagonal matrix has determinant the product of its diagonal entries (For $A \in M_{n} (R)$ and columns $u, v$ over a commutative ring, $\det (A + u v^{T}) = \det (A) + v^{T} adj (A) u$ , Deleted-row-and-column minors, cofactors, the cofactor matrix and the adjugate over a commutative ring, The determinant of a triangular matrix is the product of its diagonal entries).

[F6]

For $A = (1 - r) I_{m}$ with $0 \leq r < 1$ , each diagonal cofactor equals $(1 - r)^{m - 1}$ , including the empty minor $1$ when $m = 1$ . If $i \neq j$ , deleting row $i$ and column $j$ leaves the original row $j$ present but zero, so its determinant is zero by the Leibniz formula. Thus $adj (A) = (1 - r)^{m - 1} I_{m}$ (Deleted-row-and-column minors, cofactors, the cofactor matrix and the adjugate over a commutative ring, For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix, The determinant of a triangular matrix is the product of its diagonal entries).

[F7]

The invariant quotient $\det g_{Ω} / K_{Ω}$ agrees under biholomorphisms, and diagonal kernel values are positive on bounded domains (The determinant quotient $\det g_{Ω} / K_{Ω}$ is a biholomorphic invariant, Smoothness of the Bergman kernel and positivity of its diagonal on bounded domains).

[F8]

Factorials of naturals are positive and $m! = \prod_{k = 1}^{m} k$ (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ).

[F9]

In the Leibniz determinant formula every term contains exactly $m$ matrix entries, so $\det (c A) = c^{m} \det A$ for a complex scalar $c$ (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix).

Proof

technique · direct differentiation of the explicit model kernels, a rank-one determinant update, and a finite comparison of constants

Given: ${A C}_{ω}$ , $m \geq 1$ , the unit ball $B^{m}$ and the unit polydisc $D^{m}$ with the model kernels of [F1], and $z$ in the respective domain.

1.1A1F1F2F3F4algebra

By [F1], $\log K_{B^{m}} (z, z) = \log \frac{m!}{π^{m}} - (m + 1) \log (1 - ∣ z ∣^{2})$ . Using [F3] and [F4], $\partial_{j} \log K_{B^{m}} (z, z) = \frac{(m + 1) \overline{z_{j}}}{1 - ∣ z ∣^{2}}$ and hence $(g_{B^{m}})_{j \overset{ˉ}{k}} (z) = (m + 1) \frac{(1 - ∣ z ∣^{2}) δ_{j k} + \overline{z_{j}} z_{k}}{(1 - ∣ z ∣^{2})^{2}}$ ; in matrix form $g_{B^{m}} (z) = \frac{m + 1}{(1 - ∣ z ∣^{2})^{2}} ((1 - ∣ z ∣^{2}) I_{m} + \overline{z} z^{T})$ , where $\overline{z} z^{T}$ has entries $\overline{z_{j}} z_{k}$ .

1.2F1F2F3F4F5algebra

By [F1], $\log K_{D^{m}} (z, z) = - m \log π - 2 \sum_{j = 1}^{m} \log (1 - ∣ z_{j} ∣^{2})$ . Each summand depends only on its own coordinate, so [F3] and [F4] give $(g_{D^{m}})_{j \overset{ˉ}{k}} (z) = 0$ for $j \neq k$ and $(g_{D^{m}})_{j j} (z) = \frac{2}{(1 - ∣ z_{j} ∣^{2})^{2}}$ ; the matrix is diagonal, and [F5] gives $\det g_{D^{m}} (z) = 2^{m} \prod_{j = 1}^{m} (1 - ∣ z_{j} ∣^{2})^{- 2}$ , the second displayed determinant.

2.1F5F6F9step 1.1algebra

Put $r : = ∣ z ∣^{2} \in [0, 1)$ and $A : = (1 - r) I_{m}$ . By [F6], $adj (A) = (1 - r)^{m - 1} I_{m}$ , so the rank-one update [F5] with $u = \overline{z}$ , $v = z$ gives $\det ((1 - r) I_{m} + \overline{z} z^{T}) = \det (A) + z^{T} adj (A) \overline{z} = (1 - r)^{m} + (1 - r)^{m - 1} r = (1 - r)^{m - 1} .$ Taking determinants in step 1.1 with [F9] therefore gives $\det g_{B^{m}} (z) = (m + 1)^{m} (1 - r)^{m - 1} / (1 - r)^{2 m} = (m + 1)^{m} / (1 - ∣ z ∣^{2})^{m + 1}$ , the first displayed determinant.

3.1F1F7step 1.2step 2.1algebra

Dividing by the model kernel diagonals of [F1] cancels the $(1 - ∣ z ∣^{2})$ and coordinate factors and gives $\det g_{B^{m}} / K_{B^{m}} = \frac{(m + 1)^{m} π^{m}}{m!}$ and $\det g_{D^{m}} / K_{D^{m}} = 2^{m} π^{m}$ ; the divisions use the positive diagonal values, and by [F7] the quotients are the biholomorphic invariants of the two domains.

4.1F8step 3.1algebra∎

It remains to compare the two constants. Their quotient is $\frac{(m + 1)^{m}}{2^{m} m!} = \prod_{k = 1}^{m} \frac{m + 1}{2 k}$ , a product of positive real factors. Pair the factor $k$ with the factor $m + 1 - k$ ; the pair contributes $\frac{(m + 1)^{2}}{4 k (m + 1 - k)} \geq 1$ , because $(m + 1)^{2} - 4 k (m + 1 - k) = (2 k - m - 1)^{2} \geq 0$ , with strict inequality unless $2 k = m + 1$ . If $m = 2 n$ is even, every one of the $n$ pairs has strict inequality, so the product exceeds $1$ . If $m = 2 n + 1 \geq 3$ is odd, the middle factor $k = n + 1$ contributes $1$ while the pair $k = 1$ with $k = m$ contributes $\frac{(m + 1)^{2}}{4 m} > 1$ for $m \geq 2$ , so again the product exceeds $1$ . Hence $\frac{(m + 1)^{m} π^{m}}{m!} > 2^{m} π^{m}$ for every $m \geq 2$ , and the two invariant constants are distinct.

Depends on

Used by

The claim that the ball and the polydisc are biholomorphic False statement
Poincaré's theorem: the ball and the polydisc are not biholomorphic for m≥2 Theorem

Dependency tree · two levels

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