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.
Hörmander's weighted L2 existence theorem for the dbar equation
Statement
Assume the Axiom of Choice (AC). Let and use one-based labels for , also for their derivatives and form coefficients. Let be a domain that is Hartogs pseudoconvex (Plurisubharmonic exhaustions and Hartogs pseudoconvexity), let be strictly plurisubharmonic on (The Levi form and strict plurisubharmonicity), and let . For let be the eigenvalues of the Hermitian matrix and put , so that on . Write and let be the maximal distributional of Weighted L2 spaces and maximal dbar operators.
-
If satisfies and the weighted energy is finite, then there is with and .
-
(Smooth data.) If in addition and satisfies pointwise and , then there is with and .
The strict positivity of is kept in both claims, and no boundary regularity of is claimed. Claim 2 is the branch of the same weighted estimate, quoted from the source of [F19]; it does not assert that the solution of claim 1 is smooth.
Facts & Assumptions
Given: The Axiom of Choice; an integer ; a domain that is Hartogs pseudoconvex; a function strictly plurisubharmonic on ; an integer ; the eigenvalue functions of the Hermitian matrices , , and ; and a form with whose energy is finite.
With the conventions of Weighted L2 spaces and maximal dbar operators: the space of coefficient tuples carries the inner product and is a complex Hilbert space.
With the same conventions, for with a locally integrable representative the distributional form is defined, and consists of those for which is represented by an element of , which is then (Weighted L2 spaces and maximal dbar operators).
Coefficients are extended to non-increasing tuples by antisymmetry, so that when , and this convention assigns the shuffle signs in the coefficient formula of [F2] (Weighted L2 spaces and maximal dbar operators).
The bidegree decomposition and the coefficient formula for smooth forms are as recorded in Bigraded complex forms and the Dolbeault operators; a smooth -form is identified with its tuple of coefficients and denotes the smooth compactly supported -forms.
A weak derivative is defined by the test identity for every , and it is a statement about almost-everywhere classes (Weak derivative of a locally integrable function).
The Levi form of is , and is strictly plurisubharmonic when for every and every (The Levi form and strict plurisubharmonicity).
A domain with boundary is Levi pseudoconvex when for every boundary point there are a neighbourhood of and a function with , , and for every complex tangent vector (Levi pseudoconvex domains).
A domain is Hartogs pseudoconvex when is plurisubharmonic on , where is the equal-radius polydisc boundary function; the whole space is Hartogs pseudoconvex by the empty-complement convention (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).
If is a Hartogs pseudoconvex domain, then there are strictly plurisubharmonic and a strictly increasing sequence such that, with : every is a regular value of , every is a nonempty hypersurface of , and , and for every and every with (Smooth strictly plurisubharmonic exhaustion of a pseudoconvex domain).
Weighted solvability on a smoothly bounded domain (Weighted ∂̄ solvability on a smoothly bounded pseudoconvex domain): if is a bounded Levi pseudoconvex domain with boundary, is strictly plurisubharmonic at every point of , , and satisfies , then there is with , and the least-norm such solution satisfies with the sum of the smallest eigenvalues of the Hermitian matrices on .
The Wirtinger operators satisfy and (Wirtinger operators in ).
For functions with continuous second partial derivatives the mixed second partials commute (Continuous second partials of a scalar potential commute).
A finite-dimensional complex inner product space has an orthonormal basis of eigenvectors of every normal endomorphism (Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely).
An endomorphism is self-adjoint exactly when its matrix in an orthonormal basis is Hermitian, and every self-adjoint endomorphism is normal (In an orthonormal basis, self-adjoint means conjugate-transpose symmetry and normal means commuting with the conjugate transpose, Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space).
A finite orthonormal list satisfies for every , with equality when is an orthonormal basis (Bessel's inequality for a finite orthonormal list and Parseval's identity for an orthonormal basis).
Under the Axiom of Countable Choice every complete real or complex inner-product space is reflexive (Hilbert spaces are reflexive by Riesz representation).
Under the ultrafilter lemma, DC and HB, a real or complex Banach space is reflexive if and only if every norm-bounded sequence in has a subsequence converging weakly to a point of (Reflexivity is equivalent to weak subsequential compactness of bounded sequences).
Under HB, if a net in a real or complex normed space, then , with no boundedness or completeness hypothesis (Weak convergence implies lower semicontinuity of the norm).
The Axiom of Choice implies the ultrafilter lemma (The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter).
The Axiom of Choice implies HB, the real dominated-extension principle (Hahn-Banach dominated extension theorem for real vector spaces).
In ZF, AC implies the Axiom of Countable Choice and the prescribed-initial-point form of Dependent Choice (AC supplies the countable and dependent choices used in Banach integration).
AC is the assertion that every family of nonempty sets has a choice function (The Axiom of Choice); DC is the prescribed-initial-point form of The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain; AC selects from every at most countable family of nonempty sets (The Axiom of Countable Choice ()); HB is the real dominated-extension principle over ZF (The real dominated-extension principle as an additional hypothesis over ZF).
(Demailly, Ch. VIII, Theorem 6.5 and its proof, printed p. 378, with (6.4) on p. 377.) On a weakly pseudoconvex Kähler manifold with a hermitian line bundle and a smooth weight having nonnegative curvature eigenvalues, a smooth closed -form of finite reciprocal-eigenvalue energy has a smooth solution with the corresponding norm bound. No global hypothesis on the datum is required. Here use the trivial line bundle and the flat normalization in which are orthonormal; the eigenvalues are those of and the metric volume is a constant multiple of . Put . The map commutes with and preserves coefficient norms, so the source bound transfers to -forms; the common volume constant cancels.
Weak convergence of a net means convergence against every bounded linear functional; a sequence is the case (Weak convergence of nets and sequences).
Under the complex Euclidean dictionary, is an open connected subset of , hence any two points can be joined by a polygonal path in (Complex -space and its real coordinate dictionary, For an open subset of , connectedness, path-connectedness and polygonal connectedness are equivalent).
Choice use. AC is the ambient hypothesis recorded in the Statement and cited as [F23]; its countable instance AC is consumed through the reflexive-Hilbert-space supplier [F16] and licenses the countably many applications of [F10] in step 2.2 that produce the sequence , and DC and HB are consumed through the reflexivity criterion [F17]; the consequences AC ultrafilter lemma, AC HB and AC (DC and AC) are supplied by [F20], [F21] and [F22]. No other family of nonempty sets is selected, and apart from the interfaces named above no step uses choice beyond the definitions and the cited interfaces.
Proof
By [F8] and [F9] choose a smooth strictly plurisubharmonic exhaustion and increasing regular values , with relatively compact and exhausting . Fix and discard an initial finite segment so that for every remaining . Let be the connected component of containing ; these components are nested. They exhaust : for , [F25] gives a polygonal path from to , whose compact image lies in some by the increasing open cover, so . Each is bounded because is compact. At one has ; the regular-level chart makes a connected local subgraph near , and its inside part meets , so it lies in . Thus has boundary locally defined by with . Strict plurisubharmonicity gives on every nonzero complex tangent vector, so is a bounded Levi pseudoconvex domain to which [F10] applies.
For write and . Reality of , the Wirtinger formulas [F11] and commutation of mixed partials [F12] give , so and are Hermitian and are self-adjoint by [F14]. Their characteristic polynomials agree, since , so they have the same ordered eigenvalues . With the first-variable-linear inner product, Thus strict plurisubharmonicity [F6] makes positive definite. Its orthonormal eigenbasis from [F13] shows that , hence every eigenvalue of is positive and .
For each let be the restriction of to , that is the tuple of restrictions . Then with because and the integrand is nonnegative, and with : distributional differentiation is local, so the coefficient distributions of on are obtained by evaluating those of on test functions supported in , and the coefficient formula and test identity of [F2], [F4] and [F5] pair them with the test functions , , exactly as pairs with the zero extensions of to ; since the distribution is represented by the zero form by the hypothesis , its restriction to is represented by the zero form as well.
Fix a test form and let be the -form with coefficients ; then, writing , is compactly supported, of class , and lies in , and for every one has the distributional identity , where the left side evaluates the coefficient distributions of F2 against the test functions and the antisymmetry convention of [F3] assigns the shuffle signs: both sides equal the single sum , the left by the test identity of [F5] and the sign convention for of [F4], and the right by expanding the pairing of F1 with and conjugating the holomorphic derivative by the Wirtinger rules [F11].
The function is upper semicontinuous, hence Borel measurable, on : for every orthonormal -frame the function is continuous, and over the nonempty set of orthonormal -frames, because expanding in an eigenbasis of step 1.2 gives with by the Bessel inequality of [F15] and by its Parseval clause, and for such a mass vector , with equality for ; hence is a union of open sets, and since on by step 1.2 the integrand is a nonnegative measurable function, so that the energy of the statement is a well-defined extended Lebesgue integral.
Fix and take . The domain is a bounded Levi pseudoconvex domain with boundary, the weight lies in on a neighbourhood of and is strictly plurisubharmonic at every point of by step 1.2 and the hypothesis, and the datum lies in with by step 1.3; all hypotheses of [F10] are therefore met, and its conclusion supplies the least-norm solution of with , where the eigenvalue functions named in [F10] are the functions of step 1.2 and the last inequality is step 1.3 with the nonnegative integrand and .
Extend each by zero: let equal on and on , regarded as a coefficient tuple. Then with measurable coefficients, by step 2.2, and consequently is a norm-bounded sequence in the complex Hilbert space of [F1].
Let and let be an index with , which exists because the sets increase to by step 1.1 while is compact; for every the left side of the identity of step 1.4 with equals : on the open set the tuples and agree, so by the locality of distributional differentiation the coefficient distributions of evaluated against the test functions depend only on , and there the identity of step 2.2 represents them by the coefficients .
The space is reflexive by [F16], whose countable-choice hypothesis is the instance AC supplied by AC through [F22]; by [F17], whose ultrafilter-lemma, DC and HB hypotheses are supplied from AC by [F20], [F22] and [F21], a reflexive complex Banach space has the property that the norm-bounded sequence admits a subsequence converging weakly in to some .
By [F18], whose HB hypothesis is supplied from AC by [F21], applied to the weakly convergent sequence of step 4.1 one has , and for every by step 3.1, so that and .
Let . By step 1.4 the left side of its identity with equals , and this scalar converges to as because and weakly (step 4.1 and the characterization of weak convergence by bounded functionals in [F24]); by step 3.2 the same scalar equals for all sufficiently large , so , and by step 1.4 applied with , whose left side is by construction the pairing of the coefficient distributions of with the test form , the distribution is represented by the form ; by the definition of the maximal operator F2 this says and .
Claim 1 holds: the element of step 5.2 lies in with , and by step 5.1. Claim 2 holds by the source fact [F19] under its hypotheses: with the Euclidean Kähler form is a weakly pseudoconvex Kähler manifold because the exhaustion of [F9] is a plurisubharmonic exhaustion, has nonnegative eigenvalues , and the smooth -closed form has finite energy, so the branch of the quoted theorem supplies with and the same weighted bound; no boundary regularity of is asserted in either claim, and both claims are stated under the ambient Axiom of Choice cited as [F23].
Depends on
For an open subset of , connectedness, path-connectedness and polygonal connectedness are equivalent
Complex -space and its real coordinate dictionary
Weighted L2 spaces and maximal dbar operators
Bigraded complex forms and the Dolbeault operators
Weak derivative of a locally integrable function
The Levi form and strict plurisubharmonicity
Levi pseudoconvex domains
Plurisubharmonic exhaustions and Hartogs pseudoconvexity
Smooth strictly plurisubharmonic exhaustion of a pseudoconvex domain
Weighted ∂̄ solvability on a smoothly bounded pseudoconvex domain
Wirtinger operators in
Continuous second partials of a scalar potential commute
Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely
In an orthonormal basis, self-adjoint means conjugate-transpose symmetry and normal means commuting with the conjugate transpose
Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space
Bessel's inequality for a finite orthonormal list and Parseval's identity for an orthonormal basis
Hilbert spaces are reflexive by Riesz representation
Reflexivity is equivalent to weak subsequential compactness of bounded sequences
Weak convergence implies lower semicontinuity of the norm
Weak convergence of nets and sequences
The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter
Hahn-Banach dominated extension theorem for real vector spaces
AC supplies the countable and dependent choices used in Banach integration
The real dominated-extension principle as an additional hypothesis over ZF
The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain
The Axiom of Countable Choice ()
The Axiom of Choice