TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 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.

Basic Bochner–Kodaira–Morrey estimate on $C^{n}$

Statement

Assume the Axiom of Choice (AC). Let $Ω \subseteq C^{n}$ be open with $n \geq 1$ . Use one-based labels $z_{j} : = z_{j - 1}^{c a n}$ for $1 \leq j \leq n$ , also for their derivatives and form coefficients. Let $φ \in C^{2} (Ω; R)$ , write

$D_{k} : = \frac{\partial}{\partial {\overset{ˉ}{z}}_{k}}, φ_{j} : = \frac{\partial φ}{\partial z_{j}}, φ_{j \overset{ˉ}{k}} : = \frac{\partial^{2} φ}{\partial z_{j} \partial {\overset{ˉ}{z}}_{k}},$

let $1 \leq q \leq n$ , and let $u$ be a compactly supported smooth $(0, q)$ -form on $Ω$ , with coefficients $u_{J}$ on increasing tuples extended to non-increasing tuples by antisymmetry, so that $u_{j J} = 0$ when $j \in J$ (Weighted L2 spaces and maximal dbar operators); the operators $\partial_{z_{j}}, \partial_{{\overset{ˉ}{z}}_{j}}$ are those of Wirtinger operators in $C^{m}$ . All sums over multi-indices below run over increasing tuples, $⟨ \cdot, \cdot ⟩_{φ}$ and $∥ \cdot ∥_{φ}$ are the inner product and norm of $L_{0, ∙}^{2} (Ω, e^{- φ})$ , and ${\overset{ˉ}{\partial}}_{φ}^{*}$ is the weighted Hilbert adjoint of ${\overset{ˉ}{\partial}}_{q - 1}$ (Weighted L2 spaces and maximal dbar operators).

(Exact Bochner–Kodaira–Morrey form.) The following identity holds, all integrals being finite:

$∥ \overset{ˉ}{\partial} u ∥_{φ}^{2} + ∥ {\overset{ˉ}{\partial}}_{φ}^{*} u ∥_{φ}^{2} = \sum_{∣ J ∣ = q} \sum_{k = 1}^{n} \int_{Ω} ∣ D_{k} u_{J} ∣^{2} e^{- φ} d V + \int_{Ω} \sum_{∣ J ∣ = q - 1} \sum_{j, k = 1}^{n} φ_{j \overset{ˉ}{k}} u_{j J} \overline{u_{k J}} e^{- φ} d V .$

(Levi inequality.) If in addition $φ$ is plurisubharmonic on $Ω$ , then

$∥ \overset{ˉ}{\partial} u ∥_{φ}^{2} + ∥ {\overset{ˉ}{\partial}}_{φ}^{*} u ∥_{φ}^{2} \geq \int_{Ω} \sum_{∣ J ∣ = q - 1} \sum_{j, k = 1}^{n} φ_{j \overset{ˉ}{k}} u_{j J} \overline{u_{k J}} e^{- φ} d V .$

Facts & Assumptions

Given: The Axiom of Choice; an open set $Ω \subseteq C^{n}$ with $n \geq 1$ ; a function $φ \in C^{2} (Ω; R)$ ; an integer $1 \leq q \leq n$ ; a compactly supported smooth $(0, q)$ -form $u$ ; and the notation $e_{j} : = d {\overset{ˉ}{z}}_{j}$ , $D_{j} : = \partial_{{\overset{ˉ}{z}}_{j}}$ , $δ_{j} : = φ_{j} - \partial_{z_{j}}$ acting coefficientwise, where the Wirtinger operators $\partial_{z_{j}}, \partial_{{\overset{ˉ}{z}}_{j}}$ are those fixed in the Statement, so that the holomorphic derivative, and not $D_{j} = \partial_{{\overset{ˉ}{z}}_{j}}$ , appears in $δ_{j}$ ; further $ε_{j} f : = e_{j} \land f$ on coefficient tensors, and $(ι_{j} w)_{K} : = w_{j K}$ for increasing $K$ .

[F1]

The weighted inner product and norm on coefficient tuples of bidegree $(0, q)$ are $⟨ v, w ⟩_{φ} = \int_{Ω} \sum_{∣ J ∣ = q} v_{J} \overline{w_{J}} e^{- φ} d V$ and $∥ v ∥_{φ}^{2} = ⟨ v, v ⟩_{φ}$ (Weighted L2 spaces and maximal dbar operators).

[F2]

The distributional derivative of $u \in L_{0, q}^{2}$ is $\overset{ˉ}{\partial} u = \sum_{∣ J ∣ = q} \sum_{j = 1}^{n} (\partial u_{J} / \partial {\overset{ˉ}{z}}_{j}) d {\overset{ˉ}{z}}_{j} \land d {\overset{ˉ}{z}}^{J}$ (Weighted L2 spaces and maximal dbar operators).

