CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-02

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Positive-degree Dolbeault vanishing on pseudoconvex domains

Statement

Assume the Axiom of Choice (AC). Let $n \geq 1$ , let $Ω \subseteq C^{n}$ be a domain, and suppose that $Ω$ is Hartogs pseudoconvex (Plurisubharmonic exhaustions and Hartogs pseudoconvexity). Let $1 \leq q \leq n$ .

(Smooth vanishing.) Every smooth $\overset{ˉ}{\partial}$ -closed $(0, q)$ -form $η \in Ω^{0, q} (Ω)$ (Bigraded complex forms and the Dolbeault operators) is exact in the Dolbeault complex: there is $ζ \in Ω^{0, q - 1} (Ω)$ with $\overset{ˉ}{\partial} ζ = η$ . Consequently $H_{\overset{ˉ}{\partial}}^{0, q} (Ω) = 0$ (Dolbeault cohomology of a domain).
(Weighted $L^{2}$ exactness under finite energy.) Let $φ \in C^{2} (Ω; R)$ be strictly plurisubharmonic on $Ω$ (The Levi form and strict plurisubharmonicity); for $a \in Ω$ let $λ_{1} (a) \leq \dots \leq λ_{n} (a)$ be the eigenvalues of the Hermitian matrix $(φ_{j \overset{ˉ}{k}} (a))$ and put $w (a) : = λ_{1} (a) + \dots + λ_{q} (a) > 0$ . If $f \in Dom {\overset{ˉ}{\partial}}_{q}$ satisfies ${\overset{ˉ}{\partial}}_{q} f = 0$ and $E (f) : = \int_{Ω} ∣ f ∣^{2} w^{- 1} e^{- φ} d V < + \infty,$ then there is $u \in Dom {\overset{ˉ}{\partial}}_{q - 1}$ with ${\overset{ˉ}{\partial}}_{q - 1} u = f$ and $∥ u ∥_{φ}^{2} \leq E (f)$ .

No boundary regularity of the primitives is claimed, and the statement is asserted for $1 \leq q \leq n$ only.

Facts & Assumptions

Given: The Axiom of Choice; an integer $n \geq 1$ ; a Hartogs pseudoconvex domain $Ω \subseteq C^{n}$ ; an integer $1 \leq q \leq n$ ; a smooth $\overset{ˉ}{\partial}$ -closed $(0, q)$ -form $η \in Ω^{0, q} (Ω)$ ; and a triple $(φ, f, w)$ consisting of a strictly plurisubharmonic $φ \in C^{2} (Ω; R)$ , its eigenvalue functions $λ_{1} \leq \dots \leq λ_{n}$ and $w = λ_{1} + \dots + λ_{q}$ , and a form $f \in Dom {\overset{ˉ}{\partial}}_{q}$ with ${\overset{ˉ}{\partial}}_{q} f = 0$ and $E (f) < + \infty$ .

[F1]

A domain $Ω$ is Hartogs pseudoconvex when $- \log δ_{Ω}$ is plurisubharmonic on $Ω$ , where $δ_{Ω}$ is the equal-radius polydisc boundary function (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).

[F2]

If $Ω \subseteq C^{n}$ is Hartogs pseudoconvex, then there are $S \in C^{\infty} (Ω)$ strictly plurisubharmonic and a strictly increasing sequence $c_{k} \to + \infty$ such that, with $Ω_{k} : = {z \in Ω : S (z) < c_{k}}$ : every $c_{k}$ is a regular value of $S$ , every $\partial Ω_{k} = {z \in Ω : S (z) = c_{k}}$ is a nonempty $C^{\infty}$ hypersurface of $Ω$ , $\overline{Ω_{k}} \subseteq Ω_{k + 1}$ and $⋃_{k} Ω_{k} = Ω$ , so every $\overline{Ω_{k}}$ is a compact subset of $Ω$ (Smooth strictly plurisubharmonic exhaustion of a pseudoconvex domain).

[F3]

