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

How statement and proof provenance work

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

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

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

Weighted Morrey–Kohn estimate with a pseudoconvex boundary term

Statement

Assume the Axiom of Choice (AC). Let $n \geq 1$ , and use $z_{j}$ for the canonical coordinate $z_{j - 1}$ , $1 \leq j \leq n$ , with the same relabeling for derivatives and form coefficients. Let $D \subseteq C^{n}$ be a bounded domain with $C^{\infty}$ boundary, let $ρ \in C^{\infty} (\overline{D}; R)$ be a defining function with $D = {z \in \overline{D} : ρ (z) < 0}$ and $∣ \nabla ρ ∣ = 1$ on $\partial D$ , let $φ \in C^{2} (\overline{D}; R)$ , let $1 \leq q \leq n$ , and let $u \in C^{\infty} (\overline{D}; Λ^{0, q})$ 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 $u_{j K}$ is the antisymmetric coefficient of $u$ on the tuple $(j, K)$ and $d S$ denotes $(2 n - 1)$ -dimensional surface measure on $\partial D$ . Then:

$u \in Dom {\overset{ˉ}{\partial}}_{φ}^{*}$ , and the exact identity $∥ \overset{ˉ}{\partial} u ∥_{φ}^{2} + ∥ {\overset{ˉ}{\partial}}_{φ}^{*} u ∥_{φ}^{2} = \sum_{∣ J ∣ = q} \sum_{k = 1}^{n} \int_{D} ∣ D_{k} u_{J} ∣^{2} e^{- φ} d V + \int_{D} \sum_{∣ K ∣ = q - 1} \sum_{j, k = 1}^{n} φ_{j \overset{ˉ}{k}} u_{j K} \overline{u_{k K}} e^{- φ} d V + \int_{\partial D} \sum_{∣ K ∣ = q - 1} \sum_{j, k = 1}^{n} ρ_{j \overset{ˉ}{k}} u_{j K} \overline{u_{k K}} e^{- φ} d S$ holds, with $D_{k} = \partial_{{\overset{ˉ}{z}}_{k}}$ and $ρ_{j \overset{ˉ}{k}} = \partial_{z_{j}} \partial_{{\overset{ˉ}{z}}_{k}} ρ$ .
If $D$ is Levi pseudoconvex, the boundary term is nonnegative and therefore $\int_{D} \sum_{∣ K ∣ = q - 1} \sum_{j, k = 1}^{n} φ_{j \overset{ˉ}{k}} u_{j K} \overline{u_{k K}} e^{- φ} d V \leq ∥ \overset{ˉ}{\partial} u ∥_{φ}^{2} + ∥ {\overset{ˉ}{\partial}}_{φ}^{*} u ∥_{φ}^{2} .$
If $D$ is Levi pseudoconvex and $λ_{1} (a) \leq \dots \leq λ_{n} (a)$ denote the eigenvalues of the Hermitian matrix $(φ_{j \overset{ˉ}{k}} (a))$ , then $\int_{D} (λ_{1} + \dots + λ_{q}) ∣ u ∣^{2} e^{- φ} d V \leq ∥ \overset{ˉ}{\partial} u ∥_{φ}^{2} + ∥ {\overset{ˉ}{\partial}}_{φ}^{*} u ∥_{φ}^{2} .$
If $D$ is Levi pseudoconvex, the inequality of claim 3 holds for every $u \in Dom {\overset{ˉ}{\partial}}_{q} \cap Dom {\overset{ˉ}{\partial}}_{φ}^{*}$ .

Facts & Assumptions

