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

Compactly supported dbar solutions on complex Euclidean space

Statement

Assume AC. Let $n \geq 2$ , and let $g = \sum_{j = 1}^{n} g_{j} d {\overset{ˉ}{z}}_{j}$ be a smooth compactly supported $\overset{ˉ}{\partial}$ -closed $(0, 1)$ -form on $C^{n}$ . Then there is a unique smooth compactly supported function $u$ on $C^{n}$ such that $\overset{ˉ}{\partial} u = g$ . The solution vanishes on the unique unbounded connected component of $C^{n} ∖ supp g$ .

Facts & Assumptions

Given: An integer $n \geq 2$ , the full Axiom of Choice, and a smooth compactly supported $\overset{ˉ}{\partial}$ -closed $(0, 1)$ -form $g = \sum_{j = 1}^{n} g_{j} d {\overset{ˉ}{z}}_{j}$ on $C^{n}$ .

[F1]

The $d z^{I} \land d {\overset{ˉ}{z}}^{J}$ expansion is unique, and the $\overset{ˉ}{\partial}$ coefficient formula differentiates each coefficient in ${\overset{ˉ}{z}}_{j}$ and wedges $d {\overset{ˉ}{z}}_{j}$ before its type factors (Bigraded complex forms and the Dolbeault operators).

[F2]

Under full AC, the whole-plane Cauchy transform $T_{k} h$ of a compactly supported smooth function is globally smooth and satisfies $\partial_{{\overset{ˉ}{z}}_{k}} T_{k} h = h$ (Local Cauchy transform with smooth parameters).

[F3]

For every $ℓ \neq k$ , the same whole-plane transform obeys $\partial_{{\overset{ˉ}{z}}_{ℓ}} T_{k} h = T_{k} (\partial_{{\overset{ˉ}{z}}_{ℓ}} h)$ (Local Cauchy transform with smooth parameters).

[F4]

AC says every family of nonempty sets has a choice function (The Axiom of Choice); the Cauchy transform supplier and Cauchy–Pompeiu formula both explicitly assume AC (Local Cauchy transform with smooth parameters, The Cauchy–Pompeiu formula with fixed signs).

[F5]

The support of a differential form is the closure of its nonzero locus; the form is compactly supported when that support is compact (Compact support of a differential form).

[F6]

A closure is a closed superset of the original set (Interior, closure, boundary, exterior, derived set and isolated point in a topological space).

[F7]

A closed subset of a compact space is compact (A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact).

[F8]

The complex Euclidean norm and metric agree under $C^{n} ≅ R^{2 n}$ , and in this metric a set is compact exactly when it is closed and bounded (Complex $m$ -space and its real coordinate dictionary).

[F9]

A set is bounded when it is empty or contained in a ball $B (c, r)$ for some center $c$ and radius $r > 0$ (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, Open ball, closed ball and sphere in a metric space).

[F10]

The Euclidean norm satisfies the triangle inequality $∥ x + y ∥ \leq ∥ x ∥ + ∥ y ∥$ (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms).

[F11]

In $R^{m}$ , the unit sphere is $S^{m - 1}$ (Euclidean spheres and closed balls as subspaces of $R^{n}$ ) and is path-connected for $m \geq 2$ (For $n \geq 2$ , the sphere $S^{n - 1}$ is path-connected and connected).

[F12]

Every path-connected space is connected (Every path-connected space is connected, and every path component lies inside a component).

[F13]

A connected component is the largest connected subset containing each of its points (Connected components, quasicomponents, and totally disconnected spaces).

[F14]

Each connected component of an open subset of $R^{m}$ is open (Every connected component of an open subset of $R^{n}$ is open and polygonally connected).

[F15]

For a $C^{1}$ function on an open subset of $C^{m}$ , the pointwise Cauchy–Riemann system implies complex differentiability, and complex differentiability at every point is holomorphy (For $C^{1}$ functions, holomorphy, complex linearity of the real derivative, and the Cauchy–Riemann system agree, Holomorphic functions on an open subset of $C^{m}$ ). Here take $m = n$ and match the theorem's zero-based coordinate index $0 \leq k < m$ with our one-based index $j = k + 1$ .

[F16]

A holomorphic function on a nonempty connected open set that vanishes on a nonempty open subset vanishes identically (A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically).

[F17]

For a bounded domain $D \subset C$ with $C^{1}$ boundary, full AC, $f \in C^{1} (\overline{D})$ , and $z \in D$ , Cauchy–Pompeiu gives $f (z) = \frac{1}{2 π i} \int_{\partial D} \frac{f (ζ)}{ζ - z} d ζ + \frac{1}{2 π i} \int_{D} \frac{\partial_{\overset{ˉ}{ζ}} f (ζ)}{ζ - z} d ζ \land d \overset{ˉ}{ζ} .$ (The Cauchy–Pompeiu formula with fixed signs)

Proof

technique · direct

1.1F1givenalgebra

By [F1], $\overset{ˉ}{\partial} g = \sum_{a, b} (\partial_{{\overset{ˉ}{z}}_{a}} g_{b}) d {\overset{ˉ}{z}}_{a} \land d {\overset{ˉ}{z}}_{b}$ ; for $a < b$ the coefficient of $d {\overset{ˉ}{z}}_{a} \land d {\overset{ˉ}{z}}_{b}$ is $\partial_{{\overset{ˉ}{z}}_{a}} g_{b} - \partial_{{\overset{ˉ}{z}}_{b}} g_{a}$ . Since $\overset{ˉ}{\partial} g = 0$ and the wedge expansion is unique, $\partial_{{\overset{ˉ}{z}}_{a}} g_{b} = \partial_{{\overset{ˉ}{z}}_{b}} g_{a}$ for all $a, b$ .