For $u \in C^{2} (Ω, R)$ the Levi form is $L_{u} (a; v) = \sum_{j, k} \frac{\partial^{2} u}{\partial z_{j} \partial {\overset{ˉ}{z}}_{k}} (a) v_{j} \overline{v_{k}}$ , and $u$ is strictly plurisubharmonic when $L_{u} (a; v) > 0$ for every $a \in Ω$ and every $v \neq 0$ ; a strictly plurisubharmonic function is plurisubharmonic (The Levi form and strict plurisubharmonicity).

[F4]

A $C^{2}$ function $u$ on an open set is plurisubharmonic if and only if $L_{u} (a; v) \geq 0$ for every $a$ and every $v$ (The C^2 Levi criterion for plurisubharmonicity).

[F5]

If $u : Ω \to R$ is plurisubharmonic and $ϕ : R \to R$ is convex and nondecreasing, then $ϕ \circ u$ is plurisubharmonic on $Ω$ (Basic stability operations for plurisubharmonic functions).

[F6]

With $Ω^{p, q} (U)$ the smooth complex-valued forms of bidegree $(p, q)$ on open $U$ , $Z_{\overset{ˉ}{\partial}}^{p, q} (U) = \ker (\overset{ˉ}{\partial} : Ω^{p, q} (U) \to Ω^{p, q + 1} (U))$ , $B_{\overset{ˉ}{\partial}}^{p, q} (U) = im (\overset{ˉ}{\partial} : Ω^{p, q - 1} (U) \to Ω^{p, q} (U))$ and $H_{\overset{ˉ}{\partial}}^{p, q} (U) = Z_{\overset{ˉ}{\partial}}^{p, q} (U) / B_{\overset{ˉ}{\partial}}^{p, q} (U)$ (Dolbeault cohomology of a domain).

[F7]

Hörmander's weighted $L^{2}$ existence theorem (Hörmander's weighted L2 existence theorem for the dbar equation): under AC, with $Ω$ Hartogs pseudoconvex, $φ \in C^{2} (Ω; R)$ strictly plurisubharmonic, $1 \leq q \leq n$ , eigenvalues $λ_{1} \leq \dots \leq λ_{n}$ and $w = λ_{1} + \dots + λ_{q}$ : (claim 1) every $f \in Dom {\overset{ˉ}{\partial}}_{q}$ with ${\overset{ˉ}{\partial}}_{q} f = 0$ and finite energy $E (f) = \int_{Ω} ∣ f ∣^{2} w^{- 1} e^{- φ} d V$ has a solution $u \in Dom {\overset{ˉ}{\partial}}_{q - 1}$ with ${\overset{ˉ}{\partial}}_{q - 1} u = f$ and $∥ u ∥_{φ}^{2} \leq E (f)$ ; (claim 2) if in addition $φ \in C^{\infty} (Ω; R)$ and $f \in C^{\infty} (Ω; Λ^{0, q})$ is $\overset{ˉ}{\partial}$ -closed with $E (f) < + \infty$ , then there is $u \in C^{\infty} (Ω; Λ^{0, q - 1}) \cap L_{0, q - 1}^{2} (Ω, e^{- φ})$ with $\overset{ˉ}{\partial} u = f$ and $∥ u ∥_{φ}^{2} \leq E (f)$ .

[F8]

With the conventions of Weighted L2 spaces and maximal dbar operators: $L_{0, k}^{2} (Ω, e^{- φ})$ is the space of coefficient tuples with the inner product $⟨ u, v ⟩_{φ} = \int_{Ω} \sum_{∣ J ∣ = k} u_{J} \overline{v_{J}} e^{- φ} d V$ , and $Dom {\overset{ˉ}{\partial}}_{k}$ consists of those $u$ for which the distributional $\overset{ˉ}{\partial} u$ is represented by an element of $L_{0, k + 1}^{2}$ , which is then ${\overset{ˉ}{\partial}}_{k} u$ .

[F10]

The standard smooth step function is $σ (t) = β (t) / (β (t) + β (1 - t))$ with $β$ the standard flat function; it satisfies $σ \in C^{\infty} (R)$ , $σ (t) = 0$ for $t \leq 0$ and $σ (t) = 1$ for $t \geq 1$ , and takes values in $[0, 1]$ (The standard smooth step function).

