LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-02

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 maximal distributional dbar operator is closed and densely defined

Statement

Assume the Axiom of Choice (AC). Let $Ω \subseteq C^{n}$ be open with $n \geq 1$ , let $0 \leq q \leq n$ , let $φ \in C^{2} (Ω; R)$ , let ${\overset{ˉ}{\partial}}_{q} : Dom {\overset{ˉ}{\partial}}_{q} \subseteq L_{0, q}^{2} (Ω, e^{- φ}) \to L_{0, q + 1}^{2} (Ω, e^{- φ})$ be the maximal distributional $\overset{ˉ}{\partial}$ of degree $q$ , and let ${\overset{ˉ}{\partial}}_{φ}^{*}$ be the Hilbert adjoint of ${\overset{ˉ}{\partial}}_{q - 1}$ , all with the conventions of Weighted L2 spaces and maximal dbar operators, including its one-based relabeling of the canonical coordinates.

$Dom {\overset{ˉ}{\partial}}_{q}$ is dense in $L_{0, q}^{2}$ , and ${\overset{ˉ}{\partial}}_{q}$ is closed.
For $1 \leq q \leq n$ and every $ψ \in C_{c}^{\infty} (Ω)$ of bidegree $(0, q)$ , $ψ$ lies in $Dom {\overset{ˉ}{\partial}}_{φ}^{*}$ , and ${\overset{ˉ}{\partial}}_{φ}^{*} ψ$ is the compactly supported form with $C^{1}$ coefficients $({\overset{ˉ}{\partial}}_{φ}^{*} ψ)_{K} = \sum_{j = 1}^{n} (ψ_{j K} \frac{\partial φ}{\partial z_{j}} - \frac{\partial ψ_{j K}}{\partial z_{j}}), ψ_{j K} : = 0 when j \in K .$
${\overset{ˉ}{\partial}}_{φ}^{*}$ is closed.

Facts & Assumptions

Given: The Axiom of Choice; an open set $Ω \subseteq C^{n}$ with $n \geq 1$ ; an integer $0 \leq q \leq n$ ; and a real function $φ \in C^{2} (Ω; R)$ .

[F1]

The weighted $(0, q)$ -space is $L_{0, q}^{2} (Ω, e^{- φ}) : = {u : u measurable, ∥ u ∥_{φ} < \infty} / \sim$ for the pairing $⟨ u, v ⟩_{φ} = \int_{Ω} \sum_{∣ J ∣ = q} u_{J} \overline{v_{J}} e^{- φ} d V$ (Weighted L2 spaces and maximal dbar operators).

[F2]

The maximal domain is $Dom {\overset{ˉ}{\partial}}_{q} : = {u \in L_{0, q}^{2} : \overset{ˉ}{\partial} u is represented by an element of L_{0, q + 1}^{2}}$ , where $\overset{ˉ}{\partial} u = \sum_{∣ J ∣ = q} \sum_{j} \frac{\partial u_{J}}{\partial {\overset{ˉ}{z}}_{j}} d {\overset{ˉ}{z}}_{j} \land d {\overset{ˉ}{z}}^{J}$ is the distributional derivative; for $u \in Dom {\overset{ˉ}{\partial}}_{q}$ the form ${\overset{ˉ}{\partial}}_{q} u$ is that representing element (Weighted L2 spaces and maximal dbar operators).

[F3]

The weighted adjoint satisfies $⟨ {\overset{ˉ}{\partial}}_{q - 1} u, v ⟩_{φ} = ⟨ u, {\overset{ˉ}{\partial}}_{φ}^{*} v ⟩_{φ}$ for all $u \in Dom {\overset{ˉ}{\partial}}_{q - 1}$ and $v \in Dom {\overset{ˉ}{\partial}}_{φ}^{*}$ , its formal density is $({\overset{ˉ}{\partial}}_{φ}^{*} v)_{K} = - e^{φ} \sum_{j} \partial_{z_{j}} (e^{- φ} v_{j K}) = \sum_{j} (v_{j K} \partial_{z_{j}} φ - \partial_{z_{j}} v_{j K})$ whenever $v \in Dom {\overset{ˉ}{\partial}}_{φ}^{*}$ , and coefficients are extended to non-increasing tuples by antisymmetry, with $v_{j K} = 0$ when $j \in K$ (Weighted L2 spaces and maximal dbar operators).

[F4]

Test forms are dense in the weighted space: every $u \in L_{0, q}^{2}$ is the $∥ \cdot ∥_{φ}$ -limit of a sequence of forms in $C_{c}^{\infty} (Ω)$ (Weighted L2 spaces and maximal dbar operators).

[F5]

Every coefficient of every $u \in L_{0, q}^{2}$ is locally integrable for Lebesgue measure on $Ω$ (Weighted L2 spaces and maximal dbar operators).

[F6]

Every smooth compactly supported $(0, q)$ -form has its smooth $\overset{ˉ}{\partial}$ in $L_{0, q + 1}^{2}$ , hence lies in $Dom {\overset{ˉ}{\partial}}_{q}$ (Weighted L2 spaces and maximal dbar operators).