[F3]

The weighted adjoint is characterized by $⟨ {\overset{ˉ}{\partial}}_{q - 1} v, w ⟩_{φ} = ⟨ v, {\overset{ˉ}{\partial}}_{φ}^{*} w ⟩_{φ}$ for all $v \in Dom {\overset{ˉ}{\partial}}_{q - 1}$ and $w \in Dom {\overset{ˉ}{\partial}}_{φ}^{*}$ (Weighted L2 spaces and maximal dbar operators).

[F4]

Coefficients are extended to non-increasing tuples by antisymmetry, so that $v_{j K} = 0$ when $j \in K$ (Weighted L2 spaces and maximal dbar operators).

[F5]

The conventions $L_{0, q}^{2} = {0}$ and ${\overset{ˉ}{\partial}}_{q} = 0$ are in force for $q < 0$ and for $q > n$ (Weighted L2 spaces and maximal dbar operators).

[F6]

For $1 \leq q \leq n$ every $ψ \in C_{c}^{\infty} (Ω)$ of bidegree $(0, q)$ lies in $Dom {\overset{ˉ}{\partial}}_{φ}^{*}$ , and $({\overset{ˉ}{\partial}}_{φ}^{*} ψ)_{K} = \sum_{j = 1}^{n} (ψ_{j K} φ_{j} - \partial_{z_{j}} ψ_{j K})$ (The maximal distributional dbar operator is closed and densely defined).

[F7]

