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 Estimates and the Levi Problem
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Algebraic Closure, Embeddings, and Separability
- Algebraic Extensions, Extension Degree, and Finite Fields
- Analyticity of Holomorphic Functions; Liouville and Morera
- Approximation and Compactness in C(K)
- Arc Length and Rectifiable Curves
- Areas of Elementary Plane Figures
- Banach Alaoglu Goldstine and Krein Milman
- Banach Valued Integration and the Radon Nikodym Property
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Linear Operators and Quotient Spaces
- Bounded Variation and the Riemann–Stieltjes Integral
- Compactness
- Compactness in Metric Spaces
- Complete Metrizability, Čech-Completeness, and Baire Category
- Completeness, Completion, and Uniform Continuity
- Complex Differentiability and the Cauchy–Riemann Equations
- Complex Lp Spaces and Test-Function Conventions
- Complex Power Series and Analytic Functions
- Composition Series, the Jordan–Hölder Theorem and Solvable Groups
- Congruences, the Integers Modulo n and the Chinese Remainder Theorem
- Connectedness
- Constant Rank, Submersions, Immersions and Regular Level Sets
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Contour Integration
- Convergence: Nets and Filters
- Convex and Semicontinuous Functions on Rⁿ
- Convexity
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Countability Axioms and Cardinal Functions
- Cyclic Groups and Direct Products
- Darboux, L'Hôpital, and Taylor's Theorem
- Density Separability and Convolution in Lᵖ
- Determinants of Matrices over a Commutative Ring
- Diagonalisation and the Minimal Polynomial
- Distributions Test Functions and Differentiation
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Domains of Holomorphy, Plurisubharmonicity and Pseudoconvexity
- Dual Spaces Adjoint Operators and Annihilators
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Eigenvalues, Eigenvectors and the Characteristic Polynomial
- Exterior Powers, Orientation and Hodge Duality
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Free Modules, Exact Sequences, Projective and Injective Modules
- Fubini and Change of Variables
- Function Space Topologies and the Exponential Law
- Fundamental Trigonometric Identities
- Gaussian Elimination, Elementary Matrices and Reduced Row Echelon Form
- Goursat's Theorem and Cauchy's Theorem in a Convex Domain
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Harmonic Functions and the Poisson Integral
- Hausdorff via the Diagonal
- Hereditary and Productive Behaviour of the Separation Axioms
- Hilbert Space Geometry and Riesz Representation
- Holomorphic Functions of Several Complex Variables
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Lebesgue Measure on Euclidean Space
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Line Integrals and the Gradient Theorem
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Measurable Functions and Simple Approximation
- Measures and Their Basic Properties
- Metric Spaces
- Mixed Partials, Taylor Formulae, and Extrema
- Modes of Convergence Egorov and Lusin
- Modules, Submodules, Quotient Modules and the Isomorphism Theorems
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Normed and Banach Spaces
- Norming and Separation under Hahn–Banach
- Order, Zorn's Lemma, and the Axiom of Choice
- Outer Measure and the Caratheodory Extension Theorem
- Partitions of Unity and Paracompactness
- pi: the Equivalent Characterizations
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Primes, Euclid's Lemma and the Fundamental Theorem of Arithmetic
- Product Measures and the Fubini Tonelli Theorems
- Properties of the Integral and the Working FTC
- Rank Theorems and Embedded Submanifolds
- Reflexivity and Eberlein Smulian
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sard Theorem and Transversality
- Schwartz Space and the Plancherel Theorem
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Sigma Algebras and Borel Sets
- Simple Field Extensions and the Construction of the Complex Numbers
- Sine, Cosine, and the Definition of Pi
- Smooth Manifolds and Smooth Maps
- Smooth Partitions of Unity and Exhaustions
- Smooth Vector Bundles and Sections
- Splitting Fields
- Stone–Weierstrass in General
- Subharmonic Functions and the Dirichlet Problem
- Subspaces, Products, and Quotients
- Suprema and Infima
- Sylow's Theorems, p-Groups and Nilpotent Groups
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- Tangent Cotangent and the Differential
- Tensor Fields Exterior Algebra and Differential Forms
- Tensor Products of Modules
- The Analytic Hahn Banach Theorem
- The Baire Principles of Functional Analysis
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Complex Exponential and Euler's Formula
- The Derivative and the Mean Value Theorems
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Dolbeault Complex and Integral Solutions
- The Exponential Function
- The Exterior Derivative and Cartan Calculus
- The Fundamental Theorem of Algebra
- The Fundamental Theorem of Finite Abelian Groups
- The Fundamental Theorems of Calculus
- The Galois Correspondence
- The Hartogs Phenomena
- The Identity Theorem, the Maximum Principle and the Open Mapping Theorem
- The Inverse and Implicit Function Theorems
- The Inverse Function Theorem Completed
- The Lebesgue Integral and the Convergence Theorems
- The Logarithm and General Powers
- The Lᵖ Spaces Holder Minkowski and Riesz Fischer
- The Maximal Function and Lebesgue Differentiation
- The Riemann Integral in Rᵐ and Jordan Content
- The Riemann Integral: Definition and Integrability
- The Spectral Theorem, Positive Operators and Singular Value Decomposition
- The Topology of Euclidean Space
- The Total Derivative in ℝᵐ → ℝⁿ
- The Winding Number and the Global Cauchy Theorem
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Triangularisation, Generalised Eigenspaces and Jordan Canonical Form
- Unbounded Self Adjoint Operators and Stones Theorem
- Vector Fields Flows and Lie Derivatives
- Vector Spaces, Linear Subspaces, Span and Direct Sums
- Weak and Weak Star Topologies
- Weak Derivatives and Sobolev Spaces
2 · Summary
This page proves weighted estimates for the -equation on pseudoconvex domains and records a sourced solution of the Levi problem. The first half sets up the weighted Hilbert spaces of -forms with their maximal distributional and weighted adjoint, solves the abstract Hilbert-complex problem from a coercive estimate, and records the Bochner-Kodaira-Morrey identity of the weighted -Laplacian together with the weighted Morrey estimate on smooth Levi-pseudoconvex domains; the last step produces the Hörmander solver and the existence theorem for -closed forms on Hartogs pseudoconvex domains, including the smooth-data branch. The local boundary separator and boundary peak construction are recorded separately, with a positive outer collar, smooth global defining functions and a proved exhaustion-to-Hartogs bridge supplying the correction on a neighborhood of the closure. The host-domain Oka-Weil theorem is used through Boas's approximation theorem.
The second half uses Demailly's Levi theorem and Cartan–Thullen to identify Hartogs pseudoconvex domains, domains of holomorphy, and holomorphically convex domains. The smooth exhaustion supplies the bridge to Demailly's pseudoconvexity criterion. Oka-Weil approximation on a pseudoconvex domain, Dolbeault vanishing, and the first Cousin problem follow from these inputs.
Conventions: is a domain with , weights are real (or ) functions, denotes the weighted Hilbert space of Weighted L2 spaces and maximal dbar operators, and the maximal distributional is the operator of that definition. The Axiom of Choice is declared on every proof-bearing item and is tracked through the suppliers, with the countable instance used by the exhaustion and regularization arguments recorded in the item-level choice notes. No regularity of solutions at the boundary is claimed, and the Demailly (6.9) upper-semicontinuous weight statement is not used.
3 · Logical flowchart
4 · Definitions, theorems and proofs
Smooth strict plurisubharmonic regularization of a psh exhaustion
Statement
Assume the Axiom of Choice (AC) and the Axiom of Countable Choice. Let , , be a domain and let be a continuous plurisubharmonic exhaustion, that is, is continuous and plurisubharmonic and every sublevel set , , is a compact subset of .
Then there exist a function and a strictly increasing sequence with such that, writing :
- is strictly plurisubharmonic on , on , and is again an exhaustion of , that is, is a compact subset of for every real ;
- every is a regular value of , and is a nonempty hypersurface of ;
- and , so every is a compact subset of ;
- (strong pseudoconvexity) for every , every and every with one has .
Facts & Assumptions
Given: The Axiom of Choice and the Axiom of Countable Choice; a domain with ; and a continuous plurisubharmonic exhaustion .
A function is a continuous plurisubharmonic exhaustion when it is continuous, plurisubharmonic, and every sublevel is compact in (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).
(Richberg's approximation theorem.) If is continuous and strictly plurisubharmonic on an open set , with for a continuous positive Hermitian form , then for every continuous there is such that on and ; if is strictly plurisubharmonic on all of , can be chosen strictly plurisubharmonic on all of (Demailly, Complex Analytic and Differential Geometry, Ch. I §5.E, Theorem 5.21, printed pp. 43-44).
For a smooth map from a finite-dimensional manifold to , the regular values are dense; in particular every nonempty open interval contains a regular value when the Axiom of Countable Choice holds (Regular values have null complement and are dense).
A value is regular for if every point of is a regular point; an empty fibre is regular by convention (Regular and critical points and values).
A regular level of a smooth real-valued function on an open subset of is locally a smooth graph of dimension (A regular level set is locally a graph of dimension ).
In ZF, AC implies AC (AC implies DC implies countable choice; The Axiom of Countable Choice ()), and AC states that every family of nonempty sets has a choice function (The Axiom of Choice).
Choice use. AC and AC are the ambient hypotheses. The proof uses AC only to choose a sequence of regular values from nonempty open intervals; each such interval contains regular values by [F3].
Proof
Put and . Then is continuous and plurisubharmonic, and because is plurisubharmonic. It is an exhaustion: if , then , and is closed in ; thus it is a closed subset of the compact set . Moreover everywhere.
Apply [F2] to on with the constant error . This gives satisfying and . Hence is strictly plurisubharmonic, , and is an exhaustion because each sublevel is closed in and contained in the compact sublevel .
Fix . The exhaustion is unbounded above: otherwise for some , making the noncompact open set compact. Choose an integer . For each , [F3] supplies a regular value in the fixed nonempty interval ; AC selects one such for each . Then , , and every level is nonempty: the continuous image is an interval because is connected, it contains , and it is unbounded above.
Set . Each is contained in the compact set , and The sublevels cover because . Continuity gives ; conversely, every point of the regular level is a boundary point by the implicit function theorem. Thus is a nonempty smooth hypersurface, by [F4] and [F5].
At every the function defines near . Since is strictly plurisubharmonic, every nonzero complex tangent vector satisfies . Steps 2.1–4.1 establish the remaining assertions in the Statement. [F1, F2, step 2.1, step 4.1]
Meromorphic functions on an open set in complex Euclidean space
Definition
Fix and read through Complex -space and its real coordinate dictionary. Let be a nonempty open set, and for an open write for the set of holomorphic functions (Holomorphic functions on an open subset of ). Open subsets of carry the subspace topology, and components are those of Connected components, quasicomponents, and totally disconnected spaces.
(a) Meromorphic functions. A meromorphic function on is a function such that
- is open and dense in ;
- is holomorphic on ;
- every point has a neighbourhood and holomorphic functions , with not identically zero on any connected component of , such that
The set is the domain of definition of , briefly its domain. Every determines a meromorphic function on with domain (take and in clause 3). A meromorphic representative with is holomorphic on when it admits a holomorphic extension as in clause (c); removable omissions from are therefore allowed.
(b) Restriction. If is meromorphic on with domain and is open and nonempty, then the restriction is the meromorphic function on with domain and values ; the domain is dense in because is dense in , and clause 3 for restricts to clause 3 for .
(c) Holomorphic on a subset; differences. Let be meromorphic on with domain and let be open. Then is holomorphic on when there is with for every ; such an is called a holomorphic extension of to . For meromorphic on with domains the difference is the function , , and for open the phrase " is holomorphic on " means that admits a holomorphic extension to in this sense.
(d) Sums with holomorphic functions. If is meromorphic on with domain and , then , , is meromorphic on : it is holomorphic on , and wherever on for a local representation of clause 3 one has there, while and are holomorphic on and is not identically zero on any component of (Sums, products and nonvanishing quotients of holomorphic functions are holomorphic).
Remark
Poles. Let be meromorphic on with domain . A point of is a pole of when admits no holomorphic extension to any neighbourhood of the point. The points where does admit a holomorphic extension form an open subset of : each such extension also works near every point in its domain. Hence the pole set is closed. Every pole lies outside , and is closed with empty interior because is open and dense, so the pole set also has empty interior. In particular a meromorphic function is never undefined on a nonempty open subset of its ambient set: its domain meets every nonempty open subset of .
Local nature. Clause 3 is a local condition: if every point of has a neighbourhood to which restricts as a meromorphic function, then is meromorphic on . Concretely a ratio of two holomorphic functions is meromorphic on the open set where the denominator does not vanish identically on a component. This is the standard definition in several complex variables: in several variables only the local ratio is available in general.
Choice. This definition quantifies only over points, neighbourhoods and holomorphic functions; it invokes no choice principle, and none of its clauses selects from a family of nonempty sets.
Weighted L2 spaces and maximal dbar operators
Definition
Assume the Axiom of Choice (AC). Let and let be open, let , and let . Write for the object defined in (a) below, and use the conventions and for and for . In formulas indexed by , write for the canonical coordinate of Complex -space and its real coordinate dictionary, and relabel the corresponding Wirtinger operators and form coefficients in the same way.
(a) Weighted spaces of -forms. A -form coefficient tuple is measurable when every is a measurable function in the sense of (Complex Lp classes and Euclidean test-function conventions); two tuples are identified when they agree almost everywhere. Put and define Here is Lebesgue measure on . The space carries the inner product and is a complex Hilbert space.
(b) The maximal distributional . For choose any representative, which is locally integrable, and let be its distributional derivative, an element of the space of distributions on . The maximal domain is and for the form is that representing element. The operator is the maximal distributional in degree . Its minimal domain contains every smooth form with compact support in .
(c) The weighted adjoint. Let be the maximal operator of degree . Its weighted adjoint is the Hilbert adjoint , using the same bounded-functional definition for operators between the two Hilbert spaces: holds exactly when the functional is continuous on in the ambient norm, and then is the unique with Convention: always denotes the adjoint of the preceding degree, and the formal density expresses as a distribution whenever ; coefficients are extended to non-increasing tuples by antisymmetry, so that when . The Hilbert adjoint is not asserted to equal this formal expression on all of , and no boundary condition on is imposed here.
(d) Density of test forms. The smooth compactly supported -forms, regarded as tuples of their coefficient functions, form a linear subspace that is dense in . The reduction to the unweighted Euclidean density theorem, first for compactly supported tuples and then in general by cutoff along a compact exhaustion of , is carried out in step 1.3 below.
Facts & Assumptions
Given: The Axiom of Choice; an integer ; an open set ; an integer ; and a real function .
A measurable complex function is locally integrable for Lebesgue measure when on every compact (Complex Lp classes and Euclidean test-function conventions).
For every measure space and the complex space is complete (Complex Lp completeness and almost-everywhere subsequences).
On every measure space the pairing on complex is representative-independent, linear in the first variable, conjugate-linear in the second, conjugate symmetric and positive definite, and (The complex pairing is well-defined and satisfies Cauchy–Schwarz); the finite-tuple clause of the same theorem gives the same conclusions for the summed tuple pairing.
The bidegree decomposition of complex forms and the coefficient formula are as recorded in Bigraded complex forms and the Dolbeault operators.
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).
Assuming countable choice, is dense in Euclidean Lebesgue for and (Complex finite-simple and smooth compact-support density for finite p).
An operator is densely defined when its domain is dense and closed when its graph is closed (Densely defined, closed and closable operators, and cores), and the adjoint bounded-functional criterion for a densely defined operator on one Hilbert space reads: a vector lies in the adjoint domain exactly when is bounded on the domain (Adjoint of a densely defined operator).
A complex Hilbert space is a complex inner-product space whose norm is complete (Hilbert space); the pairing of [F3] is the first-variable-linear convention fixed by The complex pairing on equivalence classes.
AC states that every family of nonempty sets has a choice function (The Axiom of Choice); its countable instance gives the countable-choice conventions used by [F2] and [F6] (The Axiom of Countable Choice ()).
For compact inside an open Euclidean set , there is with equal to one near (Test function cutoffs and euclidean localization).
Under countable choice every bounded linear functional on a complex Hilbert space has a unique Riesz vector; the vector depends conjugate-linearly on the functional (Riesz representation for Hilbert spaces).
Under countable choice a locally integrable function representing the zero distribution is zero almost everywhere (Locally integrable functions embed in distributions).
Dominated convergence applies to measurable functions converging almost everywhere with a single integrable majorant (Dominated convergence).
A compactly supported smooth unit-mass bump generates a mollifier family, and convolution with it 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 used only through its countable instance, for the measure-theoretic completeness and density interfaces [F2], [F6], [F11] and [F12], and to select the cutoff sequence in step 1.3. The definitions of the weighted pairing, of the maximal operator and of the Hilbert adjoint select nothing.
Proof
If , all coefficient spaces contain only the zero class and the assertions are immediate. Assume . The weight is continuous and strictly positive on , so is a Borel measure on with the same null sets as Lebesgue measure and with finite mass on every compact subset of the -compact space ; by [F3] the tuple pairing of coefficient tuples satisfies the inner-product axioms and Cauchy-Schwarz, and by [F2] with and the complex space is complete, so the coefficientwise space of (a), a finite product of copies of with the summed pairing, is a complex inner-product space whose norm is complete, that is, a complex Hilbert space in the sense of [F8]; the countable instance of [F9] is exactly the hypothesis consumed by [F2] and [F6], and no other selection is made here.
Let and let be a nonempty compact set; then by Cauchy-Schwarz, and gives , so every coefficient of is locally integrable; by [F1] it therefore has a distributional derivative in each variable, and by [F5] that derivative depends only on the almost-everywhere class of , so it is well defined on and additive and -homogeneous in the coefficient.
Test forms are dense in the weighted space. Let . For integers choose with , near and , where and the distance constraint is omitted when . These sets are compact, exhaust , and satisfy : distance to the nonempty complement is continuous by the triangle inequality, and both defining inequalities become strict at the next index. Apply [F10] with and use countable choice for the cutoffs (take zero when is empty); then and pointwise, so [F13] gives and each has compact support in . It remains to approximate any such compactly supported tuple . If there is nothing to prove; otherwise put and use the already chosen exhaustion cutoff , which equals near and has compact support in . Thus . Let , extend each coefficient of by zero to a tuple on , and apply [F6] componentwise: for every there is a tuple with and for each of the coefficients. The tuple lies in , and because its error is on . Therefore This proves the claimed weighted density.
Define for by the formula of (b) using the locally integrable representative supplied by step 1.2; by [F4] its coefficient in front of , , is , a distribution, and if both represent , then every coefficient of is locally integrable by step 1.2 and represents the zero distribution, so [F12] gives almost everywhere; hence and are well defined.
For the preceding-degree adjoint is zero by convention. For , let and . For every compactly supported smooth -form , the adjoint identity and [F4], with wedge signs absorbed in the antisymmetric coefficients , give The identity [F5], conjugated and summed, therefore gives as distributions. Here a first derivative of a locally integrable function acts continuously on compactly supported tests by its defining integral. To use such a test, extend it by zero and convolve with a smooth unit-mass bump as in [F14]: the approximations and their first derivatives converge uniformly, with supports in a fixed compact subset of . Local integrability then passes each defining integral to the limit. This also justifies the multiplier and its product rule in this order-one identity. Multiplying by and expanding yields exactly (c), only on the Hilbert-adjoint domain.
The domain of is a linear subspace and is linear: by [F5] the distributional identity holds for all scalars and all locally integrable (test against every compactly supported smooth function and use linearity of the integral), and applying the uniqueness part of step 2.1 to the two representations of gives ; the domain is nonempty because every smooth compactly supported -form has its smooth in by [F4].
The operator is densely defined because its domain contains the compactly supported smooth -forms by step 3.1 and these are dense by step 1.3; therefore the bounded-functional criterion in (c) defines its adjoint: each bounded functional extends to the domain Hilbert space and has a unique Riesz vector by [F11], so is unique, and it is linear because and the Riesz correspondence are both conjugate-linear, while the convention for and is the zero operator on ; this completes the well-definedness of the objects named in (a), (b) and (c).
The maximal distributional dbar operator is closed and densely defined
Statement
Assume the Axiom of Choice (AC). Let be open with , let , let , let be the maximal distributional of degree , and let be the Hilbert adjoint of , all with the conventions of Weighted L2 spaces and maximal dbar operators, including its one-based relabeling of the canonical coordinates.
- is dense in , and is closed.
- For and every of bidegree , lies in , and is the compactly supported form with coefficients
- is closed.
Facts & Assumptions
Given: The Axiom of Choice; an open set with ; an integer ; and a real function .
The weighted -space is for the pairing (Weighted L2 spaces and maximal dbar operators).
The maximal domain is , where is the distributional derivative; for the form is that representing element (Weighted L2 spaces and maximal dbar operators).
The weighted adjoint satisfies for all and , its formal density is whenever , and coefficients are extended to non-increasing tuples by antisymmetry, with when (Weighted L2 spaces and maximal dbar operators).
Test forms are dense in the weighted space: every is the -limit of a sequence of forms in (Weighted L2 spaces and maximal dbar operators).
Every coefficient of every is locally integrable for Lebesgue measure on (Weighted L2 spaces and maximal dbar operators).
Every smooth compactly supported -form has its smooth in , hence lies in (Weighted L2 spaces and maximal dbar operators).
A weak derivative is characterized by the test identity for every real test function (Weak derivative of a locally integrable function).
An operator is densely defined when its domain is dense, and closed when its graph is a closed subset of (Densely defined, closed and closable operators, and cores).
A vector lies in the adjoint domain exactly when is bounded on the domain, and then is the unique with for all in the domain (Adjoint of a densely defined operator).
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.
On every measure space the complex pairing satisfies , also for finite tuples (The complex pairing is well-defined and satisfies Cauchy–Schwarz).
In a metric space a set is closed exactly when it is sequentially closed (A point lies in the closure of iff some sequence in converges to it, and a set is closed iff it is sequentially closed).
AC implies the Axiom of Countable Choice (AC implies DC implies countable choice, The Axiom of Countable Choice ()).
AC states that every family of nonempty sets has a choice function (The Axiom of Choice).
The Wirtinger operator is (Wirtinger operators in ).
For a compactly supported smooth unit-mass bump on Euclidean space, is its mollifier family, and convolution of a locally integrable function with 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 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 and the formal expression are given.
Proof
By [F6] every smooth compactly supported -form lies in , and by [F4] these forms are dense in ; hence contains a dense subset and is itself dense in , which is the definition of being densely defined in the sense of [F9]. The density interface [F4] is where the countable instance of [F14] is consumed.
Let and . The unweighted distributional identity of [F2] extends from smooth compactly supported test forms to test forms. Indeed extend a test 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 together with every first derivative uniformly: differentiate under the integral in the expression and use uniform continuity of and its first derivatives. Local integrability of and then passes both sides of the test identity to the limit. For a smooth -form of compact support, use the test coefficients . The coefficient sum in [F2], with its antisymmetric wedge signs, and the product rule give Only as a whole is assumed locally integrable; no individual weak derivative of a coefficient of is assumed to be a function.
The operator is closed. Let with in and in . On every compact , the positive minimum of gives , and the same bound holds for . Cauchy-Schwarz on therefore gives local convergence. Against any ordinary smooth compactly supported test form, both sides of the unweighted distributional identity for pass to the limit, since the test and its first derivatives are bounded. Thus as distributions, so [F2] gives and . (For 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].
Let have bidegree with , and let be the formal expression of [F3]. Then has compact support contained in and coefficients in because and , so ; moreover step 1.1 makes densely defined, and step 1.2 gives for every , so by [F12] the functional is bounded on the domain with norm at most . By the characterization [F10] we therefore have and ; the countable choice used by the adjoint definition is supplied through [F14].
The adjoint is closed even though its source and target Hilbert spaces have different form degrees. Let satisfy in and in . For every the adjoint identity [F3] and continuity of the two inner products give . Thus lies in the adjoint domain and by its definition [F3]. The graph is sequentially closed and hence closed by [F13].
Conclusion: is dense and is closed by steps 1.1 and 1.3; every compactly supported smooth -test form lies in with the formal weighted expression of [F3] by step 2.1; and 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].
Basic Bochner–Kodaira–Morrey estimate on
Statement
Assume the Axiom of Choice (AC). Let be open with . Use one-based labels for , also for their derivatives and form coefficients. Let , write
let , and let be a compactly supported smooth -form on , with coefficients on increasing tuples extended to non-increasing tuples by antisymmetry, so that when (Weighted L2 spaces and maximal dbar operators); the operators are those of Wirtinger operators in . All sums over multi-indices below run over increasing tuples, and are the inner product and norm of , and is the weighted Hilbert adjoint of (Weighted L2 spaces and maximal dbar operators).
- (Exact Bochner–Kodaira–Morrey form.) The following identity holds, all integrals being finite:
- (Levi inequality.) If in addition is plurisubharmonic on , then
Facts & Assumptions
Given: The Axiom of Choice; an open set with ; a function ; an integer ; a compactly supported smooth -form ; and the notation , , acting coefficientwise, where the Wirtinger operators are those fixed in the Statement, so that the holomorphic derivative, and not , appears in ; further on coefficient tensors, and for increasing .
The weighted inner product and norm on coefficient tuples of bidegree are and (Weighted L2 spaces and maximal dbar operators).
The distributional derivative of is (Weighted L2 spaces and maximal dbar operators).
The weighted adjoint is characterized by for all and (Weighted L2 spaces and maximal dbar operators).
Coefficients are extended to non-increasing tuples by antisymmetry, so that when (Weighted L2 spaces and maximal dbar operators).
The conventions and are in force for and for (Weighted L2 spaces and maximal dbar operators).
For every of bidegree lies in , and (The maximal distributional dbar operator is closed and densely defined).
Wedge multiplication of basis vectors is multilinear and alternating, so and transposing two neighbouring entries changes the sign; it is also associative, and the strictly increasing monomials form a basis; hence for a distinct and an increasing tuple one has , while when (The basic wedge map is multilinear and alternating, Exterior multiplication is well defined, graded, associative, unital, and graded-commutative, Wedge monomials in a dual basis form a basis).
The Levi form is (The Levi form and strict plurisubharmonicity).
A real-valued function is plurisubharmonic if and only if its Levi form is pointwise semidefinite nonnegative (The C^2 Levi criterion for plurisubharmonicity).
For a function with continuous second partial derivatives, (Continuous second partials of a scalar potential commute).
On every measure space the complex pairing is linear in the first variable, conjugate-linear in the second, conjugate symmetric and positive definite (The complex pairing is well-defined and satisfies Cauchy–Schwarz).
The Axiom of Countable Choice supplies a choice function for every at most countable family of nonempty sets (The Axiom of Countable Choice ()).
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 DC 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
The notation of the given block is well defined on coefficient tensors, and for increasing the sign rule [F7] gives for and for , while the antisymmetry convention [F4] gives for and for , where ; consequently the Clifford relation holds, because for one has and , for one has and , for with both terms vanish since an index occurring twice wedges to zero, and for with the terms vanish when and otherwise cancel by the sign identity , whose two exponents differ by exactly one because exactly one of , holds.
For coefficient tensors of degree and of degree with compactly supported smooth coefficients, : by [F11] both sides are sesquilinear in , and on constant basis tensors , the formulas above from [F7] and [F4] give and , which are equal since exactly when ; multiplying the pointwise identity by the positive factor and integrating with the pairing of [F1] gives the weighted statement.
For all one has , and hence also by conjugate symmetry; indeed, is a compactly supported smooth -form and a compactly supported smooth -form lying in with by [F6], while [F2] gives , so the characterizing identity [F3] reads .
On compactly supported smooth forms the operator identities and hold pointwise in the increasing coefficients, the first because [F2] expands as the sum of the wedges , and the second because the coefficient formula of [F6] is on each increasing , which is what produces; consequently the self-adjoint-shaped operator satisfies on those forms.
The operator identity holds on compactly supported smooth forms: by the identities of step 1.4, the constant-coefficient form operators commute with the coefficientwise operators , and by the Clifford relation of step 1.1 one has and , so ; the commutator acting coefficientwise is the multiplication operator , since the coefficientwise derivatives commute and only the term where hits survives, and by clairaut [F10].
The left-hand side of claim 1 equals : since and its images are compactly supported smooth forms lying in the relevant domains, with by the degree convention [F5] when , the characterizing adjoint identity [F3] applied to the pairs and gives and , while conjugate symmetry [F11] turns the first expression into because [F1] makes it a real number; adding the two terms and using the definition of from step 1.4 gives the claim.
The two summands of evaluate as by the adjoint identity of step 1.3, and by the adjointness of step 1.2, the scalar commutation of 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.
If is plurisubharmonic, the Levi criterion [F9] applied to the Levi form [F8] gives for every and , and applying this at each point with the given coefficients , for every increasing of size , 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.
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.
A coercive Hilbert-complex estimate solves the closed equation
Statement
Assume the Axiom of Choice (AC). Let be complex Hilbert spaces and let and be closed densely defined linear operators with , so that on . Suppose there is a constant with where is the Hilbert adjoint of . Then for every :
(i) there exists with ; (ii) among all such there is exactly one of least norm, and it lies in ; (iii) that least-norm solution satisfies .
Independently of the constant , the following -weighted form of the argument holds.
(iv) Suppose is a bounded self-adjoint operator with for every , that and that has the form for some . Then there exists with , and the least-norm such satisfies
No closedness of the range of and no surjectivity of is assumed.
Facts & Assumptions
Given: The Axiom of Choice; complex Hilbert spaces ; closed densely defined linear operators and with ; a constant with for every ; and an element . For the independent part (iv) assume in addition a bounded self-adjoint operator with for every and for every , together with an element satisfying .
For the operator , define to be the set of for which is bounded in the norm. Density of , [F5] and [F4] give a unique with for every . The graph identities needed below are proved in step 1.3.
For a linear subspace of a Hilbert space, (The double orthogonal complement of a subspace is its closure).
If is a closed linear subspace of a real or complex Hilbert space , then every has a unique decomposition with and (Orthogonal decomposition by a closed subspace).
For a bounded linear functional on a complex Hilbert space there is a unique representing vector of the same norm (Riesz representation for Hilbert spaces).
A bounded functional on a dense linear subspace extends uniquely by limits to the ambient Hilbert space: boundedness makes values on a convergent approximating sequence Cauchy and makes the limit independent of the sequence. The resulting functional has a Riesz vector by [F4].
An operator is densely defined when its domain is dense, and closed when its graph is a closed subset of (Densely defined, closed and closable operators, and cores).
In a real or complex inner-product space for all vectors (Cauchy–Schwarz: , with equality exactly for dependent pairs).
A complex Hilbert space is a complex inner-product space whose induced norm is complete (Hilbert space).
AC states that every family of nonempty sets has a choice function (The Axiom of Choice), and it supplies its countable instance (The Axiom of Countable Choice ()).
A bounded self-adjoint operator satisfies for all , so in particular (The Hilbert-space adjoint of a bounded operator, Self-adjoint, positive, unitary and normal operators, The spaces (\mathcal B(X,Y)) and (\mathcal B(X)) of bounded linear operators).
Choice use. AC is used only through the countable instance consumed by the operator, decomposition and representation facts [F1], [F2], [F3] and [F4]. The adjoint graph argument, functional extension, minimal-norm projection and the -weighted variant select nothing further.
Proof
Since is closed, its kernel is closed: if and in then lies in the closed graph of , so and ; the same argument shows that is a closed subspace of , and says exactly that the composition is zero on .
Semidefinite Cauchy–Schwarz. For all one has : fix and note that for every real , using [F10] and , ; if the discriminant of this nonnegative quadratic is , so , while if the same quadratic forces and the inequality holds trivially; choosing with and and applying the real-part inequality to the pair , whose quadratic values are unchanged because is linear and , gives the stated modulus bound.
The adjoint defined in [F1] has a linear domain. Directly from its defining identity, : vanishing of for every is equivalent to . More precisely, in one has because is orthogonal to every exactly when for every . Since is closed, [F2] gives .
For decompose with and by [F3] applied to the closed subspace of step 1.1; since , taking orthogonal complements gives by step 1.3, so , hence as well, with ; moreover because .
For every the vector of step 2.1 lies in and , so the hypothesis and step 2.1 give , and [F7] together with step 2.1 gives .
Define on the subspace by ; if then step 3.1 gives , so is well defined, and step 3.1 says for every , so is linear and bounded on ; let and define for and any sequence with : the sequence is Cauchy because , and the limit exists by [F8]; the countable instance of [F9] is the choice principle consumed by [F1], [F3], [F4] and [F8] here, and the construction selects nothing further; it is independent of the sequence because two sequences for the same have difference tending to , and passing to limits of the defining inequalities preserves linearity (limits of sums and scalar multiples) and gives .
-weighted estimate. For every , with as in step 2.1, the vector lies in with and (step 3.1 for the first two, step 2.1 for the third), so by step 1.2 applied to the pair , by [F10], by and by the domination hypothesis for (iv) on : , where and by positivity of .
Let be the orthogonal projection onto the closed subspace , defined for by the unique decomposition with of [F3], and put ; then is linear and for all , so by [F4] there is a unique with for all and .
For every , steps 4.1 and 5.1 give . Therefore is orthogonal to every by step 1.3 (take complex conjugates of the displayed identity). Since is closed, ; hence and , proving (i).
Define on by for and put : step 4.2 with shows is well defined, and it shows for every , so is linear and bounded; the extension of to by limits along sequences in , its independence of the chosen sequence, its linearity and its bound are verified by the same computation as in step 4.1 with in place of , with the Cauchy property supplied by [F8] and the same countable instance of [F9]; letting be the orthogonal projection of [F3] onto as in step 5.1, the functional is linear with on , so [F4] gives a unique with for all and .
By step 1.1 the subspace is closed, so [F3] decomposes the solution of step 6.1 as with and ; then , so is a solution lying in , every solution has the form with , and since the Pythagorean identity gives with equality only for ; thus is the unique least-norm solution and by step 5.1, proving (ii) and (iii).
For every , step 6.2 gives . As in step 6.1, the graph identity of step 1.3 and closedness of yield , so and . This proves existence in (iv).
By step 1.1 the subspace is closed, so [F3] decomposes the solution of step 7.2 as with and ; then and the argument of step 7.1 shows that is the unique least-norm solution, with by step 6.2, hence , which proves (iv); moreover with and the hypotheses of (iv) hold by the coercivity assumption, and its conclusion specializes to , in agreement with (iii).
Weighted Morrey–Kohn estimate with a pseudoconvex boundary term
Statement
Assume the Axiom of Choice (AC). Let , and use for the canonical coordinate , , with the same relabeling for derivatives and form coefficients. Let be a bounded domain with boundary, let be a defining function with and on , let , let , and let satisfy the ∂̄-Neumann boundary condition \sum_{j=1}^n u_{jK}\,\frac{\partial\rho}{\partial z_j}=0\quad\text{on }\partial D,\qquad\text{for every }K\text{ with }|K|=q-1, \tag{BC} where is the antisymmetric coefficient of on the tuple and denotes -dimensional surface measure on . Then:
-
, and the exact identity holds, with and .
-
If is Levi pseudoconvex, the boundary term is nonnegative and therefore
-
If is Levi pseudoconvex and denote the eigenvalues of the Hermitian matrix , then
-
If is Levi pseudoconvex, the inequality of claim 3 holds for every .
Facts & Assumptions
Given: The Axiom of Choice; a bounded domain with boundary; a defining function normalized by on ; a weight ; an integer ; and a form satisfying (BC); the conventions and on coefficient tensors, and acting coefficientwise, and for the unweighted Hilbert adjoint of (the case of the operators of [F1]), whose formal density on its smooth domain is .
The weighted space, its pairing , the maximal distributional , and the weighted Hilbert adjoint with its formal density on its domain are as in Weighted L2 spaces and maximal dbar operators; coefficients are extended to non-increasing tuples by antisymmetry, so when .
For every of bidegree one has (The maximal distributional dbar operator is closed and densely defined).
Wedge multiplication of basis vectors is multilinear and alternating, so and transposing two neighbouring entries changes the sign; it is also associative, and the strictly increasing monomials form a basis; hence for a distinct and an increasing tuple one has , while when (The basic wedge map is multilinear and alternating, Exterior multiplication is well defined, graded, associative, unital, and graded-commutative, Wedge monomials in a dual basis form a basis).
The Levi form is (The Levi form and strict plurisubharmonicity).
A domain with boundary is Levi pseudoconvex when for every there are a neighbourhood of and with , , and for every with (Levi pseudoconvex domains).
For functions with continuous second partial derivatives, (Continuous second partials of a scalar potential commute).
The Wirtinger operators are and (Wirtinger operators in ).
A normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and a self-adjoint endomorphism is normal (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).
On every measure space the complex pairing satisfies , also for finite tuples (The complex pairing is well-defined and satisfies Cauchy–Schwarz).
in ZF, and supplies a choice function for every at most countable family of nonempty sets (The Axiom of Countable Choice (), The Axiom of Choice).
(Boas, §3.3.3, printed pp. 81-84: formulas (3.3)-(3.4), Exercise 38.) For smooth scalar functions on the divergence theorem stated in the given block gives the two weighted integrations by parts and , where , , and ; Boas's (3.3) is the expansion obtained by dropping the boundary term for compactly supported data, his (3.4) is the adjoint boundary condition exhibited by these formulas, and his Exercise 38 is the same computation with a positive smooth weight in place of , which is where the factors come from.
(Haslinger, author manuscript, §4, Proposition 4.12 with Lemmas 4.14-4.16, printed pp. 45-49, and the general-degree boundary criterion (4.31) with its proof on printed p. 48.) On a bounded domain with boundary, is dense in for the unweighted graph norm ; this also holds with . For a form, , membership in is equivalent to (BC), and on this domain its value is . The source proves this in boundary frames where (BC) is vanishing of the complex normal coefficients; thus the dense smooth family satisfies (BC). The source uses the unweighted pairing. Weighted transport is proved here in steps 1.2, 2.1 and 9.1, not attributed to the source.
Given (source computation). For , the divergence theorem gives ; its conjugate gives the formula. Applying these to gives [F11], including for factors. In Boas, §3.3.3, printed p. 83, the unweighted calculation for a smooth -form is The Hilbert-adjoint identity holds precisely when the boundary term vanishes, as justified by [F12]. Boas's Exercise 38 treats a positive smooth weight; the weight here needs only the displayed divergence theorem and product rule.
Choice use. AC is the ambient hypothesis recorded in the Statement and cited as [F10]; the countable instance is the form of choice consumed by the interfaces [F1] (completeness and density of the weighted space) and [F2], and by the countable cutoffs, exhaustions and subsequences occurring in the imported density statement [F12]. The proof selects no family of nonempty sets beyond those countable instances.
Proof
Since is and there, is compact, so and the coefficients are bounded on ; put . The Hermitian matrix is well defined at every , its eigenvalues are real by [F8], and if is a unit eigenvector for then the Cauchy-Schwarz inequality gives , so the sum satisfies at every point of ; also because is real-valued.
Transport identity. A -form lies in exactly when lies in , and then Indeed and for every in the maximal domain. The weighted and unweighted graph domains of agree as sets, since are bounded on ; hence the two bounded-functional criteria are equivalent and their Riesz vectors have the displayed relation.
The form lies in and : the positive factor preserves (BC), so [F12], applied with since is , gives and The transport identity of step 1.2 gives the claimed weighted adjoint and formula.
On smooth coefficient tensors the following operator identities hold: (a) and on ; (b) ; (c) ; (d) ; (e) ; and (f) for coefficient tensors of adjacent degrees. Here (a) is the definition of the wedge and for smooth forms the formal density of [F1] established in step 2.1; (b) is the sign case check of [F3] against the antisymmetry convention of [F1]; (c) is ; (d) is by [F6]; (e) follows from (a)-(d) by writing and substituting (b), (c) and (d); and (f) is the pointwise adjointness of wedge and contraction.
For every and every coefficient tensor one has : the Hermitian matrix is self-adjoint and hence normal, so [F8] gives an orthonormal basis of with and ; putting and gives ; Parseval in each fiber gives , and because where is the adjoint, by (f) of step 3.1, of and by (b) and (f) of step 3.1, using ; finally, for real and reals with one has , because an exchange of mass between indices and never increases and repeated exchange reaches , .
The left-hand side of claim 1 equals , where and , with the coefficient of the -form on the ordered tuple : by step 2.1 and identity (e) of step 3.1, computed as formal densities, the integration by parts for in [F11] with , gives using the formal integration-by-parts expression (no Hilbert-adjoint domain claim is made for ), and by (f) of step 3.1, while by the adjoint relation applied to the form , whose first derivatives are bounded and hence whose is in , and the form ; adding gives the claim.
The first summand is , where . Indeed apply the integration by parts of [F11] with and . Since , the weight-derivative terms cancel and the remaining volume term is ; the boundary term has the sign .
The second summand of evaluates as : apply the adjointness (f) of step 3.1 pointwise, move the scalar outside the pairing, and use the coefficient formula of [F1].
At every boundary point one has the identity , all quantities being evaluated at , where denotes the coefficient of on the ordered tuple (so it equals when ) and the coefficient of on the increasing tuple ; moreover . Indeed, with the left-hand side equals by (f) and (a) of step 3.1, and since by (b), (c) and [F6] (applied to ), it equals ; the second term is by (f) of step 3.1, and the first term vanishes because and for each the tangential operator annihilates the restriction to of : it is tangential at because by (BC), and on by (BC), so ; integrating the pointwise identity over against and subtracting the definition of in step 4.3 from that of in step 4.2 gives the displayed identity for .
Claim 1 holds: by steps 4.2, 4.3 and 4.4 the sum equals , and step 5.1 replaces by , which is the stated identity; the membership is step 2.1.
If is Levi pseudoconvex the boundary term of claim 1 is nonnegative: at and for each with the vector satisfies by (BC), so by [F5]: if is its local defining function at , local coordinates transverse to give with ; the product rule on vectors tangent to gives , and the boundary integral of claim 1 is an integral of a pointwise nonnegative continuous function against the positive factor ; dropping it and the nonnegative first term of the identity of step 6.1 gives the estimate of claim 2.
Claim 3 holds: by step 4.1 the integrand dominates pointwise on , and step 7.1 bounds the integral of the former by .
Claim 4 holds. Let and put . By the transport identity of step 1.2, ; the product rule gives , so . The unweighted graph-norm density [F12] gives smooth satisfying (BC) with , , and in unweighted . Put . Then satisfies (BC) and belongs to , which suffices for the integrations by parts and boundary differentiations of steps 2.1–8.1. By step 1.2 and the product rule, The bounded factors and show that in the weighted graph norm. Apply the inequality of step 8.1 to and pass to the limit: the right side converges by graph-norm convergence, and the left side converges because by step 1.1 and convergence implies convergence of the squared norms against any bounded real weight. Thus the inequality holds for .
Claims 1, 2, 3 and 4 of the Statement are proved: claim 1 is step 6.1, claim 2 is step 7.1, claim 3 is step 8.1 and claim 4 is step 9.1; the ambient hypothesis is the AC recorded in the Statement and cited as [F10], its countable instance is consumed by [F1], [F2] and [F12] as described in the choice-use paragraph of the given block, and the two imported inputs from outside the library are the integration-by-parts computation [F11] of Boas and the unweighted boundary-criterion and graph-norm density statements [F12] of Haslinger, used in steps 2.1, 9.1 (with the weighted reduction carried out in steps 1.2 and 9.1).
Weighted ∂̄ solvability on a smoothly bounded pseudoconvex domain
Statement
Assume the Axiom of Choice (AC). Let and use one-based labels for and the corresponding derivatives. Let be a bounded Levi pseudoconvex domain with boundary (Levi pseudoconvex domains), let be strictly plurisubharmonic at every point of (The Levi form and strict plurisubharmonicity), and let . Write and let denote the maximal distributional of Weighted L2 spaces and maximal dbar operators, with its weighted adjoint. For let be the eigenvalues of the Hermitian matrix and put , so that on . Then for every with there exists with , and the least-norm such solution , which lies in , satisfies
Facts & Assumptions
Given: The Axiom of Choice; an integer ; a bounded Levi pseudoconvex domain with boundary; a weight strictly plurisubharmonic at every point of ; an integer ; the eigenvalues of the Hermitian matrices and the function on ; and a form with .
With the conventions of Weighted L2 spaces and maximal dbar operators, the space carries the inner product and is a complex Hilbert space, and is the maximal distributional in degree (clauses (a) and (b) of that definition).
is dense in , and is closed (The maximal distributional dbar operator is closed and densely defined).
Distributional derivatives satisfy (Distributional differentiation is continuous and commutes).
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).
For , is strictly plurisubharmonic when for every and every (The Levi form and strict plurisubharmonicity).
Weighted Morrey estimate (Weighted Morrey–Kohn estimate with a pseudoconvex boundary term): if is Levi pseudoconvex and are the eigenvalues of , then and the inequality holds for every .
The -weighted form of the abstract Hilbert-complex solver (A coercive Hilbert-complex estimate solves the closed equation): if is bounded self-adjoint with on and and if has the form for some , then there exists with , and the least-norm such satisfies .
A finite-dimensional complex inner product space has an orthonormal basis of eigenvectors of every normal endomorphism, and a self-adjoint endomorphism is normal with (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).
AC states that every family of nonempty sets has a choice function (The Axiom of Choice), and it supplies its countable instance (The Axiom of Countable Choice ()).
For a function of class on an open subset of the mixed partial derivatives commute, (Continuous second partials of a scalar potential commute).
With the conventions of Weighted L2 spaces and maximal dbar operators (c), the weighted adjoint is the Hilbert adjoint of , and holds exactly when the functional is continuous on in the ambient norm.
Finite orthonormal lists satisfy the Bessel inequality, with Parseval equality for an orthonormal basis (Bessel's inequality for a finite orthonormal list and Parseval's identity for an orthonormal basis).
Choice use. AC is the ambient hypothesis recorded in the Statement and cited as [F9]; the countable instance is consumed by the closedness and density facts [F2] and by the extension step inside claim (iv) of [F7]. The proof itself selects nothing beyond those countable instances: the eigenvalue functions are determined by , the multiplier is determined by , and is determined by and .
Proof
, i.e. on : for the form has coefficients which represent the coefficient distributions of [F1] on the tuples with , each of the form with the shuffle signs of the exterior algebra; applying to therefore gives, on each increasing tuple with , a coefficient distribution in which the term belonging to the ordered pair and the term belonging to carry the shuffle signs of and , hence opposite signs; since distributional derivatives commute, as distributions by [F3], the two terms cancel and every coefficient distribution of vanishes; the zero distribution is represented by the zero form, so with , as required.
Write and . Reality of and [F10] give , so both and are Hermitian. They have the same characteristic polynomial, since , and therefore the same ordered eigenvalues . With the first-variable-linear inner product, the correct identity is Thus is positive definite by [F5], and [F8] gives . For every unit vector, Taking minima on the unit sphere shows that is continuous. Also is the minimum of over orthonormal -frames. Indeed expansion in an eigenbasis gives , where and by [F12]; subtracting and bounding each term by for , or for , gives a nonnegative difference. The first eigenvectors attain equality. The preceding uniform bound on unit-vector quotients now gives , so is continuous. On compact , put and . The same unit-vector bound gives .
Define coefficientwise by for ; since is real-valued, measurable and bounded with by step 1.3, is a bounded linear operator on with , self-adjoint because for , and nonnegative because .
For every one has : here and by [F1] and [F11], and is Levi pseudoconvex as assumed ([F4]), so the weighted Morrey estimate [F6], whose two clauses are the inequality and its extension to the maximal domains, applies to and gives .
Put , that is, the -form with coefficients for ; since by step 1.3, the estimate shows , and by step 2.1, ; moreover .
Claim (iv) of [F7] applies with the Hilbert spaces and the operators of step 1.1, the bounded self-adjoint nonnegative multiplier of step 2.1, the datum (which is the hypothesis of the theorem) and the element of step 3.2: the closedness, density and composition requirements are steps 1.1 and 1.2, the domination hypothesis is step 3.1 and the range form is step 3.2, so [F7] yields a solution with whose least-norm representative satisfies .
Unwinding step 4.1: with and , and by steps 3.2 and 4.1, , so is a solution of obeying the stated weighted bound and is the least-norm one; the ambient AC and its countable instance are used exactly as recorded in the choice-use paragraph, through [F2] and through claim (iv) of [F7].
Smooth strictly plurisubharmonic exhaustion of a pseudoconvex domain
Statement
Assume the Axiom of Choice (AC). Let be a domain, , that is Hartogs pseudoconvex (Plurisubharmonic exhaustions and Hartogs pseudoconvexity). Then there exist a function that is strictly plurisubharmonic on (The Levi form and strict plurisubharmonicity) and a strictly increasing sequence with such that, writing :
- every is a regular value of , each is a nonempty hypersurface of , and with , so every is a compact subset of ;
- each sublevel is strongly pseudoconvex along its boundary: for every , every and every with one has .
Facts & Assumptions
Given: The Axiom of Choice; a domain with that is Hartogs pseudoconvex.
A function is a continuous plurisubharmonic exhaustion when is continuous, plurisubharmonic, and every sublevel set is compact in for every real number (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).
The domain is Hartogs pseudoconvex when is plurisubharmonic on , and the whole space is Hartogs pseudoconvex by the empty-complement convention (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).
If a domain is Hartogs pseudoconvex, then it admits a continuous plurisubharmonic exhaustion function (Hartogs pseudoconvexity yields a continuous plurisubharmonic exhaustion).
Assume AC and AC; for every continuous plurisubharmonic exhaustion on a domain there are strictly plurisubharmonic and a strictly increasing sequence such that each is a regular value of , each with is a nonempty hypersurface, and , and for all and all with (Smooth strict plurisubharmonic regularization of a psh exhaustion).
The Axiom of Countable Choice selects from every at most countable family of nonempty sets (The Axiom of Countable Choice ()).
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 [F7]; the regularization lemma [F4] is stated under AC and AC, and the countable instance [F6] is obtained from the ambient AC by the exact implication [F5] in step 2.1. The proof selects no family of nonempty sets.
Proof
By the defining property [F2] the Hartogs pseudoconvexity of says that is plurisubharmonic on , so the equivalence theorem [F3] supplies a continuous plurisubharmonic exhaustion , that is, is continuous, plurisubharmonic, and every sublevel set is compact in by [F1].
The regularization lemma [F4], whose hypotheses are assumed AC together with AC here, applies to the continuous plurisubharmonic exhaustion produced in step 1.1 and yields strictly plurisubharmonic together with a strictly increasing sequence such that each is a regular value of , each is a nonempty hypersurface of , and , and whenever and satisfies ; the countable instance required by that lemma is supplied from the ambient AC by the implication [F5] and its content [F6].
The function and the sequence produced in step 2.1 have exactly the properties listed as claims 1 and 2 of the Statement: strictly plurisubharmonic and smooth on , increasing regular values tending to infinity, sublevels with nonempty smooth boundary, increasing relatively compact closures exhausting , and strong pseudoconvexity along each boundary. The ambient hypothesis is the AC cited as [F7].
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].
Positive-degree Dolbeault vanishing on pseudoconvex domains
Statement
Assume the Axiom of Choice (AC). Let , let be a domain, and suppose that is Hartogs pseudoconvex (Plurisubharmonic exhaustions and Hartogs pseudoconvexity). Let .
-
(Smooth vanishing.) Every smooth -closed -form (Bigraded complex forms and the Dolbeault operators) is exact in the Dolbeault complex: there is with . Consequently (Dolbeault cohomology of a domain).
-
(Weighted exactness under finite energy.) Let be strictly plurisubharmonic on (The Levi form and strict plurisubharmonicity); for let be the eigenvalues of the Hermitian matrix and put . If satisfies and then there is with and .
No boundary regularity of the primitives is claimed, and the statement is asserted for only.
Facts & Assumptions
Given: The Axiom of Choice; an integer ; a Hartogs pseudoconvex domain ; an integer ; a smooth -closed -form ; and a triple consisting of a strictly plurisubharmonic , its eigenvalue functions and , and a form with and .
A domain is Hartogs pseudoconvex when is plurisubharmonic on , where is the equal-radius polydisc boundary function (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).
If is Hartogs pseudoconvex, 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 , so every is a compact subset of (Smooth strictly plurisubharmonic exhaustion of a pseudoconvex domain).
For the Levi form is , and is strictly plurisubharmonic when for every and every ; a strictly plurisubharmonic function is plurisubharmonic (The Levi form and strict plurisubharmonicity).
A function on an open set is plurisubharmonic if and only if for every and every (The C^2 Levi criterion for plurisubharmonicity).
If is plurisubharmonic and is convex and nondecreasing, then is plurisubharmonic on (Basic stability operations for plurisubharmonic functions).
With the smooth complex-valued forms of bidegree on open , , and (Dolbeault cohomology of a domain).
Hörmander's weighted existence theorem (Hörmander's weighted L2 existence theorem for the dbar equation): under AC, with Hartogs pseudoconvex, strictly plurisubharmonic, , eigenvalues and : (claim 1) every with and finite energy has a solution with and ; (claim 2) if in addition and is -closed with , then there is with and .
With the conventions of Weighted L2 spaces and maximal dbar operators: is the space of coefficient tuples with the inner product , and consists of those for which the distributional is represented by an element of , which is then .
The standard smooth step function is with the standard flat function; it satisfies , for and for , and takes values in (The standard smooth step function).
The standard flat function for and for satisfies and for (The standard flat function, The standard flat function is smooth and flat at zero).
Every continuous function on an order-convex interval with at least two elements has a primitive on ; the function is one, and for in and any primitive , (Every continuous function on an interval has a primitive; two primitives differ by a constant; and for any primitive ).
For and integrable and arbitrary one has (For : is integrable on if and only if it is integrable on and on , and then ; with the oriented form for arbitrary ).
For a bounded the Darboux sums over a partition are the lower and upper sums , and is integrable with defined through these sums (For bounded on and a partition : the infimum and supremum of on the -th subinterval, and the lower and upper Darboux sums and , The lower and upper Darboux integrals of a bounded on as and , Darboux integrability as their equality, and the notation ).
For a nonempty the following are equivalent: is compact; is closed and bounded; every continuous attains a maximum and a minimum on (For a nonempty subset of with , compactness, closedness and boundedness, pseudocompactness, and attainment of extrema by every continuous real-valued function are equivalent).
Under the identification of with , the metric of , its balls, its open sets, its convergent sequences, its Cauchy sequences and its continuous maps are verbatim those of (Complex -space and its real coordinate dictionary).
Under the Axiom of Countable Choice, every bounded subset has finite outer measure, a bounded Lebesgue measurable set has finite measure, and every compact subset of is Lebesgue measurable of finite measure (Lebesgue measure is sigma-finite, and every metrically bounded subset of has finite outer measure).
Under the Axiom of Countable Choice, every continuous map is Borel measurable (Continuous functions on Euclidean spaces are Borel measurable).
If are measurable and : implies , and for (Monotonicity and nonnegative homogeneity of the nonnegative integral).
For a nonnegative simple measurable function with pairwise disjoint measurable and , the simple integral is (The integral of a nonnegative simple function).
For nonnegative measurable functions with one has (Beppo Levi's theorem for nonnegative series).
If a real sequence has no vanishing term and , then converges (Ratio test: gives absolute convergence and hence convergence, and gives divergence).
The exponential function is strictly increasing (The exponential function is strictly increasing).
A finite-dimensional complex inner product space has an orthonormal basis of eigenvectors of every normal endomorphism, and an endomorphism is self-adjoint exactly when its matrix in an orthonormal basis is Hermitian, self-adjoint endomorphisms being normal (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); the eigenvalues of a self-adjoint endomorphism are real, since from , , one gets with .
The determinant of a matrix is the product of its eigenvalues, counted with algebraic multiplicity (If in , then : determinant is the product of the eigenvalues counted with algebraic multiplicity).
The trace of a matrix is the sum of its eigenvalues, counted with algebraic multiplicity (If in , then : trace is the sum of the eigenvalues counted with algebraic multiplicity).
A twice differentiable on an open interval is convex if and only if for every (A twice-differentiable function on an open interval is convex if and only if its second derivative is nonnegative).
Finite componentwise sums and products of Euclidean maps are , and a composite of composable Euclidean maps is ( Euclidean maps are closed under componentwise algebra and composition).
A continuous map of smooth manifolds is smooth if and only if its restrictions to the members of an open cover are smooth (Smoothness is local on the source).
If and are totally differentiable at and , then is totally differentiable at with (The chain rule for total derivatives: ).
For functions with continuous second partial derivatives the mixed second partials commute (Continuous second partials of a scalar potential commute).
AC is the assertion that every family of nonempty sets has a choice function (The Axiom of Choice); AC selects from every at most countable family of nonempty sets (The Axiom of Countable Choice ()); and in ZF, AC implies AC (AC implies DC implies countable choice).
Choice use. AC is the ambient hypothesis recorded in the Statement and cited as [F32]; the countable instance AC is consumed through the measure-theoretic suppliers [F17] and [F18] and is obtained from the ambient AC by the implication [F32]. The Hörmander theorem [F7] is applied under its own AC hypothesis, which is the Given. Apart from these interfaces no family of nonempty sets is selected: the shells , the numbers , the sequence , the coefficients and the function are all defined by explicit formulas.
Proof
By [F2] and the definition [F1] of Hartogs pseudoconvexity there are strictly plurisubharmonic and regular values such that, with , every is a nonempty hypersurface of , and , so every is a compact subset of ; by the dictionary [F16] the extreme-value criterion [F15] applies to the nonempty compact set and the continuous function , so is attained and finite; if then would give , so , while because is nonempty with there; hence on .
For put ; since is real-valued with commuting mixed second partials [F31], is Hermitian, hence self-adjoint, so by [F24] it has an orthonormal eigenbasis with real eigenvalues , and expansion in that basis gives ; strict plurisubharmonicity makes [F3], so and by [F25] and [F26], and since for every , one has ; the functions and are continuous on because the entries are, so is a continuous positive function on with for all .
Let be the standard smooth step function [F10]; its defining formula is with the standard flat function, and the flat function vanishes on and is positive on [F11], so with on all of , on and on .
Claim 2 is the instance of [F7] claim 1 with the given strictly plurisubharmonic , the given with and : it yields with and , which is exactly the assertion of claim 2.
Put . Then , on , the complex Hessian of equals that of , and adding the constant changes neither the Levi form nor strict plurisubharmonicity [F3], so is strictly plurisubharmonic; every sublevel set is closed in and contained in for every with , hence is compactly contained in by [F2].
Define for . By [F12] the function is a primitive of the continuous function on , hence is differentiable with ; since (step 1.3), as well.
For every integer put . Each is a Borel subset of , being the preimage under the continuous of a Borel subset of [F18]; the are pairwise disjoint and because on by step 2.1, so the indicator functions sum pointwise to .
One has and on because vanishes there (step 1.3); on because : for every partition of all lower and upper Darboux sums of are those of the zero function, so the integral is by the definition of the Darboux integral [F13, F14]; and for additivity over subintervals gives , the last equality because is a primitive of the constant function and by the evaluation clause of [F12], while the first summand is .
The function is continuous and nonnegative on by step 1.2, and for every one has for a finite number : if take ; otherwise is a nonempty compact subset of by step 2.1, so by [F16] and [F15] the continuous function attains on it a finite maximum , while because is bounded and Lebesgue measurable [F15, F17]; then and with one gets by monotonicity of the nonnegative integral [F19] and the simple-integral formula [F20].
Define . Then is a primitive of the continuous [F12], so with and by step 2.2; on since vanishes there, and on by monotonicity of the integral and (step 3.2); finally , using for (step 3.2), additivity and monotonicity of the integral [F13, F14], and the primitive evaluation [F12].
With the numbers of step 4.1 define for , , for , and for . At each only the finitely many indices with contribute a nonzero term because for (step 4.2), so near the function agrees with a finite sum of functions and is by the algebra and locality properties of smooth maps [F28, F29]; differentiating that finite sum termwise by the chain rule [F30] gives and .
By step 5.1 and steps 1.3, 3.2, 4.2 the coefficients are nonnegative and , , so and for every ; ; and since is a primitive of the continuous , the evaluation clause of [F12] gives for , so is strictly increasing, and for ; moreover for one has by step 4.2 and the definition of , while and because ; hence for every integer .
Let and put on . On one has and by step 6.1, so is convex by [F27] and nondecreasing because for by [F12] and ; the function is real-valued with for by step 2.1, hence everywhere on the real vector space , and the Levi criterion [F4] makes plurisubharmonic on ; therefore the composition is plurisubharmonic on by [F5].
Put . Then by the chain rule and the algebra of smooth maps [F28, F30], and for every and the Levi form is additive, : the middle inequality holds because is plurisubharmonic, so by the Levi criterion [F4], while for by step 2.1 and [F3]; hence is strictly plurisubharmonic on and .
Let and let be the sum of its smallest eigenvalues. By steps 8.1 and 1.2 and the Rayleigh characterization recorded in step 1.2, , the last equality because and have the same complex Hessian (step 2.1) and the last inequality by step 1.2; hence on .
The function is continuous, hence Borel measurable, on [F18]; since the partition (step 3.1), Beppo Levi's theorem [F21] gives ; on one has , hence because is strictly increasing (step 6.1), and (step 4.1), so the scalar rule and monotonicity [F19] give , the middle inequality because (steps 5.1 and 6.1); the series converges by the ratio test [F22] since by strict increase of the exponential [F23]; therefore the energy of with respect to satisfies by step 9.1.
Since is a smooth -closed -form and is strictly plurisubharmonic with (steps 8.1 and 10.1), the branch of the Hörmander theorem [F7] (claim 2) supplies with ; thus , its class in is zero by [F6], and since was an arbitrary smooth -closed -form one has .
Claim 1 of the statement is proved by steps 10.1 and 11.1, and claim 2 by step 1.4; both are stated under the ambient Axiom of Choice recorded in the Given and cited as [F32], consumed in this proof only through the AC instances of the measure-theoretic suppliers [F17] and [F18] and through the AC hypothesis of [F7], and the weight produced in step 8.1 is smooth and strictly plurisubharmonic with no boundary regularity claimed.
A strictly pseudoconvex boundary point has a local holomorphic separator
Statement
Assume the Axiom of Choice (AC). Let , , be a domain and let be a boundary point such that is of class near and strongly pseudoconvex at . In this item, denotes the canonical coordinate for , with the same relabeling for derivatives and form coefficients. There are a neighbourhood of and a function with and
Then there are a neighbourhood of and a holomorphic function such that
In particular has no zero on . Moreover the separator is quantitative in suitable coordinates: there are a holomorphic chart centred at , a radius and a constant such that in this chart and at every point of corresponding to .
Facts & Assumptions
Given: The Axiom of Choice; a domain ; a boundary point with boundary near ; a defining function on a neighbourhood of with , , and for every nonzero complex tangent vector at .
For open set and , as above, the Levi form is and is strictly plurisubharmonic when for all and all (The Levi form and strict plurisubharmonicity).
With a defining function of a domain on a neighbourhood of a boundary point , the complex tangent vectors at are those with , and the Levi form is evaluated on that subspace (Levi pseudoconvex domains).
Two defining functions near the same boundary point have Levi forms on complex tangent vectors differing by a positive scalar factor; in particular the strict positivity demanded at does not depend on the choice of (Levi pseudoconvexity does not depend on the defining function).
For a scalar field near , (Second-order Taylor expansion ).
The Wirtinger operators in several variables satisfy for real totally differentiable , and real-valued is recovered from its Wirtinger partials by this identity (Wirtinger operators in ).
AC states that every family of nonempty sets has a choice function (The Axiom of Choice).
Choice use. AC is the ambient hypothesis stated in the lemma. The normalization, the multiplication by the positive function , the choice of the polynomial and the final pullback are all explicit formulas, so neither [F6] nor any weaker selection principle is consumed by the construction itself; the cited suppliers are used as stated.
Proof
With and as given, the only rephrasing needed is the description of the complex tangent space: by [F2] the complex tangent vectors at form the kernel of the -linear form , and because (if all Wirtinger partials of vanished at , then by [F5]); relabel the indices so that , so that has complex dimension and the hypothesis of the statement says that for every . The Axiom of Choice [F6] is the ambient hypothesis of the statement, and this step selects nothing.
Expansion of at in complex notation: applying the second-order Taylor expansion [F4] to the function and rewriting its linear and quadratic terms with the differential identity of [F5] (for the linear term , because is real; for the quadratic term, substituting the real coordinates and into the real Hessian form and collecting the , , terms), one obtains with , and the expansion as .
First normalization: define the holomorphic affine map by for and with , so that and the Jacobian of is triangular with diagonal entries and ; shrinking makes a biholomorphism onto a neighbourhood of , and is a defining function of near with expansion from step 2.1, where and . The hypothesis survives: equals for the linear part of , and for with the chain rule gives together with by step 1.1.
Multiplication by a positive function: for put and , a defining function of the same domain near with and . Writing and and using the identity , multiplication of the expansion of step 3.1 by gives , the terms of having been absorbed into ; thus the holomorphic quadratic part of is and its Hermitian quadratic part is the Hermitian form in the variable .
is positive definite for all large : the hypothesis of step 1.1 says for with , so on the hyperplane there is with , while the Hermitian form satisfies for with a constant independent of . Decomposing with and gives , and because . Choosing with therefore gives for all , where and ; fix such a and write and for and .
Killing the holomorphic quadratic part: let and define the holomorphic polynomial map , which fixes the first coordinates and sends to ; since it is a local biholomorphism fixing , and with one computes for that and , hence , while because is quadratic; therefore , and is a defining function near of the image of under the change of coordinates.
Conclusion: since , after shrinking the ball to a radius on which is biholomorphic and , every with , and satisfies ; define and where is the inverse chart, so that is holomorphic on , , and on because those points correspond exactly to the parameters , , , and the displayed inequality is the quantitative bound in the chart with the constant of step 5.1.
Positive smooth collars for strictly plurisubharmonic negative sets
Statement
Assume the Axiom of Choice. Let , , be bounded and open, with nonempty boundary. Suppose is open, , in , and is strictly plurisubharmonic near . No nonvanishing-gradient condition is imposed.
For every open with , there are finitely many pairwise disjoint bounded domains such that each has strongly pseudoconvex boundary, and each admits a continuous plurisubharmonic exhaustion.
Facts & Assumptions
Given: AC; the data of the Statement; and the prescribed neighborhood .
A fixed smooth Euclidean bump is nonnegative, equals on the closed unit ball and has support in the radius-two ball (Explicit compactly supported smooth cutoffs).
Uniform convergence of continuously differentiable functions and their derivatives on a closed interval permits termwise differentiation of the limit (If continuously differentiable functions converge at one point and their derivatives converge uniformly on a closed interval, then the functions converge uniformly to a differentiable function whose derivative is the derivative limit).
Smooth real-valued maps have dense regular values; a regular level is locally a smooth graph (Regular values have null complement and are dense, A regular level set is locally a graph of dimension ).
For smooth functions the nonnegative Levi form characterizes plurisubharmonicity; strict positivity is the positive-definite Levi form condition (The C^2 Levi criterion for plurisubharmonicity, The Levi form and strict plurisubharmonicity).
Nonnegative sums, finite maxima and convex nondecreasing composition preserve plurisubharmonicity (Basic stability operations for plurisubharmonic functions). An exhaustion has compact sublevel sets in its domain (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).
Choice use. AC supplies the choice hypotheses of [F3]. The bump sequence, its coefficients and their sum below are explicit after fixing an enumeration of rational balls; the remaining selections are finite.
Proof
Put . Enumerate all rational centers and positive rational radii for which . Their inner balls cover : openness of the complement supplies a sufficiently small ball, then a rational center and radius. Set , Each is finite since the derivatives have compact support. For every fixed multi-index , the tail with is bounded termwise by , so the series of derivatives converges uniformly. Apply [F2] on coordinate segments in closed boxes, successively to every derivative: the limit is with . Every derivative vanishes on , while at any point outside some is ; hence and . This argument proves smoothness across , without assuming local finiteness of the bumps there.
Choose a compact neighborhood of contained in the strict Levi collar of and in . Compactness of this neighborhood times the unit sphere gives a uniform positive lower Levi bound for and a finite upper absolute Levi bound for . Thus for some , is strictly plurisubharmonic on an open neighborhood of . On it agrees with , so it is negative on and zero on ; on both and , so . In particular and the zero set of in is exactly .
Choose a bounded open with and . Then is compact and disjoint from , so . On the compact set the function is positive whenever that set is nonempty. On the compact subset where also has a positive minimum if nonempty, since its zero set would lie in . Choose a positive regular value smaller than all these positive minima, using [F3]. Then contains , has , and its boundary lies in . Regular-level charts show that is smooth and that the inside half of each such chart is connected. Consequently every connected component of has smooth boundary locally defined by , with strictly positive tangential Levi form by step 2.1.
Components of the open set are open and cover the compact set , so finitely many distinct components cover . Their union satisfies the required compact containment. In each choose an open neighborhood of with . Put on . It is smooth and plurisubharmonic near by [F5], and tends to there. The set is a compact subset of , so choose greater than its maximum of . The function is continuous and plurisubharmonic: near the boundary both terms in the maximum are psh; near every point outside the maximum is the constant ; these descriptions agree on their overlap. Its sublevels are closed in and stay away from the boundary, hence are compact in the bounded . Thus it is an exhaustion.
The domains constructed in steps 3.1–4.1 have all the properties in the Statement, including when the original boundary has critical points or the original has zeros outside .
Smooth global defining functions for strongly pseudoconvex boundaries
Statement
Assume the Axiom of Choice. Let , , be a bounded domain with boundary, strongly pseudoconvex at every boundary point. Then there are a neighborhood of and with in , on , and strictly plurisubharmonic near .
Facts & Assumptions
Given: AC; and its local smooth strongly pseudoconvex boundary data.
A local defining function is smooth, defines the negative side , has nonzero differential on the boundary, and has positive Levi form on every nonzero complex tangent vector (Levi pseudoconvex domains).
For compact in an open Euclidean set there is a smooth cutoff in , equal to near and compactly supported in (Test function cutoffs and euclidean localization).
Strict plurisubharmonicity is positive definiteness of the Levi form (The Levi form and strict plurisubharmonicity).
Choice use. AC licenses the stated ambient hypotheses; the compact-boundary cover and cutoffs use finitely many selections.
Proof
Compactness of supplies finitely many local defining charts and smaller relatively compact neighborhoods covering . Shrink them so each local differential stays nonzero on the boundary in its chart and each tangential Levi form stays positive there. By [F2] take nonnegative smooth bumps supported in the charts and equal to on the smaller neighborhoods. On a neighborhood of where , put and , extending each supported product by zero outside its chart. This is smooth and has the same negative, zero and positive sides as the local defining functions. At a boundary point, all active differentials are positive multiples of one outward conormal: they annihilate the common real tangent hyperplane and evaluate positively on an outward vector. Thus .
If is complex tangent at a boundary point, then for all active charts and . The product rule therefore gives Terms involving derivatives of the weights vanish because they contain either or a tangential first derivative of . By [F2] choose equal to near . Define on and on , and define off , with on the boundary. Here is extended by zero off , and is zero near the boundary. Hence is globally smooth, negative exactly on , positive outside , and agrees with near the boundary.
On the compact boundary put . Its norm has a positive lower bound , and the operator norm of the Levi matrix of has a finite bound . For the tangential Levi form has a uniform positive bound . Write any with and . Then and Choose with . For the tangent space is zero and one instead chooses . In either case for every nonzero on the boundary.
Set . The chain rule gives Step 3.1 and compactness give strict positivity on a neighborhood of . The function is because the constructed is ; its negative set is exactly and on the boundary. Restricting to any neighborhood of gives the Statement.
A smooth psh exhaustion gives Hartogs pseudoconvexity on bounded domains
Statement
Assume the Axiom of Choice. Let , , be a bounded domain with a smooth plurisubharmonic exhaustion . Then is Hartogs pseudoconvex: is plurisubharmonic, where is the equal-radius polydisc boundary function.
Facts & Assumptions
Given: AC; the bounded domain ; and plurisubharmonic, with compact sublevels in .
Holomorphic pullback preserves plurisubharmonicity for a psh function (Holomorphic pullbacks of plurisubharmonic functions are plurisubharmonic). Psh is subharmonicity on affine complex lines (Plurisubharmonic functions).
An upper semicontinuous, finite function on a plane domain is subharmonic if it satisfies harmonic comparison on every compactly contained closed disc (Subharmonicity is equivalent to harmonic comparison on compactly contained discs).
On a disc a harmonic function is the real part of a holomorphic function, since a disc is homologically simply connected (Harmonic conjugates exist on homologically simply connected plane domains).
A subharmonic function attaining a finite interior maximum is constant (A plane subharmonic function with an interior maximum is constant on its component); the submean convention is that of Subharmonic functions on plane domains.
The equal-radius polydisc radius is the distance to the complement in the coordinate sup norm (The equal-radius polydisc boundary function), and its negative logarithm being psh is Hartogs pseudoconvexity (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).
Choice use. AC is the ambient hypothesis. The argument makes only finitely many selections for each disc, direction and harmonic majorant.
Proof
For each fixed nonzero define These radii are positive and finite because is open and bounded. If , the closed directional disc of radius is compact in , and sufficiently small translations stay in . Thus is lower semicontinuous, so is upper semicontinuous.
Fix an affine base disc with , and a continuous real harmonic majorant on the closed unit disc with on its boundary. For the function is harmonic on a disc of radius greater than , and uniformly on the closed unit disc. Given , choose so that there; by [F3] choose a holomorphic on a disc of radius greater than with . Then is holomorphic near the closed base disc, and for , , its value belongs to , since . Compactness of the base disc also puts all its images in for sufficiently small .
Let be the supremum of radii for which . Suppose , and fix . The image of is a compact subset of by step 2.1. Let be the maximum of on this image. For each , [F1] makes subharmonic, continuous on the closed base disc; its boundary values are at most , so [F4] bounds it everywhere by . All these images therefore lie in the fixed compact sublevel . By continuity their limits with also lie in . Uniform continuity on a slightly larger compact product then increases the admissible radius beyond , contradicting its definition. Thus , and throughout the base disc.
Step 3.1 gives . Choose and with the stated uniform error, to conclude . The affine-disc normalization covers every closed disc in every complex line in . Hence [F2], together with the upper semicontinuity of step 1.1, makes each plurisubharmonic. The dilation of the majorant in step 2.1 ensures that and are defined past the base boundary; no boundary continuity of an arbitrary harmonic conjugate is assumed.
Write . A sup-norm polydisc of radius consists exactly of all directional discs of radius with , so By [F5], is a positive continuous distance function on , so is continuous. On any compactly contained affine circle, each satisfies its submean inequality and is at most on the circle. Therefore at the center is at most the circle average of ; taking the supremum gives that same bound for at the center. Its continuity and these submean inequalities make it psh by [F1] and [F4]. This proves the exact Hartogs convention of [F5].
Peak functions at strongly pseudoconvex boundary points, by a dbar correction
Statement
Assume the Axiom of Choice (AC). Let , let be a bounded open set and let . Suppose that there are a neighbourhood of and a function such that and such that is strictly plurisubharmonic on some neighbourhood of (The Levi form and strict plurisubharmonicity).
-
Then there is a function , holomorphic on a neighbourhood of , with
-
(Strongly pseudoconvex boundaries.) The same conclusion holds when is a bounded domain whose boundary is of class and strongly pseudoconvex at every point, that is: for every there are a neighbourhood of and with , and for every nonzero complex tangent vector at (Levi pseudoconvex domains); namely, there is then holomorphic on a neighbourhood of with and on .
Facts & Assumptions
Given: AC; ; a bounded open ; ; and the smooth negative-set defining data in branch 1. Branch 2 is reduced to this data in step 7.1. Coordinates are canonical .
Real second-order Taylor expansion, rewritten using Wirtinger derivatives, separates the real part of a holomorphic linear/quadratic polynomial from the Hermitian Levi quadratic form. Strict psh means the latter is positive definite (Second-order Taylor expansion , Wirtinger operators in , The Levi form and strict plurisubharmonicity).
The negative set of smooth data strictly psh near its boundary has arbitrarily small outer neighborhoods consisting of finitely many bounded smooth strongly pseudoconvex domains, each with a continuous psh exhaustion; critical boundary points are allowed (Positive smooth collars for strictly plurisubharmonic negative sets).
Smooth strongly pseudoconvex boundary data admit a global smooth defining function strictly psh near the boundary (Smooth global defining functions for strongly pseudoconvex boundaries), for the boundary convention of Levi pseudoconvex domains.
Under AC and countable choice a continuous psh exhaustion has a smooth strictly psh exhaustive majorant (Smooth strict plurisubharmonic regularization of a psh exhaustion). On a bounded domain a smooth psh exhaustion implies Hartogs pseudoconvexity with the equal-radius polydisc convention (A smooth psh exhaustion gives Hartogs pseudoconvexity on bounded domains).
On a Hartogs pseudoconvex domain, with smooth strictly psh weight , every smooth closed -form of finite weighted energy has a smooth scalar solution of (Hörmander's weighted L2 existence theorem for the dbar equation, Statement, smooth-data branch).
There is a smooth cutoff in , equal to on a smaller closed ball and supported in a larger open ball (A smooth bump between concentric Euclidean balls).
Smooth forms satisfy (The d, partial and dbar identities). A smooth function with all derivatives zero is holomorphic (For functions, holomorphy, complex linearity of the real derivative, and the Cauchy–Riemann system agree); polynomial algebra and reciprocals of nonzero holomorphic functions are holomorphic (Sums, products and nonvanishing quotients of holomorphic functions are holomorphic).
The complex exponential satisfies (, , and ).
AC implies countable choice (The Axiom of Choice, The Axiom of Countable Choice (), AC implies DC implies countable choice).
Choice use. AC is inherited by the collar, regularization and Hörmander interfaces; it supplies countable choice for [F4]. Only finitely many outer components and corrections are selected. The polynomial, cutoff, corrected quotient and exponential below are explicit once those data are fixed.
Proof
Put and define the holomorphic Levi polynomial By [F1], The Hermitian form is bounded below by for some . Choose with and remainder at most . Since on , Thus and is zero-free on this part of . The argument includes : the linear term then vanishes and the same quadratic estimate applies.
Fix . By [F6] take equal to on a neighborhood of . Its derivative support lies in the compact annulus . The compact set is disjoint from by step 1.1. Apply [F2] with the prescribed open neighborhood to get , with . Hence is bounded away from zero on when this set is nonempty. On define in the annulus and zero outside it. More precisely, use the quotient on the open zero-free neighborhood of and zero wherever is locally constant. These definitions agree, so is smooth, bounded on , and by [F7]. It vanishes near and satisfies everywhere on . No sublevel of is asserted to lie in a ball.
Each has a continuous psh exhaustion by [F2]. Using [F9], apply [F4] to regularize it and then conclude that is Hartogs pseudoconvex in the actual polydisc-radius convention. Take : its Levi eigenvalues are all . The energy is finite because is bounded and is bounded. Thus [F5] gives a smooth scalar on with . Define on each of the finitely many disjoint components. Then solves , is holomorphic near , and is bounded on the compact set . The data need not have compact support in each : boundedness on the bounded domain proves the required finite energy.
Choose and put on . Since , so is holomorphic by [F7]. Where in a neighborhood, is holomorphic and the expression is holomorphic wherever . Where , the expression is holomorphic. The two expressions agree on their common domain where is locally zero: and there forces . They therefore glue on the union of these open sets.
This union contains . At a point of outside , is locally zero and . At a point other than , step 1.1 gives and , whence Thus . At one has , so is holomorphic on a full neighborhood of and . Every point of has : where this follows from , and where from the same displayed inequality and . Therefore is holomorphic on an open neighborhood of , vanishes at , and has positive real part on .
Set on this neighborhood. It is holomorphic, , and for every . This proves branch 1 under exactly its stated smooth negative-set hypotheses, including critical boundary points and disconnected .
Under the smooth strongly pseudoconvex boundary hypotheses of branch 2, [F3] constructs a defining function on a neighborhood of , strictly psh near . Its proof glues the given smooth local defining functions with a finite partition near the compact boundary, extends with a sign-constant interior/exterior term, and applies after a tangent/normal Levi estimate. Thus it supplies the smooth data required by branch 1 without upgrading a merely function. Step 6.1 now gives the same for branch 2.
Both branches of the Statement hold with all their original hypotheses, under the ambient AC.
Oka-Weil approximation on a domain of holomorphy (host-domain lemma)
Statement
Assume the Axiom of Choice (AC). Let be a domain of holomorphy (Holomorphic extension and domains of holomorphy in several variables), let be compact and convex with respect to the holomorphic functions on , i.e. (Holomorphic hulls and holomorphic convexity), and let be holomorphic in an open neighbourhood of . Then for every there is with
Facts & Assumptions
Given: The Axiom of Choice; a domain of holomorphy; a compact with ; a function holomorphic on an open neighbourhood of ; and .
The holomorphic hull is (Holomorphic hulls and holomorphic convexity). Thus is exactly the compact -convexity hypothesis.
(Harold P. Boas, Lecture Notes on Multidimensional Complex Analysis, §3.3.2, Theorem 21, printed p. 79, with proof on printed pp. 79–80.) If is a domain of holomorphy in and is compact and convex with respect to , then every function holomorphic in a neighbourhood of is uniformly approximable on by functions in . The proof uses finite analytic-polyhedron reduction, Oka's graph lift and a correction, a power-series approximation, and a telescoping exhaustion.
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 [F3]. No additional choice is made in applying [F2].
Proof
If , take , since the supremum of the nonnegative empty family is in the convention of [F1]. Otherwise the hypotheses of Boas's Theorem 21 [F2] hold with and : is a domain of holomorphy, and is the required -convexity condition by [F1]. The given is holomorphic in a neighbourhood of .
For nonempty , apply [F2] with approximation tolerance . It gives with , which is the Statement under the ambient AC assumption [F3].
The Levi problem: pseudoconvexity, domains of holomorphy, and holomorphic convexity
Statement
Assume the Axiom of Choice (AC). Let be a domain, . Then the following three conditions are equivalent:
- is Hartogs pseudoconvex (Plurisubharmonic exhaustions and Hartogs pseudoconvexity);
- is a domain of holomorphy (Holomorphic extension and domains of holomorphy in several variables);
- is holomorphically convex, that is, for every compact (Holomorphic hulls and holomorphic convexity).
Facts & Assumptions
Given: The Axiom of Choice and a domain , .
Hartogs pseudoconvexity gives a continuous plurisubharmonic exhaustion on (Hartogs pseudoconvexity yields a continuous plurisubharmonic exhaustion).
In Demailly, Complex Analytic and Differential Geometry, Ch. I §7.A, Theorem 7.2(c) implies (e): a plurisubharmonic exhaustion on a proper open subset of makes plurisubharmonic, which is his pseudoconvexity criterion. Ch. VIII §9, Theorem 9.11(a), printed pp. 392–393, says that an open subset of is a domain of holomorphy if and only if it is pseudoconvex. Its proof of the forward implication used here applies Skoda's Theorem 9.10 to the coordinate functions at a boundary point with a plurisubharmonic distance weight; the resulting identity prevents common holomorphic continuation across .
For a domain in , being a domain of holomorphy is equivalent to holomorphic convexity (Cartan-Thullen theorem).
Every domain of holomorphy in is Hartogs pseudoconvex (Domains of holomorphy are Hartogs pseudoconvex).
The holomorphic hull of a compact set is closed in its ambient domain and bounded in each coordinate (Basic properties of the holomorphic hull). A closed bounded subset of is compact (Complex -space and its real coordinate dictionary, Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).
AC supplies the ambient choice assumptions of the source theorem and the cited library interfaces (The Axiom of Choice).
Choice use. AC is the stated ambient hypothesis. The proof itself makes no new arbitrary selection; the nontrivial existence theorem imported in [F2] is used under its classical choice setting.
Proof
Suppose is Hartogs pseudoconvex and proper in . By [F1] it has a continuous plurisubharmonic exhaustion. Demailly's pseudoconvexity equivalence in [F2] makes it pseudoconvex in his sense; his Levi theorem in [F2] then gives that is a domain of holomorphy.
If , then for every compact its holomorphic hull is closed in and coordinate-bounded by [F5], hence compact. Thus is holomorphically convex and therefore a domain of holomorphy by [F3]. This covers the whole-space convention separately.
By [F3], the domain-of-holomorphy conclusion of steps 1.1–1.2 is equivalent to holomorphic convexity. Conversely, either of those conditions gives Hartogs pseudoconvexity by [F4]. Hence all three conditions in the Statement are equivalent.
Behnke-Stein: increasing unions of pseudoconvex domains
Statement
Assume the Axiom of Choice (AC). Let be an increasing sequence of Hartogs pseudoconvex domains in , , whose union is a domain. Then is Hartogs pseudoconvex: when this is the whole-space convention, and otherwise, for every , the decreasing tail consists of plurisubharmonic functions on and converges pointwise there to .
Facts & Assumptions
Given: The Axiom of Choice; an increasing sequence of domains in , , each Hartogs pseudoconvex, with union a domain.
A domain is Hartogs pseudoconvex when the function is plurisubharmonic on , where is the equal-radius polydisc boundary function (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).
When one has and the boundary function is by convention the constant function ; thus the whole space is Hartogs pseudoconvex (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).
The equal-radius polydisc boundary function is for , where is the open polydisc of constant polyradius (The equal-radius polydisc boundary function).
The closed polydisc is and the open polydisc is defined by the strict inequalities (Balls, polydiscs and the distinguished boundary in ).
A subset of is compact if and only if it is closed and bounded (Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).
Under the identification of with the metric, the balls, the open sets, the convergent sequences and the continuous maps of are verbatim those of (Complex -space and its real coordinate dictionary).
If is a decreasing sequence of plurisubharmonic functions on a domain and pointwise, then either on a connected component, or is plurisubharmonic (Decreasing limits of plurisubharmonic functions).
AC states that every family of nonempty sets has a choice function (The Axiom of Choice).
Choice use. AC is the ambient hypothesis recorded in the Statement. The proof selects nothing: the indices attached to a compact set or to a radius are produced by a finite subcover argument and then taken to be maximal in the increasing family, and the functions are given. No family of nonempty sets is chosen from.
Proof technique: direct.
Proof
If , then [F2] is exactly the conclusion, so assume from now on that ; then is nonempty, and writing and in the sense of [F3] one has for every (positivity because is open, finiteness because ) and for every .
For the inclusion implies for every , hence and, if , the eventual-tail limit exists and is independent of ; moreover , because for every with and every with the definition [F3] gives , so the closed polydisc of [F4] is closed and bounded in , hence compact by [F5] read through [F6], and is therefore covered by finitely many members of the increasing open cover of , whose largest index, increased to if necessary, satisfies and hence ; letting gives .
Let be compact and choose with (the same finite-subcover argument applied to the increasing cover of ); then for every the function is plurisubharmonic on by the hypothesis that is Hartogs pseudoconvex and [F1], hence on the smaller domain , the sequence is decreasing on by step 2.1, and it converges pointwise on to by the identity of step 2.1; the limit is real-valued on because there by step 1.1, so it is not identically on any component and [F7] makes plurisubharmonic on .
Every point lies in some , an open neighbourhood of on which is plurisubharmonic by step 3.1 applied with ; plurisubharmonicity is a local condition, so is plurisubharmonic on and [F1] makes Hartogs pseudoconvex; together with the whole-space case of step 1.1 this proves the statement in both cases.
Oka-Weil approximation on a pseudoconvex domain
Statement
Assume the Axiom of Choice (AC). Let be a domain that is Hartogs pseudoconvex (Plurisubharmonic exhaustions and Hartogs pseudoconvexity), let be compact with (Holomorphic hulls and holomorphic convexity), and let be holomorphic in an open neighbourhood of . Then for every there is with
Facts & Assumptions
Given: The Axiom of Choice; a Hartogs pseudoconvex domain ; a compact with ; a holomorphic on an open neighbourhood of ; a real number .
For a domain the following three conditions are equivalent: is Hartogs pseudoconvex; is a domain of holomorphy; is holomorphically convex (The Levi problem: pseudoconvexity, domains of holomorphy, and holomorphic convexity).
If is a domain of holomorphy, is compact with , and is holomorphic in an open neighbourhood of , then for every there is with (Oka-Weil approximation on a domain of holomorphy (host-domain lemma)).
AC is the assertion that every family of nonempty sets has a choice function (The Axiom of Choice).
Choice use. AC is the ambient hypothesis recorded in the Statement and cited as [F3]; it is consumed only inside the suppliers [F1] and [F2], each of which carries its own choice hypotheses. The proof selects nothing.
Proof
By [F1] the Hartogs pseudoconvex domain is a domain of holomorphy.
Applying [F2] with , , and , and with , gives with , which is the assertion of the Statement under the ambient Axiom of Choice cited as [F3].
Locally finite smooth partitions of unity on domains
Statement
Assume the Axiom of Choice (AC) and the Axiom of Countable Choice. Let , , be a domain and let be an open cover of . Then there are an open cover of refining and functions , , such that:
- is locally finite and there is a map with for every ;
- and for every ;
- the family is locally finite;
- at every point of .
In particular is a smooth partition of unity subordinate to the locally finite refinement .
Facts & Assumptions
Given: The Axiom of Choice and the Axiom of Countable Choice; a domain with ; an open cover of ; the function on , read as when .
A family of smooth functions is a smooth partition of unity subordinate to an open cover of a smooth manifold when the supports are locally finite, for every , and for every (Smooth partitions of unity subordinate to an open cover).
For all there is a smooth function with on and (A smooth bump between concentric Euclidean balls).
A subset is a compact subset of if and only if is closed in and bounded (Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).
Under the coordinate identification of with the metric, the balls, the open sets, the convergent sequences, the Cauchy sequences and the continuous maps of are verbatim those of (Complex -space and its real coordinate dictionary).
The Axiom of Countable Choice: for every family of nonempty sets there is with domain and for all (The Axiom of Countable Choice ()).
AC states that every family of nonempty sets has a choice function (The Axiom of Choice).
Choice use. AC selects, for each point of the shells below, one cover member and one radius; the countable instance [F5] selects the finite subcover list of each shell and the bumps built on it. No other selection occurs: the shell functions , , and the normalisation are explicit.
Proof
If , then is constant. Otherwise , and for and every , , so taking infima and then interchanging gives . Thus is continuous in either case. For put ; then each is closed in (intersection of the closed ball with the closed set ) and bounded, hence compact by [F3] read through [F4]; moreover , because and hold for and persist on a small ball around by continuity of the modulus and of ; finally , since for one has (or ) and , so some integer satisfies and .
Put for and, for , and ; then every is compact (a closed subset of the compact ), with open (because and ), and the cover : for let , which exists by step 1.1, so and , that is . The family is locally finite: a neighbourhood of contained in misses every with , while only finitely many smaller indices remain; thus the family is locally finite.
For each the set of finite lists (including the empty list when ) with , , , and is nonempty: for every the cover gives some with , the set is open and contains , so some radius satisfies (choosing the pair by [F6]), and compactness of by step 2.1 lets the resulting open cover be reduced to a finite subcover; by [F5] select one such finite list for every and enumerate the union of the selected lists as a sequence of balls . Then by step 2.1.
For each , [F2] applied with the pair and the centre provides a smooth with on and ; the balls here are Euclidean balls of under the identification of [F4], so . By step 3.1, ; the countably many choices of the are read through [F5]. Since only finitely many selected balls occur for each , each support lies in its assigned , and the family is locally finite by step 2.1, every point of has a neighbourhood meeting only finitely many supports, so is a well-defined smooth function on ; finally at every point of , because every point lies in some by step 2.1 and hence in some selected ball on which .
Define , so each is open with and with by step 4.1, and put ; then , , , and because . The family covers , because makes positive at every point for at least one , and then that point lies in ; it refines by the map , and is locally finite because and is locally finite by step 2.1; the supports of the are locally finite for the same reason. Hence is a smooth partition of unity subordinate to the locally finite refinement in the sense of [F1].
First Cousin problem on a pseudoconvex domain
Statement
Assume the Axiom of Choice (AC). Let and let be a Hartogs pseudoconvex domain (Plurisubharmonic exhaustions and Hartogs pseudoconvexity). Let be a locally finite open cover of and, for every , let be a meromorphic function on (Meromorphic functions on an open set in complex Euclidean space) such that for all the difference is holomorphic on (clause (c) of the definition of a meromorphic function).
Then there is a meromorphic function on such that is holomorphic on for every . Equivalently, the first Cousin problem with the locally finite data is solvable: one global meromorphic function realizes the prescribed principal parts.
Facts & Assumptions
Given: The Axiom of Choice; an integer ; a Hartogs pseudoconvex domain ; a locally finite open cover of ; meromorphic functions on with holomorphic on for all ; the Wirtinger operators and the operators on smooth forms of Bigraded complex forms and the Dolbeault operators.
A domain is Hartogs pseudoconvex when is plurisubharmonic on (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).
If is meromorphic on an open with domain and , then is meromorphic on (clause (d) of Meromorphic functions on an open set in complex Euclidean space); and is holomorphic on an open when some agrees with on (clause (c)).
Meromorphy is a local condition: if every point of has a neighbourhood to which restricts as a meromorphic function, then is meromorphic on (Meromorphic functions on an open set in complex Euclidean space).
Let be a domain and let be an open cover of . Then there are a locally finite open cover of refining with and smooth functions with , , locally finite supports and on (Locally finite smooth partitions of unity on domains).
Let be Hartogs pseudoconvex and let . Every smooth -closed -form on is exact in the Dolbeault complex: there is a smooth -form with (Positive-degree Dolbeault vanishing on pseudoconvex domains, claim 1).
Let be open and of class . Then is complex differentiable at if and only if for every (clause 3 of For functions, holomorphy, complex linearity of the real derivative, and the Cauchy–Riemann system agree); a function is holomorphic on when it is complex differentiable at every point of (Holomorphic functions on an open subset of ).
On smooth complex-valued forms and (The d, partial and dbar identities); on a -form one has , and components outside the bidegree range are zero (Bigraded complex forms and the Dolbeault operators).
AC is the statement that every family of nonempty sets has a choice function (The Axiom of Choice); in ZF, AC implies the Axiom of Countable Choice (AC implies DC implies countable choice), which selects one element from each family of nonempty sets indexed by (The Axiom of Countable Choice ()).
Choice use. AC is the ambient hypothesis of the corollary. The partition-of-unity lemma [F4] selects cover members over its shell construction using AC and uses its countable instance for the finite lists and bumps; [F8] supplies that implication. This proof makes no additional selection.
Proof
Apply [F4] to the cover : let be the resulting locally finite refinement with , and let be the associated smooth partition of unity with , , locally finite supports and on . The countable-choice hypothesis of [F4] is discharged by the implication from [F8].
For each fixed define on as follows. By hypothesis the difference is holomorphic on , a set containing ; multiplying by the cutoff , which vanishes outside , extends it by zero to a smooth function on , and the family is locally finite, so every point of has a neighbourhood on which only finitely many terms are nonzero; hence the sum is a well-defined element of .
For , evaluate on the dense open set where all relevant meromorphic representatives are defined. There each summand of equals , so there. The left side is continuous, and the right side has the given holomorphic extension to . Equality on the dense set and continuity give equality everywhere with that extension; in particular is holomorphic on the overlap.
Define on by , a smooth -form on by [F7] and step 1.2. For the identity of step 2.1 gives on , and is holomorphic there, so by the Cauchy-Riemann system [F6] and [F7]. Hence on every overlap, so the local definitions glue to a well-defined smooth -form .
On each one has with smooth, hence on by [F7]; therefore is a smooth -closed -form on .
Since is Hartogs pseudoconvex and is smooth and -closed, [F5] with provides with ; by the conventions of [F7] the space is the space of smooth functions, so is a smooth function on .
For each put on , a smooth function by step 1.2 and step 5.1; then on by step 3.1 and step 5.1. Since is , the Cauchy-Riemann system [F6] makes complex differentiable at every point of , that is, holomorphic on .
Let be the open dense domain of the representative and put , an open dense subset of . Define by when . On , the compatibility of the meromorphic differences and step 2.1 give , so is well defined. It is holomorphic on because each local expression is holomorphic there. Near any point choose a chart and a local ratio on . On the dense open set one has ; both sides are holomorphic on , so continuity extends this identity there. Thus has the required local ratio and [F3] makes it meromorphic on .
Finally on the common domain for every by the definition of , and is a holomorphic extension to by step 6.1; thus the meromorphic function realizes the prescribed principal parts , as asserted. [step 6.1, step 7.1]
Remarks
Local finiteness is not needed. The proof uses the locally finite cover only as an input to the partition-of-unity lemma [F4], whose output is locally finite for an arbitrary open cover; the argument is verbatim valid for an arbitrary open cover with compatible meromorphic data, and the locally finite case stated here is the form promised by the scaffold.
Why the pseudoconvexity enters. The only analytic input is the smooth solvability of the -equation for -forms on , supplied here by [F5]. On the ball or on a polydisc this is the classical Dolbeault lemma; on a general Hartogs pseudoconvex domain it is the content of the in-pair corollary, and it is exactly the hypothesis that fails on , where the Cousin-I data on the two coordinate complements is not solvable.
Holomorphy of the correction. The smooth solution of is used, not merely an solution: the local corrections must be so that the Cauchy-Riemann system [F6] applies, and this is why the smooth branch of the vanishing corollary [F5] is invoked.
5 · Examples, counterexamples and false statements
None yet.
Sources
- Jean-Pierre Demailly, Complex Analytic and Differential Geometry
- Jiří Lebl, Tasty Bits of Several Complex Variables
- Harold P. Boas, Lecture Notes on Several Complex Variables
- Mohammad Jabbari, Several Complex Variables course notes
- Friedrich Haslinger, Complex analysis, the dbar-Neumann problem, and Schrodinger operators (author manuscript)
- Jiri Lebl, Tasty Bits of Several Complex Variables