1.2F8F9F10F11F12F13givenalgebra

Put $K = supp g$ . If $K = \emptyset$ set $R = 1$ ; otherwise [F8]–[F9] give a ball $B (c, r)$ containing $K$ , and [F10] lets us take $R = ∥ c ∥ + r + 1$ so $K \subset {∥ z ∥ \leq R}$ . Let $E = {∥ z ∥ > R}$ . In $R^{2 n}$ , radial segments from any two points of $E$ to a common radius $L > R$ , joined by a rescaled path in $S^{2 n - 1}$ from [F11], stay in $E$ ; thus $E$ is path-connected and connected by [F12]. It is unbounded and lies in $Ω = C^{n} ∖ K$ . Fix $e = (R + 1, 0, \dots, 0) \in E$ and put $C_{\infty} = C_{Ω} (e)$ . Then $E \subseteq C_{\infty}$ by [F13], and every unbounded component of $Ω$ meets $E$ and equals $C_{\infty}$ by maximality; hence this is the unique unbounded component.

1.3F1F2F4F5F6F7givenalgebra

For each $j$ , $g_{j} \neq 0$ implies $g \neq 0$ by [F1]; hence $K_{j} : = \overline{{z : g_{j} (z) \neq 0}}$ is a closed subset of the compact set $K$ and is compact by [F5]–[F7]. Thus $g_{j} \in C_{c}^{\infty} (C^{n})$ . Define $u : = T_{1} g_{1}$ . Since the full AC hypothesis in [F4] is present, [F2] gives $u \in C^{\infty} (C^{n})$ and $\partial_{{\overset{ˉ}{z}}_{1}} u = g_{1}$ .

2.1F1F3F4F17step 1.1step 1.3givenalgebra

For $j > 1$ , [F3] and step 1.1 give $\partial_{{\overset{ˉ}{z}}_{j}} u = T_{1} (\partial_{{\overset{ˉ}{z}}_{j}} g_{1}) = T_{1} (\partial_{{\overset{ˉ}{z}}_{1}} g_{j})$ . Fix $z = (z_{1}, z_{2}, \dots, z_{n})$ and choose $M > \max (R, ∣ z_{1} ∣)$ ; the slice $h (ζ) = g_{j} (ζ, z_{2}, \dots, z_{n})$ is $C^{1}$ and vanishes on the boundary of the disc $D = {∣ ζ ∣ < M}$ because $K \subseteq {∥ z ∥ \leq R}$ . Applying [F17] to this slice at $z_{1}$ , its boundary term is zero. Since $\partial_{{\overset{ˉ}{z}}_{1}} g_{j} (ζ, z_{2}, \dots, z_{n}) = 0$ whenever $∣ ζ ∣ > R$ , the area integral over $D$ equals its whole-plane integral, namely $T_{1} (\partial_{{\overset{ˉ}{z}}_{1}} g_{j}) (z)$ . Thus [F17] gives $T_{1} (\partial_{{\overset{ˉ}{z}}_{1}} g_{j}) (z) = g_{j} (z)$ . Together with step 1.3 and the scalar case of [F1], this proves $\overset{ˉ}{\partial} u = g$ .

3.1F5F6F8F14F15F16step 1.2step 1.3step 2.1givenalgebra

The set $K$ is closed by [F5]–[F6], so $Ω$ is open. On $Ω$ we have $\overset{ˉ}{\partial} u = g = 0$ ; by [F15], $u$ is holomorphic there. The open half-space $V = {z : Re z_{2} > R}$ is nonempty, connected, unbounded, and contained in $Ω$ . For every $z \in V$ and every integration coordinate $ζ$ , $∥ (ζ, z_{2}, \dots, z_{n}) ∥ \geq ∣ z_{2} ∣ \geq Re z_{2} > R$ , so $g_{1} (ζ, z_{2}, \dots, z_{n}) = 0$ and the defining integral gives $u (z) = 0$ . By step 1.2, $V \subseteq C_{\infty}$ ; [F14] makes $C_{\infty}$ open. Applying [F16] on this connected open component yields $u = 0$ throughout $C_{\infty}$ .

4.1F5F6F8F9step 1.2step 3.1algebra

Since $E \subseteq C_{\infty}$ , step 3.1 gives $u = 0$ on the open exterior $E$ . Therefore $supp u = \overline{{z : u (z) \neq 0}}$ is closed and lies in ${∥ z ∥ \leq R} \subset B (0, R + 1)$ , so it is bounded by [F9]. By [F8], this closed bounded subset of complex Euclidean space is compact, and hence $u$ is compactly supported.

5.1F8F9F10F12F15F16step 2.1step 4.1givenalgebra∎

If $v$ is another smooth compactly supported solution, then $w = u - v$ is smooth and $\overset{ˉ}{\partial} w = 0$ , so [F15] makes $w$ holomorphic on all of $C^{n}$ . By [F8]–[F10], each compact support lies in a ball $B (c_{i}, r_{i})$ and the norm triangle inequality places both in one sufficiently large ball centred at $0$ ; hence $w = 0$ on a nonempty open exterior. Since $C^{n}$ is connected by straight paths and [F12], [F16] gives $w \equiv 0$ . Thus $u = v$ .

Depends on

Used by

Dependency tree · two levels

92 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 4 §4.2 (standard reference, not scraped)