Given: The Axiom of Choice; a bounded domain $D \subseteq C^{n}$ with $C^{\infty}$ boundary; a defining function $ρ$ normalized by $∣ \nabla ρ ∣ = 1$ on $\partial D$ ; a weight $φ \in C^{2} (\overline{D}; R)$ ; an integer $1 \leq q \leq n$ ; and a form $u \in C^{\infty} (\overline{D}; Λ^{0, q})$ satisfying (BC); the conventions $ε_{j} v : = d {\overset{ˉ}{z}}_{j} \land v$ and $(ι_{j} v)_{K} : = v_{j K}$ on coefficient tensors, $D_{j} : = \partial_{{\overset{ˉ}{z}}_{j}}$ and $δ_{j} : = φ_{j} - \partial_{z_{j}}$ acting coefficientwise, and ${\overset{ˉ}{\partial}}_{0}^{*}$ for the unweighted Hilbert adjoint of $\overset{ˉ}{\partial}$ (the case $φ \equiv 0$ of the operators of [F1]), whose formal density on its smooth domain is $- \sum_{j} ι_{j} \partial_{z_{j}}$ .

[F1]

The weighted space, its pairing $⟨ v, w ⟩_{φ} = \int_{D} \sum_{∣ J ∣ = q} v_{J} \overline{w_{J}} e^{- φ} d V$ , the maximal distributional $\overset{ˉ}{\partial}$ , and the weighted Hilbert adjoint ${\overset{ˉ}{\partial}}_{φ}^{*}$ with its formal density $({\overset{ˉ}{\partial}}_{φ}^{*} v)_{K} = \sum_{j} (v_{j K} φ_{j} - \partial_{z_{j}} v_{j K})$ on its domain are as in Weighted L2 spaces and maximal dbar operators; coefficients are extended to non-increasing tuples by antisymmetry, so $v_{j K} = 0$ when $j \in K$ .

[F2]

For every $ψ \in C_{c}^{\infty} (D)$ of bidegree $(0, q)$ one has $ψ \in Dom {\overset{ˉ}{\partial}}_{φ}^{*}$ (The maximal distributional dbar operator is closed and densely defined).

[F3]

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

[F4]

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

[F5]

A domain with $C^{2}$ boundary is Levi pseudoconvex when for every $p \in \partial D$ there are a neighbourhood $U$ of $p$ and $ρ \in C^{2} (U, R)$ with $D \cap U = {ρ < 0}$ , $d ρ (p) \neq 0$ , and $L_{ρ} (p; v) \geq 0$ for every $v \in C^{n}$ with $\sum_{j} \frac{\partial ρ}{\partial z_{j}} (p) v_{j} = 0$ (Levi pseudoconvex domains).

[F6]

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

[F7]

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

[F8]

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

[F9]

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

[F10]

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

[F11]

(Boas, §3.3.3, printed pp. 81-84: formulas (3.3)-(3.4), Exercise 38.) For smooth scalar functions $F, G$ on $\overline{D}$ the divergence theorem stated in the given block gives the two weighted integrations by parts $\int_{D} (\partial_{z_{j}} F) \overline{G} e^{- φ} d V = \int_{\partial D} F \overline{G} ρ_{z_{j}} e^{- φ} d S - \int_{D} F \overline{\partial_{{\overset{ˉ}{z}}_{j}} G} e^{- φ} d V + \int_{D} F \overline{G} φ_{j} e^{- φ} d V$ and $\int_{D} (\partial_{{\overset{ˉ}{z}}_{j}} F) \overline{G} e^{- φ} d V = \int_{\partial D} F \overline{G} ρ_{{\overset{ˉ}{z}}_{j}} e^{- φ} d S - \int_{D} F \overline{\partial_{z_{j}} G} e^{- φ} d V + \int_{D} F \overline{G} φ_{\overset{ˉ}{j}} e^{- φ} d V$ , where $ρ_{z_{j}} = \partial_{z_{j}} ρ$ , $ρ_{{\overset{ˉ}{z}}_{j}} = \partial_{{\overset{ˉ}{z}}_{j}} ρ$ , $φ_{j} = \partial_{z_{j}} φ$ and $φ_{\overset{ˉ}{j}} = \partial_{{\overset{ˉ}{z}}_{j}} φ$ ; Boas's (3.3) is the $q = 1$ 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 $e^{- φ}$ , which is where the factors $φ_{j}, φ_{\overset{ˉ}{j}}$ come from.

[F12]