Wedge multiplication of basis vectors is multilinear and alternating, so $e_{i} \land e_{i} = 0$ and transposing two neighbouring entries changes the sign; it is also associative, and the strictly increasing monomials form a basis; hence for a distinct $i$ and an increasing tuple $I = (i_{1} < \dots < i_{p})$ one has $e_{i} \land e_{I} = (- 1)^{# {i_{j} < i}} e_{sort ({i} \cup I)}$ , while $e_{i} \land e_{I} = 0$ when $i \in I$ (The basic wedge map $(v_{1}, \dots, v_{k}) \mapsto v_{1} \land \dots \land v_{k}$ is multilinear and alternating, Exterior multiplication is well defined, graded, associative, unital, and graded-commutative, Wedge monomials in a dual basis form a basis).

[F8]

The Levi form is $L_{u} (a; v) = \sum_{j = 1}^{m} \sum_{k = 1}^{m} \frac{\partial^{2} u}{\partial z_{j} \partial {\overline{z}}_{k}} (a) v_{j} \overline{v_{k}}$ (The Levi form and strict plurisubharmonicity).

[F9]

A $C^{2}$ real-valued function is plurisubharmonic if and only if its Levi form is pointwise semidefinite nonnegative (The C^2 Levi criterion for plurisubharmonicity).

[F10]

For a function with continuous second partial derivatives, $\partial_{j} \partial_{i} ϕ = \partial_{i} \partial_{j} ϕ$ (Continuous second partials of a scalar potential commute).

[F11]

On every measure space the complex $L^{2}$ pairing is linear in the first variable, conjugate-linear in the second, conjugate symmetric and positive definite (The complex $L^{2}$ pairing is well-defined and satisfies Cauchy–Schwarz).

[F12]

$A C \Rightarrow D C \Rightarrow {A C}_{ω}$ in ZF (AC implies DC implies countable choice).

[F13]

The Axiom of Countable Choice ${A C}_{ω}$ supplies a choice function for every at most countable family of nonempty sets (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F14]

The Axiom of Choice supplies a choice function for every family of nonempty sets (The Axiom of Choice).

Choice use. AC is the ambient hypothesis recorded in the Statement and cited as [F14]; the countable instance [F13] is the form of choice consumed by the constructions behind [F1] (completeness and density of the weighted space) and [F6] (the maximal operator and its adjoint on compactly supported smooth forms), and [F12] is the exact implication AC $\Rightarrow$ DC $\Rightarrow$ AC $_{ω}$ supplying it. The proof itself selects no family of nonempty sets: the form, its coefficients, the weight and the finitely many index sets in the sums are all given.

Proof

technique · direct

1.1F4F7givenalgebra

The notation of the given block is well defined on coefficient tensors, and for increasing $L$ the sign rule [F7] gives $e_{k} \land e_{L} = ϵ (k, L) e_{L \cup k}$ for $k \notin L$ and $e_{k} \land e_{L} = 0$ for $k \in L$ , while the antisymmetry convention [F4] gives $ι_{j} e_{L} = ϵ (j, L ∖ j) e_{L ∖ j}$ for $j \in L$ and $ι_{j} e_{L} = 0$ for $j \notin L$ , where $ϵ (a, M) : = (- 1)^{# {m \in M : m < a}}$ ; consequently the Clifford relation $ι_{j} ε_{k} + ε_{k} ι_{j} = δ_{j k} i d$ holds, because for $j = k \in L$ one has $ι_{j} ε_{j} e_{L} = 0$ and $ε_{j} ι_{j} e_{L} = e_{L}$ , for $j = k \notin L$ one has $ι_{j} ε_{j} e_{L} = e_{L}$ and $ε_{j} ι_{j} e_{L} = 0$ , for $j \neq k$ with $j \notin L$ both terms vanish since an index occurring twice wedges to zero, and for $j \neq k$ with $j \in L$ the terms vanish when $k \in L$ and otherwise cancel by the sign identity $ϵ (k, L) ϵ (j, (L ∖ j) \cup k) = - ϵ (j, L ∖ j) ϵ (k, L ∖ j)$ , whose two exponents differ by exactly one because exactly one of $j < k$ , $k < j$ holds.

1.2F1F4F7F11givenalgebra

For coefficient tensors $f$ of degree $p$ and $w$ of degree $p + 1$ with compactly supported smooth coefficients, $⟨ ε_{j} f, w ⟩_{φ} = ⟨ f, ι_{j} w ⟩_{φ}$ : by [F11] both sides are sesquilinear in $(f, w)$ , and on constant basis tensors $f = e_{I}$ , $w = e_{L}$ the formulas above from [F7] and [F4] give $(ε_{j} e_{I})_{L} = ϵ (j, I) δ_{L, I \cup j}$ and $(ι_{j} e_{L})_{I} = ϵ (j, L ∖ j) δ_{I, L ∖ j}$ , which are equal since $L = I \cup j$ exactly when $I = L ∖ j$ ; multiplying the pointwise identity by the positive factor $e^{- φ}$ and integrating with the pairing of [F1] gives the weighted statement.

1.3F1F2F3F6F11givenalgebra

For all $f, g \in C_{c}^{\infty} (Ω)$ one has $⟨ D_{j} f, g ⟩_{φ} = ⟨ f, δ_{j} g ⟩_{φ}$ , and hence also $⟨ δ_{j} f, g ⟩_{φ} = ⟨ f, D_{j} g ⟩_{φ}$ by conjugate symmetry; indeed, $f$ is a compactly supported smooth $(0, 0)$ -form and $g e_{j}$ a compactly supported smooth $(0, 1)$ -form lying in $Dom {\overset{ˉ}{\partial}}_{φ}^{*}$ with ${\overset{ˉ}{\partial}}_{φ}^{*} (g e_{j}) = δ_{j} g$ by [F6], while [F2] gives $\overset{ˉ}{\partial} f = \sum_{k} D_{k} f e_{k}$ , so the characterizing identity [F3] reads $\sum_{k} δ_{k j} ⟨ D_{k} f, g ⟩_{φ} = ⟨ f, δ_{j} g ⟩_{φ}$ .

1.4F2F6givenalgebra

On compactly supported smooth forms the operator identities $\overset{ˉ}{\partial} = \sum_{k} ε_{k} D_{k}$ and ${\overset{ˉ}{\partial}}_{φ}^{*} = \sum_{j} ι_{j} δ_{j}$ hold pointwise in the increasing coefficients, the first because [F2] expands $\overset{ˉ}{\partial}$ as the sum of the wedges $(D_{k} u_{J}) e_{k} \land e_{J}$ , and the second because the coefficient formula of [F6] is $\sum_{j} δ_{j} (ψ_{j K})$ on each increasing $K$ , which is what $\sum_{j} ι_{j} δ_{j}$ produces; consequently the self-adjoint-shaped operator $□ : = {\overset{ˉ}{\partial}}_{φ}^{*} \overset{ˉ}{\partial} + \overset{ˉ}{\partial} {\overset{ˉ}{\partial}}_{φ}^{*}$ satisfies $□ = \sum_{j, k} (ι_{j} δ_{j} ε_{k} D_{k} + ε_{k} D_{k} ι_{j} δ_{j})$ on those forms.

2.1F10step 1.1step 1.4givenalgebra

The operator identity $□ = \sum_{j} δ_{j} D_{j} + \sum_{j, k} φ_{j \overset{ˉ}{k}} ε_{k} ι_{j}$ holds on compactly supported smooth forms: by the identities of step 1.4, the constant-coefficient form operators $ε_{k}, ι_{j}$ commute with the coefficientwise operators $δ_{j}, D_{k}$ , and by the Clifford relation of step 1.1 one has $ι_{j} δ_{j} ε_{k} D_{k} = ι_{j} ε_{k} δ_{j} D_{k} = δ_{j k} δ_{j} D_{k} - ε_{k} ι_{j} δ_{j} D_{k}$ and $ε_{k} D_{k} ι_{j} δ_{j} = ε_{k} ι_{j} D_{k} δ_{j}$ , so $□ = \sum_{j} δ_{j} D_{j} + \sum_{j, k} ε_{k} ι_{j} (D_{k} δ_{j} - δ_{j} D_{k})$ ; the commutator acting coefficientwise is the multiplication operator $D_{k} φ_{j}$ , since the coefficientwise derivatives commute and only the term where $D_{k}$ hits $φ_{j}$ survives, and $D_{k} φ_{j} = \partial_{{\overset{ˉ}{z}}_{k}} \partial_{z_{j}} φ = φ_{j \overset{ˉ}{k}}$ by clairaut [F10].

2.2F1F3F5F6F11step 1.4givenalgebra

The left-hand side of claim 1 equals $⟨ □ u, u ⟩_{φ}$ : since $u$ and its images are compactly supported smooth forms lying in the relevant domains, with $\overset{ˉ}{\partial} u = 0$ by the degree convention [F5] when $q = n$ , the characterizing adjoint identity [F3] applied to the pairs $(u, \overset{ˉ}{\partial} u)$ and $({\overset{ˉ}{\partial}}_{φ}^{*} u, u)$ gives $⟨ u, {\overset{ˉ}{\partial}}_{φ}^{*} \overset{ˉ}{\partial} u ⟩_{φ} = ⟨ \overset{ˉ}{\partial} u, \overset{ˉ}{\partial} u ⟩_{φ} = ∥ \overset{ˉ}{\partial} u ∥_{φ}^{2}$ and $⟨ \overset{ˉ}{\partial} {\overset{ˉ}{\partial}}_{φ}^{*} u, u ⟩_{φ} = ⟨ {\overset{ˉ}{\partial}}_{φ}^{*} u, {\overset{ˉ}{\partial}}_{φ}^{*} u ⟩_{φ} = ∥ {\overset{ˉ}{\partial}}_{φ}^{*} u ∥_{φ}^{2}$ , while conjugate symmetry [F11] turns the first expression into $⟨ {\overset{ˉ}{\partial}}_{φ}^{*} \overset{ˉ}{\partial} u, u ⟩_{φ}$ because [F1] makes it a real number; adding the two terms and using the definition of $□$ from step 1.4 gives the claim.

3.1F1step 1.2step 1.3step 2.1step 2.2algebra

The two summands of $⟨ □ u, u ⟩_{φ}$ evaluate as $\sum_{j} ⟨ δ_{j} D_{j} u, u ⟩_{φ} = \sum_{j} ⟨ D_{j} u, D_{j} u ⟩_{φ} = \sum_{∣ J ∣ = q} \sum_{k} \int_{Ω} ∣ D_{k} u_{J} ∣^{2} e^{- φ} d V$ by the adjoint identity of step 1.3, and $\sum_{j, k} ⟨ φ_{j \overset{ˉ}{k}} ε_{k} ι_{j} u, u ⟩_{φ} = \sum_{j, k} ⟨ ε_{k} (φ_{j \overset{ˉ}{k}} ι_{j} u), u ⟩_{φ} = \sum_{j, k} ⟨ φ_{j \overset{ˉ}{k}} ι_{j} u, ι_{k} u ⟩_{φ} = \sum_{j, k} \int_{Ω} \sum_{∣ J ∣ = q - 1} φ_{j \overset{ˉ}{k}} u_{j J} \overline{u_{k J}} e^{- φ} d V$ by the adjointness of step 1.2, the scalar commutation of $ε_{k}$ and the pairing formula [F1]; adding these two evaluations through the decomposition of step 2.1 and combining with step 2.2 proves claim 1.

4.1F8F9step 3.1givenalgebra

If $φ$ is plurisubharmonic, the Levi criterion [F9] applied to the Levi form [F8] gives $\sum_{j, k} φ_{j \overset{ˉ}{k}} (a) ξ_{j} \overline{ξ_{k}} \geq 0$ for every $a \in Ω$ and $ξ \in C^{n}$ , and applying this at each point with the given coefficients $ξ_{j} : = u_{j J} (a)$ , for every increasing $J$ of size $q - 1$ , exhibits the integrand of the second term in step 3.1 as a sum of nonnegative quantities; the first term of step 3.1 is a sum of squares of absolute values, hence also nonnegative, so dropping it from the identity of claim 1 yields the inequality of claim 2.

5.1F12F13F14step 3.1step 4.1∎

Both claims of the Statement are proved: claim 1 is the identity assembled in step 3.1, and claim 2 follows from it by the nonnegativity established in step 4.1; the ambient hypothesis is the AC recorded in the Statement and cited as [F14], its countable instance is [F13] as supplied through [F12] by the interfaces [F1] and [F6], and no family of nonempty sets is selected anywhere in the argument.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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

Basic Bochner–Kodaira–Morrey estimate on CnCn