[F11]

The standard flat function $β (t) = \exp (- 1 / t)$ for $t > 0$ and $β (t) = 0$ for $t \leq 0$ satisfies $β \in C^{\infty} (R)$ and $β (t) > 0$ for $t > 0$ (The standard flat function, The standard flat function is smooth and flat at zero).

[F12]

Every continuous function $f : I \to R$ on an order-convex interval $I$ with at least two elements has a primitive $G$ on $I$ ; the function $F (x) = \int_{c_{0}}^{x} f$ is one, and for $a < b$ in $I$ and any primitive $G$ , $\int_{a}^{b} f = G (b) - G (a)$ (Every continuous function on an interval has a primitive; two primitives differ by a constant; and $\int_{a}^{b} f = G (b) - G (a)$ for any primitive $G$ ).

[F13]

For $α < β$ and integrable $f : [α, β] \to R$ and arbitrary $u, v, w \in [α, β]$ one has $\int_{u}^{v} f + \int_{v}^{w} f = \int_{u}^{w} f$ (For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ ).

[F14]

For a bounded $f : [a, b] \to R$ the Darboux sums over a partition $P$ are the lower and upper sums $L (f, P) \leq U (f, P)$ , and $f$ is integrable with $\int_{a}^{b} f$ defined through these sums (For bounded $f$ on $[a, b]$ and a partition $P$ : the infimum $m_{i}$ and supremum $M_{i}$ of $f$ on the $i$ -th subinterval, and the lower and upper Darboux sums $L (f, P) = \sum_{i} m_{i} Δ_{i}$ and $U (f, P) = \sum_{i} M_{i} Δ_{i}$ , The lower and upper Darboux integrals of a bounded $f$ on $[a, b]$ as $\sup_{P} L (f, P)$ and $\inf_{P} U (f, P)$ , Darboux integrability as their equality, and the notation $\int_{a}^{b} f$ ).

[F15]

For a nonempty $A \subseteq R^{n}$ the following are equivalent: $A$ is compact; $A$ is closed and bounded; every continuous $f : A \to R$ attains a maximum and a minimum on $A$ (For a nonempty subset of $R^{n}$ with $n \geq 1$ , compactness, closedness and boundedness, pseudocompactness, and attainment of extrema by every continuous real-valued function are equivalent).

[F16]

Under the identification of $C^{m}$ with $R^{2 m}$ , the metric of $C^{m}$ , its balls, its open sets, its convergent sequences, its Cauchy sequences and its continuous maps are verbatim those of $R^{2 m}$ (Complex $m$ -space and its real coordinate dictionary).

[F17]

Under the Axiom of Countable Choice, every bounded subset $E \subseteq R^{n}$ has finite outer measure, a bounded Lebesgue measurable set has finite measure, and every compact subset of $R^{n}$ is Lebesgue measurable of finite measure (Lebesgue measure is sigma-finite, and every metrically bounded subset of $R^{n}$ has finite outer measure).

[F18]

Under the Axiom of Countable Choice, every continuous map $R^{n} \to R^{m}$ is Borel measurable (Continuous functions on Euclidean spaces are Borel measurable).

[F19]

If $f, g : X \to [0, + \infty]$ are measurable and $c \geq 0$ : $f \leq g$ implies $\int f \leq \int g$ , and $\int c f = c \int f$ for $c > 0$ (Monotonicity and nonnegative homogeneity of the nonnegative integral).

[F20]

For a nonnegative simple measurable function $s = \sum_{j} c_{j} χ_{E_{j}}$ with pairwise disjoint measurable $E_{j}$ and $c_{j} \geq 0$ , the simple integral is $\int s d μ = \sum_{j} c_{j} μ (E_{j})$ (The integral of a nonnegative simple function).

[F21]