(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 $C^{k + 1}$ boundary, $C_{(0, q)}^{k} (\overline{D}) \cap Dom {\overset{ˉ}{\partial}}_{0}^{*}$ is dense in $Dom {\overset{ˉ}{\partial}}_{q} \cap Dom {\overset{ˉ}{\partial}}_{0}^{*}$ for the unweighted graph norm $(∥ v ∥_{0}^{2} + ∥ \overset{ˉ}{\partial} v ∥_{0}^{2} + ∥ {\overset{ˉ}{\partial}}_{0}^{*} v ∥_{0}^{2})^{1 / 2}$ ; this also holds with $k = \infty$ . For a $C^{k}$ form, $k \geq 1$ , membership in $Dom {\overset{ˉ}{\partial}}_{0}^{*}$ is equivalent to (BC), and on this domain its value is $- \sum_{j} ι_{j} \partial_{z_{j}} v$ . 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 $H \in C^{1} (\overline{D})$ , the divergence theorem gives $\int_{D} \partial_{z_{j}} H d V = \int_{\partial D} H ρ_{z_{j}} d S$ ; its conjugate gives the $\partial_{{\overset{ˉ}{z}}_{j}}$ formula. Applying these to $H = F \overline{G} e^{- φ}$ gives [F11], including for $C^{1}$ factors. In Boas, §3.3.3, printed p. 83, the unweighted calculation for a smooth $(0, 1)$ -form $f$ is $⟨ f, \overset{ˉ}{\partial} η ⟩_{0} = \int_{D} \sum_{j} f_{j} \overline{\partial_{{\overset{ˉ}{z}}_{j}} η} d V = - \int_{D} \sum_{j} \partial_{z_{j}} f_{j} \overline{η} d V + \int_{\partial D} \sum_{j} f_{j} ρ_{z_{j}} \overline{η} d S .$ 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 $C^{2}$ 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 ${A C}_{ω}$ 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

technique · direct

1.1F1F7F8givenalgebra

Since $\partial D$ is $C^{\infty}$ and $∣ \nabla ρ ∣ = 1$ there, $\overline{D}$ is compact, so $φ, \nabla φ$ and the coefficients $φ_{j \overset{ˉ}{k}}$ are bounded on $\overline{D}$ ; put $M : = \max_{j, k} \sup_{\overline{D}} ∣ φ_{j \overset{ˉ}{k}} ∣ < \infty$ . The Hermitian matrix $H (a) : = (φ_{j \overset{ˉ}{k}} (a))$ is well defined at every $a \in \overline{D}$ , its eigenvalues $λ_{1} (a) \leq \dots \leq λ_{n} (a)$ are real by [F8], and if $v$ is a unit eigenvector for $λ_{i} (a)$ then the Cauchy-Schwarz inequality gives $∣ λ_{i} (a) ∣ = ∣ ⟨ H (a) v, v ⟩ ∣ \leq \max_{j, k} ∣ φ_{j \overset{ˉ}{k}} (a) ∣ (\sum_{j} ∣ v_{j} ∣)^{2} \leq n \max_{j, k} ∣ φ_{j \overset{ˉ}{k}} (a) ∣ \leq n M$ , so the sum $w : = λ_{1} + \dots + λ_{q}$ satisfies $∣ w ∣ \leq q n M$ at every point of $\overline{D}$ ; also $φ_{\overset{ˉ}{j}} = \overline{φ_{j}}$ because $φ$ is real-valued.

1.2F1givenalgebra

Transport identity. A $(0, k)$ -form $z$ lies in $Dom {\overset{ˉ}{\partial}}_{φ}^{*}$ exactly when $e^{- φ} z$ lies in $Dom {\overset{ˉ}{\partial}}_{0}^{*}$ , and then ${\overset{ˉ}{\partial}}_{φ}^{*} z = e^{φ} {\overset{ˉ}{\partial}}_{0}^{*} (e^{- φ} z) .$ Indeed $⟨ \overset{ˉ}{\partial} h, z ⟩_{φ} = ⟨ \overset{ˉ}{\partial} h, e^{- φ} z ⟩_{0}$ and $⟨ h, z^{*} ⟩_{φ} = ⟨ h, e^{- φ} z^{*} ⟩_{0}$ for every $h$ in the maximal domain. The weighted and unweighted graph domains of $\overset{ˉ}{\partial}$ agree as sets, since $e^{\pm φ}$ are bounded on $\overline{D}$ ; hence the two bounded-functional criteria are equivalent and their Riesz vectors have the displayed relation.

2.1F1F12step 1.2givenalgebra

The form $u$ lies in $Dom {\overset{ˉ}{\partial}}_{φ}^{*}$ and ${\overset{ˉ}{\partial}}_{φ}^{*} u = \sum_{j} ι_{j} δ_{j} u$ : the positive factor $e^{- φ}$ preserves (BC), so [F12], applied with $k = 2$ since $e^{- φ} u$ is $C^{2}$ , gives $e^{- φ} u \in Dom {\overset{ˉ}{\partial}}_{0}^{*}$ and ${\overset{ˉ}{\partial}}_{0}^{*} (e^{- φ} u) = - \sum_{j} ι_{j} \partial_{z_{j}} (e^{- φ} u) = e^{- φ} \sum_{j} ι_{j} (φ_{j} - \partial_{z_{j}}) u .$ The transport identity of step 1.2 gives the claimed weighted adjoint and formula.

3.1F1F3F6F7step 2.1givenalgebra

On smooth coefficient tensors the following operator identities hold: (a) $\overset{ˉ}{\partial} = \sum_{j} ε_{j} D_{j}$ and ${\overset{ˉ}{\partial}}_{φ}^{*} = \sum_{j} ι_{j} δ_{j}$ on $Dom {\overset{ˉ}{\partial}}_{φ}^{*}$ ; (b) $ι_{j} ε_{k} + ε_{k} ι_{j} = δ_{j k} i d$ ; (c) $ι_{j} \overset{ˉ}{\partial} = D_{j} - \overset{ˉ}{\partial} ι_{j}$ ; (d) $[D_{k}, δ_{j}] = φ_{j \overset{ˉ}{k}}$ ; (e) ${\overset{ˉ}{\partial}}_{φ}^{*} \overset{ˉ}{\partial} + \overset{ˉ}{\partial} {\overset{ˉ}{\partial}}_{φ}^{*} = \sum_{j} δ_{j} D_{j} + \sum_{j, k} φ_{j \overset{ˉ}{k}} ε_{k} ι_{j}$ ; and (f) $⟨ ε_{j} f, g ⟩_{φ} = ⟨ f, ι_{j} g ⟩_{φ}$ for coefficient tensors $f, g$ 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 $ι_{j} \overset{ˉ}{\partial} = \sum_{k} (δ_{j k} - ε_{k} ι_{j}) D_{k} = D_{j} - \overset{ˉ}{\partial} ι_{j}$ ; (d) is $D_{k} φ_{j} = φ_{j \overset{ˉ}{k}}$ by [F6]; (e) follows from (a)-(d) by writing ${\overset{ˉ}{\partial}}_{φ}^{*} \overset{ˉ}{\partial} + \overset{ˉ}{\partial} {\overset{ˉ}{\partial}}_{φ}^{*} = \sum_{j, k} (ι_{j} δ_{j} ε_{k} D_{k} + ε_{k} D_{k} ι_{j} δ_{j})$ and substituting (b), (c) and (d); and (f) is the pointwise adjointness of wedge and contraction.

4.1F1F3F8step 3.1givenalgebra

For every $a \in \overline{D}$ and every coefficient tensor $(u_{J})_{∣ J ∣ = q}$ one has $\sum_{∣ K ∣ = q - 1} \sum_{j, k} φ_{j \overset{ˉ}{k}} (a) u_{j K} \overline{u_{k K}} \geq (λ_{1} + \dots + λ_{q}) (a) \sum_{∣ J ∣ = q} ∣ u_{J} ∣^{2}$ : the Hermitian matrix $H (a)$ is self-adjoint and hence normal, so [F8] gives an orthonormal basis $v_{1}, \dots, v_{n}$ of $C^{n}$ with $H (a) v_{i} = λ_{i} v_{i}$ and $φ_{j \overset{ˉ}{k}} (a) = \sum_{i} λ_{i} v_{i j} \overline{v_{i k}}$ ; putting $w_{i K} : = \sum_{j} v_{i j} u_{j K}$ and $d_{i} : = \sum_{∣ K ∣ = q - 1} ∣ w_{i K} ∣^{2}$ gives $\sum_{∣ K ∣ = q - 1} \sum_{j, k} φ_{j \overset{ˉ}{k}} u_{j K} \overline{u_{k K}} = \sum_{i} λ_{i} d_{i}$ ; Parseval in each fiber $K$ gives $\sum_{i} d_{i} = \sum_{∣ K ∣ = q - 1} \sum_{j} ∣ u_{j K} ∣^{2} = q \sum_{∣ J ∣ = q} ∣ u_{J} ∣^{2}$ , and $0 \leq d_{i} \leq \sum_{∣ J ∣ = q} ∣ u_{J} ∣^{2}$ because $d_{i} = ∣ ν_{i} u ∣^{2}$ where $ν_{i} : = \sum_{j} v_{i j} ι_{j}$ is the adjoint, by (f) of step 3.1, of $μ_{i} : = \sum_{j} \overline{v_{i j}} ε_{j}$ and $∣ ν_{i} u ∣^{2} + ∣ μ_{i} u ∣^{2} = ∣ u ∣^{2}$ by (b) and (f) of step 3.1, using $\sum_{j} ∣ v_{i j} ∣^{2} = 1$ ; finally, for real $λ_{1} \leq \dots \leq λ_{n}$ and reals $0 \leq d_{i} \leq U$ with $\sum_{i} d_{i} = q U$ one has $\sum_{i} λ_{i} d_{i} \geq (λ_{1} + \dots + λ_{q}) U$ , because an exchange of mass between indices $i > q$ and $j \leq q$ never increases $\sum_{i} λ_{i} d_{i}$ and repeated exchange reaches $d_{1} = \dots = d_{q} = U$ , $d_{q + 1} = \dots = d_{n} = 0$ .

4.2F1F9F11step 2.1step 3.1givenalgebra

The left-hand side of claim 1 equals $⟨ □ u, u ⟩_{φ} + B_{1}$ , where $□ : = \sum_{j} δ_{j} D_{j} + \sum_{j, k} φ_{j \overset{ˉ}{k}} ε_{k} ι_{j}$ and $B_{1} : = \int_{\partial D} \sum_{∣ K ∣ = q} \sum_{j} (\overset{ˉ}{\partial} u)_{j K} \overline{u_{K}} ρ_{z_{j}} e^{- φ} d S$ , with $(\overset{ˉ}{\partial} u)_{j K}$ the coefficient of the $(0, q + 1)$ -form $\overset{ˉ}{\partial} u$ on the ordered tuple $(j, K)$ : by step 2.1 and identity (e) of step 3.1, $⟨ □ u, u ⟩_{φ} = ⟨ {\overset{ˉ}{\partial}}_{φ}^{*} \overset{ˉ}{\partial} u, u ⟩_{φ} + ⟨ \overset{ˉ}{\partial} {\overset{ˉ}{\partial}}_{φ}^{*} u, u ⟩_{φ}$ computed as formal densities, the integration by parts for $\partial_{z_{j}}$ in [F11] with $F : = (\overset{ˉ}{\partial} u)_{j K}$ , $G : = u_{K}$ gives $⟨ {\overset{ˉ}{\partial}}_{φ}^{*} \overset{ˉ}{\partial} u, u ⟩_{φ} = ∥ \overset{ˉ}{\partial} u ∥_{φ}^{2} - B_{1}$ using the formal integration-by-parts expression (no Hilbert-adjoint domain claim is made for $\overset{ˉ}{\partial} u$ ), and $∥ \overset{ˉ}{\partial} u ∥_{φ}^{2} = \sum_{j} ⟨ D_{j} u, ι_{j} \overset{ˉ}{\partial} u ⟩_{φ}$ by (f) of step 3.1, while $⟨ \overset{ˉ}{\partial} {\overset{ˉ}{\partial}}_{φ}^{*} u, u ⟩_{φ} = ∥ {\overset{ˉ}{\partial}}_{φ}^{*} u ∥_{φ}^{2}$ by the adjoint relation applied to the $C^{1}$ form ${\overset{ˉ}{\partial}}_{φ}^{*} u$ , whose first derivatives are bounded and hence whose $\overset{ˉ}{\partial}$ is in $L^{2}$ , and the form $u \in Dom {\overset{ˉ}{\partial}}_{φ}^{*}$ ; adding gives the claim.

4.3F1F7F11step 3.1givenalgebra

The first summand is $\sum_{j} ⟨ δ_{j} D_{j} u, u ⟩_{φ} = \sum_{∣ J ∣ = q} \sum_{k} \int_{D} ∣ D_{k} u_{J} ∣^{2} e^{- φ} d V - R$ , where $R : = \int_{\partial D} \sum_{∣ J ∣ = q} \sum_{j} D_{j} u_{J} \overline{u_{J}} ρ_{z_{j}} e^{- φ} d S$ . Indeed apply the $\partial_{z_{j}}$ integration by parts of [F11] with $F = D_{j} u_{J}$ and $G = u_{J}$ . Since $δ_{j} = φ_{j} - \partial_{z_{j}}$ , the weight-derivative terms cancel and the remaining volume term is $\int_{D} (D_{j} u_{J}) \overline{\partial_{{\overset{ˉ}{z}}_{j}} u_{J}} e^{- φ} d V = \int_{D} ∣ D_{j} u_{J} ∣^{2} e^{- φ} d V$ ; the boundary term has the sign $- R$ .

4.4F1step 3.1givenalgebra

The second summand of $⟨ □ u, u ⟩_{φ}$ evaluates as $\sum_{j, k} ⟨ φ_{j \overset{ˉ}{k}} ε_{k} ι_{j} u, u ⟩_{φ} = \int_{D} \sum_{∣ K ∣ = q - 1} \sum_{j, k} φ_{j \overset{ˉ}{k}} u_{j K} \overline{u_{k K}} e^{- φ} d V$ : apply the adjointness (f) of step 3.1 pointwise, move the scalar $φ_{j \overset{ˉ}{k}}$ outside the pairing, and use the coefficient formula of [F1].

5.1F1F3F6F7F11step 3.1givenalgebra

At every boundary point $p \in \partial D$ one has the identity $\sum_{∣ K ∣ = q} \sum_{j = 1}^{n} [(\overset{ˉ}{\partial} u)_{j K} - D_{j} u_{K}] \overline{u_{K}} ρ_{z_{j}} = \sum_{∣ K ∣ = q - 1} \sum_{j, k = 1}^{n} ρ_{j \overset{ˉ}{k}} u_{j K} \overline{u_{k K}}$ , all quantities being evaluated at $p$ , where $(\overset{ˉ}{\partial} u)_{j K}$ denotes the coefficient of $\overset{ˉ}{\partial} u$ on the ordered tuple $(j, K)$ (so it equals $0$ when $j \in K$ ) and $u_{K}$ the coefficient of $u$ on the increasing tuple $K$ ; moreover $B_{1} - R = \int_{\partial D} \sum_{∣ K ∣ = q - 1} \sum_{j, k} ρ_{j \overset{ˉ}{k}} u_{j K} \overline{u_{k K}} e^{- φ} d S$ . Indeed, with $θ : = \sum_{j} ρ_{z_{j}} ι_{j}$ the left-hand side equals $⟨ (θ \overset{ˉ}{\partial} - \sum_{j} ρ_{z_{j}} D_{j}) u, u ⟩_{p t}$ by (f) and (a) of step 3.1, and since $θ \overset{ˉ}{\partial} = \sum_{j} ρ_{z_{j}} D_{j} - \overset{ˉ}{\partial} θ + \sum_{j, k} ρ_{j \overset{ˉ}{k}} ε_{k} ι_{j}$ by (b), (c) and [F6] (applied to $D_{k} ρ_{z_{j}} = ρ_{j \overset{ˉ}{k}}$ ), it equals $- ⟨ \overset{ˉ}{\partial} (θ u), u ⟩_{p t} + \sum_{j, k} ρ_{j \overset{ˉ}{k}} ⟨ ε_{k} ι_{j} u, u ⟩_{p t}$ ; the second term is $\sum_{∣ K ∣ = q - 1} \sum_{j, k} ρ_{j \overset{ˉ}{k}} u_{j K} \overline{u_{k K}}$ by (f) of step 3.1, and the first term vanishes because $- ⟨ \overset{ˉ}{\partial} (θ u), u ⟩_{p t} = - \sum_{k, K} D_{k} (θ u)_{K} \overline{u_{k K}} = - \sum_{j, k, K} (ρ_{j \overset{ˉ}{k}} u_{j K} + ρ_{z_{j}} D_{k} u_{j K}) \overline{u_{k K}}$ and for each $∣ K ∣ = q - 1$ the tangential operator $T_{K} : = \sum_{k} \overline{u_{k K}} (p) \partial_{{\overset{ˉ}{z}}_{k}}$ annihilates the restriction to $\partial D$ of $\sum_{j} u_{j K} ρ_{z_{j}}$ : it is tangential at $p$ because $\sum_{k} \overline{u_{k K}} (p) ρ_{{\overset{ˉ}{z}}_{k}} (p) = \overline{\sum_{k} u_{k K} (p) ρ_{z_{k}} (p)} = 0$ by (BC), and $\sum_{j} u_{j K} ρ_{z_{j}} = 0$ on $\partial D$ by (BC), so $0 = T_{K} (\sum_{j} u_{j K} ρ_{z_{j}}) (p) = \sum_{j, k} \overline{u_{k K}} (ρ_{j \overset{ˉ}{k}} u_{j K} + ρ_{z_{j}} D_{k} u_{j K}) (p)$ ; integrating the pointwise identity over $\partial D$ against $e^{- φ} d S$ and subtracting the definition of $R$ in step 4.3 from that of $B_{1}$ in step 4.2 gives the displayed identity for $B_{1} - R$ .

6.1step 2.1step 4.2step 4.3step 4.4step 5.1givenalgebra

Claim 1 holds: by steps 4.2, 4.3 and 4.4 the sum $∥ \overset{ˉ}{\partial} u ∥_{φ}^{2} + ∥ {\overset{ˉ}{\partial}}_{φ}^{*} u ∥_{φ}^{2}$ equals $\sum_{∣ J ∣ = q} \sum_{k} \int_{D} ∣ D_{k} u_{J} ∣^{2} e^{- φ} d V - R + \int_{D} \sum_{j, k, K} φ_{j \overset{ˉ}{k}} u_{j K} \overline{u_{k K}} e^{- φ} d V + B_{1}$ , and step 5.1 replaces $- R + B_{1}$ by $\int_{\partial D} \sum_{j, k, K} ρ_{j \overset{ˉ}{k}} u_{j K} \overline{u_{k K}} e^{- φ} d S$ , which is the stated identity; the membership $u \in Dom {\overset{ˉ}{\partial}}_{φ}^{*}$ is step 2.1.

7.1F4F5step 6.1givenalgebra

If $D$ is Levi pseudoconvex the boundary term of claim 1 is nonnegative: at $p \in \partial D$ and for each $K$ with $∣ K ∣ = q - 1$ the vector $v^{(K)} : = (u_{1 K}, \dots, u_{n K})$ satisfies $\sum_{j} v_{j}^{(K)} ρ_{z_{j}} (p) = 0$ by (BC), so $\sum_{j, k} ρ_{j \overset{ˉ}{k}} (p) u_{j K} \overline{u_{k K}} = L_{ρ} (p; v^{(K)}) \geq 0$ by [F5]: if $r$ is its local defining function at $p$ , local coordinates transverse to $\partial D$ give $ρ = h r$ with $h (p) > 0$ ; the product rule on vectors tangent to $r = 0$ gives $L_{ρ} (p; v) = h (p) L_{r} (p; v)$ , and the boundary integral of claim 1 is an integral of a pointwise nonnegative continuous function against the positive factor $e^{- φ}$ ; dropping it and the nonnegative first term of the identity of step 6.1 gives the estimate of claim 2.

8.1step 4.1step 7.1givenalgebra

Claim 3 holds: by step 4.1 the integrand $\sum_{∣ K ∣ = q - 1} \sum_{j, k} φ_{j \overset{ˉ}{k}} u_{j K} \overline{u_{k K}}$ dominates $(λ_{1} + \dots + λ_{q}) ∣ u ∣^{2}$ pointwise on $\overline{D}$ , and step 7.1 bounds the integral of the former by $∥ \overset{ˉ}{\partial} u ∥_{φ}^{2} + ∥ {\overset{ˉ}{\partial}}_{φ}^{*} u ∥_{φ}^{2}$ .

9.1F1F9F12step 1.1step 1.2step 8.1givenalgebra

Claim 4 holds. Let $u \in Dom {\overset{ˉ}{\partial}}_{q} \cap Dom {\overset{ˉ}{\partial}}_{φ}^{*}$ and put $v : = e^{- φ} u$ . By the transport identity of step 1.2, $v \in Dom {\overset{ˉ}{\partial}}_{0}^{*}$ ; the product rule gives $\overset{ˉ}{\partial} v = e^{- φ} (\overset{ˉ}{\partial} u - \overset{ˉ}{\partial} φ \land u) \in L^{2}$ , so $v \in Dom {\overset{ˉ}{\partial}}_{q}$ . The unweighted graph-norm density [F12] gives smooth $v_{ℓ}$ satisfying (BC) with $v_{ℓ} \to v$ , $\overset{ˉ}{\partial} v_{ℓ} \to \overset{ˉ}{\partial} v$ , and ${\overset{ˉ}{\partial}}_{0}^{*} v_{ℓ} \to {\overset{ˉ}{\partial}}_{0}^{*} v$ in unweighted $L^{2}$ . Put $u_{ℓ} : = e^{φ} v_{ℓ}$ . Then $u_{ℓ}$ satisfies (BC) and belongs to $C^{2} (\overline{D})$ , which suffices for the integrations by parts and boundary differentiations of steps 2.1–8.1. By step 1.2 and the product rule, ${\overset{ˉ}{\partial}}_{φ}^{*} u_{ℓ} = e^{φ} {\overset{ˉ}{\partial}}_{0}^{*} v_{ℓ}, \overset{ˉ}{\partial} u_{ℓ} = e^{φ} (\overset{ˉ}{\partial} v_{ℓ} + \overset{ˉ}{\partial} φ \land v_{ℓ}) .$ The bounded factors $e^{\pm φ}$ and $\overset{ˉ}{\partial} φ$ show that $u_{ℓ} \to u$ in the weighted graph norm. Apply the inequality of step 8.1 to $u_{ℓ}$ and pass to the limit: the right side converges by graph-norm convergence, and the left side converges because $∣ λ_{1} + \dots + λ_{q} ∣ \leq q n M$ by step 1.1 and $L^{2}$ convergence implies convergence of the squared norms against any bounded real weight. Thus the inequality holds for $u$ .

10.1F1F2F10F11F12step 1.2step 2.1step 6.1step 7.1step 8.1step 9.1∎

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

Depends on

Used by

Weighted ∂̄ solvability on a smoothly bounded pseudoconvex domain Lemma

Dependency tree · two levels

68 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

Harold P. Boas, Lecture Notes on Several Complex Variables (standard reference, not scraped)
Jean-Pierre Demailly, Complex Analytic and Differential Geometry (standard reference, not scraped)
Friedrich Haslinger, Complex analysis, the dbar-Neumann problem, and Schrodinger operators (author manuscript) (standard reference, not scraped)