DefinitionDefinition: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

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 normalized Bochner–Martinelli kernel

Definition

For $n \geq 1$ and $ζ \neq z$ in $C^{n}$ , set

$Ω_{n} (ζ, z) = \frac{(n - 1)!}{(2 π i)^{n}} \sum_{j = 1}^{n} \frac{\overline{ζ_{j} - z_{j}}}{∣ ζ - z ∣^{2 n}} d {\overset{ˉ}{ζ}}_{1} \land d ζ_{1} \land \dots \land \hat{d {\overset{ˉ}{ζ}}_{j}} \land d ζ_{j} \land \dots \land d {\overset{ˉ}{ζ}}_{n} \land d ζ_{n} .$

Here the hat means that the indicated $d {\overset{ˉ}{ζ}}_{j}$ factor is omitted, while $d ζ_{j}$ remains. Use the complex orientation determined by $d x_{1} \land d y_{1} \land \dots \land d x_{n} \land d y_{n}$ , and the induced outward-normal-first orientation on boundaries. For fixed $z$ , this is a smooth $(n, n - 1)$ form in $ζ$ away from $z$ . Its coefficients are locally integrable in pairings with smooth complementary $(0, 1)$ forms near $ζ = z$ . For $n = 1$ it is $Ω_{1} (ζ, z) = \frac{d ζ}{2 π i (ζ - z)} .$

Facts & Assumptions

Given: $n \geq 1$ and distinct points $ζ, z \in C^{n}$ ; the coordinate forms and bidegree decomposition are those of Bigraded complex forms and the Dolbeault operators.

[F1]

The complex cotangent basis separates holomorphic and antiholomorphic factors into bidegrees (Bigraded complex forms and the Dolbeault operators).

Proof

technique · direct

1.1F1givenalgebra

In each summand one $d {\overset{ˉ}{ζ}}_{j}$ is omitted and all $n$ factors $d ζ_{1}, \dots, d ζ_{n}$ remain, so every summand has bidegree $(n, n - 1)$ by [F1]. Its scalar coefficient is smooth for $ζ \neq z$ . For $r = ∣ ζ - z ∣$ , $∣ \overline{ζ_{j} - z_{j}} / r^{2 n} ∣ \leq r^{1 - 2 n}$ . On a compact neighborhood of $z$ , a smooth complementary $(0, 1)$ form has bounded coefficients; the resulting top-degree density is bounded by a constant times $r^{1 - 2 n}$ . Its absolute integral near $z$ is bounded by a constant multiple of $\int_{0}^{ϵ} r^{1 - 2 n} r^{2 n - 1} d r = ϵ$ . The finite sum is therefore locally integrable.

2.1givenalgebra∎

If $n = 1$ , the omitted antiholomorphic factor leaves only $d ζ$ , and $\overline{ζ - z} / ∣ ζ - z ∣^{2} = 1 / (ζ - z)$ ; since $(n - 1)! / (2 π i)^{n} = 1 / (2 π i)$ , the formula reduces to $d ζ / (2 π i (ζ - z))$ .

Depends on

Bigraded complex forms and the Dolbeault operators

Used by

Bochner–Martinelli on the unit ball Example
The Bochner–Martinelli formula for C1 functions Theorem

Dependency tree · two levels

7 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

Lebl, Tasty Bits of Several Complex Variables, v4.4, Chapter 5 §5.1 (standard reference, not scraped)