[F7]

A weak derivative is characterized by the test identity $\int_{Ω} u D^{α} χ = (- 1)^{∣ α ∣} \int_{Ω} v χ$ for every real test function $χ \in C_{c}^{\infty} (Ω)$ (Weak derivative of a locally integrable function).

[F9]

An operator is densely defined when its domain is dense, and closed when its graph is a closed subset of $H \oplus H$ (Densely defined, closed and closable operators, and cores).

[F10]

A vector $y \in H$ lies in the adjoint domain exactly when $x \mapsto ⟨ T x, y ⟩$ is bounded on the domain, and then $T^{*} y$ is the unique $w$ with $⟨ T x, y ⟩ = ⟨ x, w ⟩$ for all $x$ in the domain (Adjoint of a densely defined operator).

[F11]

The published same-space adjoint theorem is not used for this operator between distinct form-degree Hilbert spaces; closedness is established directly in step 2.2.

[F12]

On every measure space the complex $L^{2}$ pairing satisfies $∣ ⟨ f, g ⟩ ∣ \leq ∥ f ∥_{2} ∥ g ∥_{2}$ , also for finite tuples (The complex $L^{2}$ pairing is well-defined and satisfies Cauchy–Schwarz).

[F13]

In a metric space a set is closed exactly when it is sequentially closed (A point lies in the closure of $A$ iff some sequence in $A$ converges to it, and a set is closed iff it is sequentially closed).

[F14]

AC implies the Axiom of Countable Choice ${A C}_{ω}$ (AC implies DC implies countable choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F15]

AC states that every family of nonempty sets has a choice function (The Axiom of Choice).

[F16]

The Wirtinger operator is $\partial_{{\overset{ˉ}{z}}_{j}} = \frac{1}{2} (\partial_{x_{j}} + i \partial_{y_{j}})$ (Wirtinger operators in $C^{m}$ ).

[F17]

For a compactly supported smooth unit-mass bump $b$ on Euclidean space, $b_{ε} (x) = ε^{- 2 n} b (x / ε)$ is its mollifier family, and convolution of a locally integrable function with $b_{ε}$ is smooth (The mollifier family generated by a unit-mass smooth bump, Convolution with a mollifier is smooth, and derivatives pass under the integral sign).

Choice use. AC is the ambient hypothesis recorded in the Statement, and ${A C}_{ω}$ is the countable instance consumed by the density interface [F4], by the adjoint definition [F10], and by the sequential characterization [F13]; [F14] is the exact implication supplying it. The proof selects no family: the test forms, the limiting form $v$ and the formal expression are given.

Proof

technique · direct

1.1F4F6F9F14given

By [F6] every smooth compactly supported $(0, q)$ -form lies in $Dom {\overset{ˉ}{\partial}}_{q}$ , and by [F4] these forms are dense in $L_{0, q}^{2}$ ; hence $Dom {\overset{ˉ}{\partial}}_{q}$ contains a dense subset and is itself dense in $L_{0, q}^{2}$ , which is the definition of ${\overset{ˉ}{\partial}}_{q}$ being densely defined in the sense of [F9]. The density interface [F4] is where the countable instance ${A C}_{ω}$ of [F14] is consumed.

1.2F1F2F3F5F7F16F17givenalgebra

Let $u \in Dom {\overset{ˉ}{\partial}}_{q}$ and $g = {\overset{ˉ}{\partial}}_{q} u$ . The unweighted distributional identity of [F2] extends from smooth compactly supported test forms to $C_{c}^{1}$ test forms. Indeed extend a $C_{c}^{1}$ test $h$ by zero to Euclidean space and convolve with a nonnegative unit-mass smooth bump as in [F17]. For sufficiently small $ε$ these smooth tests have supports in a fixed compact subset of $Ω$ , and $h * b_{ε} \to h$ together with every first derivative uniformly: differentiate under the integral in the expression $\int b_{ε} (y) h (x - y) d y$ and use uniform continuity of $h$ and its first derivatives. Local integrability of $u$ and $g$ then passes both sides of the test identity to the limit. For a smooth $(0, q + 1)$ -form $ψ$ of compact support, use the $C_{c}^{2}$ test coefficients $e^{- φ} \overline{ψ_{L}}$ . The coefficient sum in [F2], with its antisymmetric wedge signs, and the product rule give $⟨ g, ψ ⟩_{φ} = ⟨ u, \partial^{*} ψ ⟩_{φ}, (\partial^{*} ψ)_{K} = \sum_{j} (ψ_{j K} φ_{j} - \partial_{z_{j}} ψ_{j K}) .$ Only $g$ as a whole is assumed locally integrable; no individual weak derivative of a coefficient of $u$ is assumed to be a function.

1.3F1F2F5F7F9F12F13F14givenalgebra