For nonnegative measurable functions $f_{k}$ with $S = \sum_{k = 0}^{\infty} f_{k}$ one has $\int S d μ = \sum_{k = 0}^{\infty} \int f_{k} d μ$ (Beppo Levi's theorem for nonnegative series).

[F22]

If a real sequence $(a_{k})$ has no vanishing term and ${lim sup}_{k} ∣ a_{k + 1} / a_{k} ∣ < 1$ , then $\sum ∣ a_{k} ∣$ converges (Ratio test: $lim sup ∣ a_{k + 1} / a_{k} ∣ < 1$ gives absolute convergence and hence convergence, and $lim inf ∣ a_{k + 1} / a_{k} ∣ > 1$ gives divergence).

[F23]

The exponential function is strictly increasing (The exponential function is strictly increasing).

[F24]

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 $T v = λ v$ , $v \neq 0$ , one gets $λ ⟨ v, v ⟩ = ⟨ T v, v ⟩ = ⟨ v, T v ⟩ = \overline{λ} ⟨ v, v ⟩$ with $⟨ v, v ⟩ > 0$ .

[F25]

The determinant of a matrix is the product of its eigenvalues, counted with algebraic multiplicity (If $χ_{T} (x) = \prod_{i < n} (x - λ_{i})$ in $F [x]$ , then $\det (T) = \prod_{i < n} λ_{i}$ : determinant is the product of the eigenvalues counted with algebraic multiplicity).

[F26]

The trace of a matrix is the sum of its eigenvalues, counted with algebraic multiplicity (If $χ_{T} (x) = \prod_{i < n} (x - λ_{i})$ in $F [x]$ , then $tr (T) = \sum_{i < n} λ_{i}$ : trace is the sum of the eigenvalues counted with algebraic multiplicity).

[F27]

A twice differentiable $f : I \to R$ on an open interval is convex if and only if $f^{''} (x) \geq 0$ for every $x \in I$ (A twice-differentiable function on an open interval is convex if and only if its second derivative is nonnegative).

[F28]

Finite componentwise sums and products of $C^{k}$ Euclidean maps are $C^{k}$ , and a composite of composable $C^{k}$ Euclidean maps is $C^{k}$ ( $C^{k}$ Euclidean maps are closed under componentwise algebra and composition).

[F29]

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

[F30]

If $f : U \to V$ and $g : V \to R^{p}$ are totally differentiable at $a$ and $f (a)$ , then $g \circ f$ is totally differentiable at $a$ with $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[F31]

For functions with continuous second partial derivatives the mixed second partials commute (Continuous second partials of a scalar potential commute).

[F32]

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 ( ${A C}_{ω}$ )); 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 $A_{j}$ , the numbers $θ_{j}$ , the sequence $d_{i}$ , the coefficients $a_{i}$ and the function $F$ are all defined by explicit formulas.

Proof

technique · direct

1.1F1F2F15F16

By [F2] and the definition [F1] of Hartogs pseudoconvexity there are $S \in C^{\infty} (Ω)$ strictly plurisubharmonic and regular values $c_{k} ↑ + \infty$ such that, with $Ω_{k} : = {S < c_{k}}$ , every $\partial Ω_{k}$ is a nonempty $C^{\infty}$ hypersurface of $Ω$ , $\overline{Ω_{k}} \subseteq Ω_{k + 1}$ and $⋃_{k} Ω_{k} = Ω$ , so every $\overline{Ω_{k}}$ is a compact subset of $Ω$ ; by the dictionary [F16] the extreme-value criterion [F15] applies to the nonempty compact set $\overline{Ω_{1}}$ and the continuous function $S$ , so $μ : = \min_{\overline{Ω_{1}}} S$ is attained and finite; if $z \in Ω ∖ \overline{Ω_{1}}$ then $S (z) < c_{1}$ would give $z \in Ω_{1} \subseteq \overline{Ω_{1}}$ , so $S (z) \geq c_{1}$ , while $μ \leq c_{1}$ because $\partial Ω_{1} \subseteq \overline{Ω_{1}}$ is nonempty with $S = c_{1}$ there; hence $S \geq μ$ on $Ω$ .

1.2F3F24F25F26F31algebra