The operator ${\overset{ˉ}{\partial}}_{q}$ is closed. Let $u_{k} \in Dom {\overset{ˉ}{\partial}}_{q}$ with $u_{k} \to u$ in $L_{0, q}^{2}$ and $g_{k} : = {\overset{ˉ}{\partial}}_{q} u_{k} \to v$ in $L_{0, q + 1}^{2}$ . On every compact $K \subseteq Ω$ , the positive minimum $c_{K}$ of $e^{- φ}$ gives $∥ u_{k} - u ∥_{L^{2} (K)} \leq c_{K}^{- 1 / 2} ∥ u_{k} - u ∥_{φ} \to 0$ , and the same bound holds for $g_{k} - v$ . Cauchy-Schwarz on $K$ therefore gives local $L^{1}$ convergence. Against any ordinary smooth compactly supported test form, both sides of the unweighted distributional identity for $\overset{ˉ}{\partial} u_{k} = g_{k}$ pass to the limit, since the test and its first derivatives are bounded. Thus $\overset{ˉ}{\partial} u = v$ as distributions, so [F2] gives $u \in Dom {\overset{ˉ}{\partial}}_{q}$ and ${\overset{ˉ}{\partial}}_{q} u = v$ . (For $q = n$ the operator is zero on the entire space and the conclusion is immediate.) The graph is sequentially closed in the metric direct sum of the two form-degree spaces, hence closed by [F13].

2.1F3F10F12F14step 1.1step 1.2givenalgebra

Let $ψ \in C_{c}^{\infty} (Ω)$ have bidegree $(0, q)$ with $1 \leq q \leq n$ , and let $\partial^{*} ψ$ be the formal expression of [F3]. Then $\partial^{*} ψ$ has compact support contained in $supp ψ$ and coefficients in $C^{1} (Ω)$ because $φ \in C^{2}$ and $ψ \in C_{c}^{\infty}$ , so $\partial^{*} ψ \in L_{0, q - 1}^{2}$ ; moreover step 1.1 makes ${\overset{ˉ}{\partial}}_{q - 1}$ densely defined, and step 1.2 gives $⟨ {\overset{ˉ}{\partial}}_{q - 1} u, ψ ⟩_{φ} = ⟨ u, \partial^{*} ψ ⟩_{φ}$ for every $u \in Dom {\overset{ˉ}{\partial}}_{q - 1}$ , so by [F12] the functional $u \mapsto ⟨ {\overset{ˉ}{\partial}}_{q - 1} u, ψ ⟩_{φ}$ is bounded on the domain with norm at most $∥ \partial^{*} ψ ∥_{φ}$ . By the characterization [F10] we therefore have $ψ \in Dom {\overset{ˉ}{\partial}}_{φ}^{*}$ and ${\overset{ˉ}{\partial}}_{φ}^{*} ψ = \partial^{*} ψ$ ; the countable choice used by the adjoint definition is supplied through [F14].

2.2F3F12F13step 1.1given

The adjoint ${\overset{ˉ}{\partial}}_{φ}^{*}$ is closed even though its source and target Hilbert spaces have different form degrees. Let $v_{m} \in Dom {\overset{ˉ}{\partial}}_{φ}^{*}$ satisfy $v_{m} \to v$ in $L_{0, q}^{2}$ and ${\overset{ˉ}{\partial}}_{φ}^{*} v_{m} \to w$ in $L_{0, q - 1}^{2}$ . For every $u \in Dom {\overset{ˉ}{\partial}}_{q - 1}$ the adjoint identity [F3] and continuity of the two inner products give $⟨ {\overset{ˉ}{\partial}}_{q - 1} u, v ⟩_{φ} = \lim_{m} ⟨ u, {\overset{ˉ}{\partial}}_{φ}^{*} v_{m} ⟩_{φ} = ⟨ u, w ⟩_{φ}$ . Thus $v$ lies in the adjoint domain and ${\overset{ˉ}{\partial}}_{φ}^{*} v = w$ by its definition [F3]. The graph is sequentially closed and hence closed by [F13].

3.1F3F15step 1.1step 2.1step 1.3step 2.2∎

Conclusion: $Dom {\overset{ˉ}{\partial}}_{q}$ is dense and ${\overset{ˉ}{\partial}}_{q}$ is closed by steps 1.1 and 1.3; every compactly supported smooth $(0, q)$ -test form lies in $Dom {\overset{ˉ}{\partial}}_{φ}^{*}$ with the formal weighted expression of [F3] by step 2.1; and ${\overset{ˉ}{\partial}}_{φ}^{*}$ is closed by step 2.2. This is exactly the content of the three claims of the Statement, and the ambient hypothesis is the AC recorded in the Statement and cited as [F15].

Depends on

Used by

Dependency tree · two levels

73 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

Jean-Pierre Demailly, Complex Analytic and Differential Geometry (standard reference, not scraped)
Harold P. Boas, Lecture Notes on Several Complex Variables (standard reference, not scraped)
Mohammad Jabbari, Several Complex Variables course notes (standard reference, not scraped)