For $a \in Ω$ put $H (a) : = (\partial^{2} S / \partial z_{j} \partial {\overset{ˉ}{z}}_{k} (a))$ ; since $S$ is real-valued with commuting mixed second partials [F31], $H (a)$ is Hermitian, hence self-adjoint, so by [F24] it has an orthonormal eigenbasis with real eigenvalues $λ_{1} (a) \leq \dots \leq λ_{n} (a)$ , and expansion in that basis gives $λ_{1} (a) = \min_{∥ v ∥ = 1} ⟨ H (a) v, v ⟩ = \min_{∥ v ∥ = 1} L_{S} (a; v)$ ; strict plurisubharmonicity makes $λ_{1} (a) > 0$ [F3], so $\det H (a) = λ_{1} (a) \dots λ_{n} (a) > 0$ and $tr H (a) = λ_{1} (a) + \dots + λ_{n} (a) \geq λ_{1} (a)$ by [F25] and [F26], and since $0 < λ_{j} (a) \leq tr H (a)$ for every $j$ , one has $λ_{1} (a) \geq \det H (a) / (tr H (a))^{n - 1}$ ; the functions $\det H$ and $tr H$ are continuous on $Ω$ because the entries $S_{j \overset{ˉ}{k}}$ are, so $g : = \det H / (tr H)^{n - 1}$ is a continuous positive function on $Ω$ with $λ_{1} (a) \geq g (a) > 0$ for all $a \in Ω$ .

1.3F10F11

Let $χ$ be the standard smooth step function [F10]; its defining formula is $χ (t) = β (t) / (β (t) + β (1 - t))$ with $β$ the standard flat function, and the flat function vanishes on $(- \infty, 0]$ and is positive on $(0, \infty)$ [F11], so $χ \in C^{\infty} (R)$ with $0 \leq χ \leq 1$ on all of $R$ , $χ = 0$ on $(- \infty, 0]$ and $χ = 1$ on $[1, \infty)$ .

1.4F7F8given

Claim 2 is the instance of [F7] claim 1 with the given strictly plurisubharmonic $φ \in C^{2}$ , the given $f \in Dom {\overset{ˉ}{\partial}}_{q}$ with ${\overset{ˉ}{\partial}}_{q} f = 0$ and $E (f) < + \infty$ : it yields $u \in Dom {\overset{ˉ}{\partial}}_{q - 1}$ with ${\overset{ˉ}{\partial}}_{q - 1} u = f$ and $∥ u ∥_{φ}^{2} \leq E (f)$ , which is exactly the assertion of claim 2.

2.1F2F3step 1.1algebra

Put $S_{1} : = S + (1 - μ)$ . Then $S_{1} \in C^{\infty} (Ω)$ , $S_{1} \geq 1$ on $Ω$ , the complex Hessian of $S_{1}$ equals that of $S$ , and adding the constant changes neither the Levi form nor strict plurisubharmonicity [F3], so $S_{1}$ is strictly plurisubharmonic; every sublevel set ${S_{1} \leq t} = {S \leq t - 1 + μ}$ is closed in $Ω$ and contained in ${S < c_{k}}$ for every $k$ with $c_{k} > t - 1 + μ$ , hence is compactly contained in $Ω$ by [F2].

2.2F10F12step 1.3

Define $κ (t) : = \int_{0}^{t} χ (s) d s$ for $t \in R$ . By [F12] the function $κ$ is a primitive of the continuous function $χ$ on $R$ , hence is differentiable with $κ^{'} = χ$ ; since $χ \in C^{\infty}$ (step 1.3), $κ \in C^{\infty}$ as well.

3.1F18step 2.1

For every integer $j \geq 2$ put $A_{j} : = {j - 1 \leq S_{1} < j}$ . Each $A_{j}$ is a Borel subset of $Ω$ , being the preimage under the continuous $S_{1}$ of a Borel subset of $R$ [F18]; the $A_{j}$ are pairwise disjoint and $⋃_{j \geq 2} A_{j} = Ω$ because $S_{1} \geq 1$ on $Ω$ by step 2.1, so the indicator functions $1_{A_{j}}$ sum pointwise to $1_{Ω}$ .

3.2F12F13F14step 1.3step 2.2

One has $κ (0) = 0$ and $κ = 0$ on $(- \infty, 0]$ because $χ$ vanishes there (step 1.3); $κ \geq 0$ on $[0, \infty)$ because $χ \geq 0$ : for every partition of $[0, t]$ all lower and upper Darboux sums of $χ$ are $\geq$ those of the zero function, so the integral is $\geq 0$ by the definition of the Darboux integral [F13, F14]; and for $t \geq 1$ additivity over subintervals gives $κ (t) = \int_{0}^{1} χ + \int_{1}^{t} χ \geq \int_{1}^{t} χ = \int_{1}^{t} 1 = t - 1$ , the last equality because $u \mapsto u$ is a primitive of the constant function $1$ and $\int_{1}^{t} 1 = [u]_{1}^{t} = t - 1$ by the evaluation clause of [F12], while the first summand is $\geq 0$ .

4.1F15F16F17F19F20step 1.2step 3.1

The function $\tilde{H} : = ∣ η ∣^{2} / g$ is continuous and nonnegative on $Ω$ by step 1.2, and for every $j \geq 2$ one has $\int_{A_{j}} \tilde{H} d V \leq θ_{j}$ for a finite number $θ_{j} \geq 0$ : if $A_{j} = \emptyset$ take $θ_{j} : = 0$ ; otherwise $\overline{A_{j}} \subseteq {S_{1} \leq j}$ is a nonempty compact subset of $Ω$ by step 2.1, so by [F16] and [F15] the continuous function $1 + \tilde{H}$ attains on it a finite maximum $M_{j} : = \max_{\overline{A_{j}}} (1 + \tilde{H})$ , while $λ (\overline{A_{j}}) < + \infty$ because $\overline{A_{j}}$ is bounded and Lebesgue measurable [F15, F17]; then $M_{j} λ (\overline{A_{j}}) < + \infty$ and with $θ_{j} : = M_{j} (1 + λ (\overline{A_{j}}))$ one gets $\int_{A_{j}} \tilde{H} d V \leq \int_{\overline{A_{j}}} (1 + \tilde{H}) d V \leq \int_{\overline{A_{j}}} M_{j} d V = M_{j} λ (\overline{A_{j}}) \leq θ_{j}$ by monotonicity of the nonnegative integral [F19] and the simple-integral formula $\int c χ_{E} d μ = c μ (E)$ [F20].

4.2F12F13F14step 3.2

Define $β (t) : = \int_{0}^{t} κ (s) d s$ . Then $β$ is a primitive of the continuous $κ$ [F12], so $β \in C^{\infty}$ with $β^{'} = κ$ and $β^{''} = κ^{'} = χ$ by step 2.2; $β = 0$ on $(- \infty, 0]$ since $κ$ vanishes there, and $β \geq 0$ on $[0, \infty)$ by monotonicity of the integral and $κ \geq 0$ (step 3.2); finally $β (2) = \int_{0}^{2} κ \geq \int_{3 / 2}^{2} κ \geq \int_{3 / 2}^{2} \frac{1}{2} d s = \frac{1}{2} (2 - \frac{3}{2}) = \frac{1}{4}$ , using $κ (s) \geq s - 1 \geq \frac{1}{2}$ for $s \geq \frac{3}{2}$ (step 3.2), additivity and monotonicity of the integral [F13, F14], and the primitive evaluation [F12].

5.1F28F29F30step 4.1step 4.2

With the numbers $θ_{j} \geq 0$ of step 4.1 define $d_{i} : = i + \log (1 + θ_{i + 1})$ for $i \geq 1$ , $C_{0} : = \max (1, d_{1}, d_{2}) \geq 1$ , $a_{i} : = \max (0, 4 (d_{i + 2} - C_{0} (i + 2))) \geq 0$ for $i \geq 1$ , and $F (t) : = C_{0} t + \sum_{i = 1}^{\infty} a_{i} β (t - i)$ for $t \in R$ . At each $t$ only the finitely many indices with $i \leq t$ contribute a nonzero term because $β (t - i) = 0$ for $t - i \leq 0$ (step 4.2), so near $t$ the function $F$ agrees with a finite sum of $C^{\infty}$ functions and is $C^{\infty}$ by the algebra and locality properties of smooth maps [F28, F29]; differentiating that finite sum termwise by the chain rule [F30] gives $F^{'} (t) = C_{0} + \sum_{i \leq t} a_{i} κ (t - i)$ and $F^{''} (t) = \sum_{i \leq t} a_{i} χ (t - i)$ .

6.1F12F13F14step 1.3step 3.2step 4.2step 5.1

By step 5.1 and steps 1.3, 3.2, 4.2 the coefficients are nonnegative and $κ \geq 0$ , $χ \geq 0$ , so $F^{'} (t) \geq C_{0} \geq 1$ and $F^{''} (t) \geq 0$ for every $t$ ; $F (0) = 0$ ; and since $F$ is a primitive of the continuous $F^{'}$ , the evaluation clause of [F12] gives $F (t) - F (s) = \int_{s}^{t} F^{'} \geq t - s > 0$ for $s < t$ , so $F$ is strictly increasing, and $F (t) \geq F (0) + t = t \geq 0$ for $t \geq 0$ ; moreover for $j \geq 3$ one has $F (j) = C_{0} j + \sum_{i \leq j} a_{i} β (j - i) \geq C_{0} j + a_{j - 2} β (2) \geq C_{0} j + a_{j - 2} / 4 \geq d_{j}$ by step 4.2 and the definition of $a_{j - 2}$ , while $F (1) \geq C_{0} \geq d_{1}$ and $F (2) \geq 2 C_{0} \geq d_{2}$ because $C_{0} \geq d_{1}, d_{2}$ ; hence $F (j) \geq d_{j}$ for every integer $j \geq 1$ .

7.1F4F5F12F27step 2.1step 6.1

Let $i d (t) : = t$ and put $ψ : = (F - i d) \circ S_{1}$ on $Ω$ . On $R$ one has $(F - i d)^{'} = F^{'} - 1 \geq 0$ and $(F - i d)^{''} = F^{''} \geq 0$ by step 6.1, so $F - i d$ is convex by [F27] and nondecreasing because $(F - i d) (t) - (F - i d) (s) = \int_{s}^{t} (F^{'} - 1) \geq 0$ for $s < t$ by [F12] and $F^{'} \geq 1$ ; the function $S_{1}$ is real-valued with $L_{S_{1}} (a; v) > 0$ for $v \neq 0$ by step 2.1, hence $L_{S_{1}} \geq 0$ everywhere on the real vector space $C^{n}$ , and the $C^{2}$ Levi criterion [F4] makes $S_{1}$ plurisubharmonic on $Ω$ ; therefore the composition $ψ = (F - i d) \circ S_{1}$ is plurisubharmonic on $Ω$ by [F5].

8.1F3F4F28F30step 2.1step 7.1

Put $Φ : = F \circ S_{1} = S_{1} + ψ$ . Then $Φ \in C^{\infty} (Ω)$ by the chain rule and the algebra of smooth maps [F28, F30], and for every $a \in Ω$ and $v \in C^{n}$ the Levi form is additive, $L_{Φ} (a; v) = L_{S_{1}} (a; v) + L_{ψ} (a; v) \geq L_{S_{1}} (a; v) > 0$ : the middle inequality holds because $ψ \in C^{2}$ is plurisubharmonic, so $L_{ψ} \geq 0$ by the $C^{2}$ Levi criterion [F4], while $L_{S_{1}} (a; v) > 0$ for $v \neq 0$ by step 2.1 and [F3]; hence $Φ$ is strictly plurisubharmonic on $Ω$ and $Φ \in C^{\infty}$ .

9.1F24step 2.1step 1.2step 8.1algebra

Let $H_{Φ} : = (\partial^{2} Φ / \partial z_{j} \partial {\overset{ˉ}{z}}_{k})$ and let $w_{Φ}$ be the sum of its $q$ smallest eigenvalues. By steps 8.1 and 1.2 and the Rayleigh characterization recorded in step 1.2, $λ_{1} (H_{Φ}) (a) = \min_{∥ v ∥ = 1} L_{Φ} (a; v) \geq \min_{∥ v ∥ = 1} L_{S_{1}} (a; v) = λ_{1} (H_{S_{1}}) (a) = λ_{1} (H) (a) \geq g (a) > 0$ , the last equality because $S_{1}$ and $S$ have the same complex Hessian (step 2.1) and the last inequality by step 1.2; hence $w_{Φ} (a) \geq λ_{1} (H_{Φ}) (a) \geq g (a) > 0$ on $Ω$ .

10.1F18F19F21F22F23step 3.1step 4.1step 5.1step 6.1step 9.1

The function $a \mapsto \tilde{H} (a) e^{- Φ (a)}$ is continuous, hence Borel measurable, on $Ω$ [F18]; since the $A_{j}$ partition $Ω$ (step 3.1), Beppo Levi's theorem [F21] gives $\int_{Ω} \tilde{H} e^{- Φ} d V = \sum_{j \geq 2} \int_{A_{j}} \tilde{H} e^{- Φ} d V$ ; on $A_{j}$ one has $S_{1} \geq j - 1$ , hence $Φ = F (S_{1}) \geq F (j - 1)$ because $F$ is strictly increasing (step 6.1), and $\int_{A_{j}} \tilde{H} d V \leq θ_{j}$ (step 4.1), so the scalar rule and monotonicity [F19] give $\int_{A_{j}} \tilde{H} e^{- Φ} d V \leq θ_{j} e^{- F (j - 1)} \leq θ_{j} (1 + θ_{j})^{- 1} e^{- (j - 1)} \leq e^{- (j - 1)}$ , the middle inequality because $F (j - 1) \geq d_{j - 1} = (j - 1) + \log (1 + θ_{j})$ (steps 5.1 and 6.1); the series $\sum_{j \geq 2} e^{- (j - 1)} = \sum_{k \geq 1} (e^{- 1})^{k}$ converges by the ratio test [F22] since $e^{- 1} < 1$ by strict increase of the exponential [F23]; therefore the energy $E_{Φ} (η) : = \int_{Ω} ∣ η ∣^{2} w_{Φ}^{- 1} e^{- Φ} d V$ of $η$ with respect to $Φ$ satisfies $E_{Φ} (η) \leq \int_{Ω} \tilde{H} e^{- Φ} d V < + \infty$ by step 9.1.

11.1F6F7step 8.1step 10.1

Since $η$ is a smooth $\overset{ˉ}{\partial}$ -closed $(0, q)$ -form and $Φ \in C^{\infty} (Ω; R)$ is strictly plurisubharmonic with $E_{Φ} (η) < + \infty$ (steps 8.1 and 10.1), the $C^{\infty}$ branch of the Hörmander theorem [F7] (claim 2) supplies $ζ \in C^{\infty} (Ω; Λ^{0, q - 1})$ with $\overset{ˉ}{\partial} ζ = η$ ; thus $η \in B_{\overset{ˉ}{\partial}}^{0, q} (Ω)$ , its class in $H_{\overset{ˉ}{\partial}}^{0, q} (Ω) = Z_{\overset{ˉ}{\partial}}^{0, q} (Ω) / B_{\overset{ˉ}{\partial}}^{0, q} (Ω)$ is zero by [F6], and since $η$ was an arbitrary smooth $\overset{ˉ}{\partial}$ -closed $(0, q)$ -form one has $H_{\overset{ˉ}{\partial}}^{0, q} (Ω) = 0$ .

12.1F7F17F18F32step 11.1step 1.4∎

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 $Φ = F \circ S_{1}$ produced in step 8.1 is smooth and strictly plurisubharmonic with no boundary regularity claimed.

Depends on

Used by

First Cousin problem on a pseudoconvex domain Corollary

Dependency tree · two levels

211 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jean-Pierre Demailly, Complex Analytic and Differential Geometry (standard reference, not scraped)
Mohammad Jabbari, Several Complex Variables course notes (standard reference, not scraped)
Jiří Lebl, Tasty Bits of Several Complex Variables (standard reference, not scraped)