Pipeline-generated

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.

✓ 6 results · all verified · 3 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Hörmander Estimates and the Levi Problem — Examples

1 · Prerequisites

2 · Summary

The examples record the computations that fix the conventions of the main page. The Levi form of the unit ball and the strict plurisubharmonic exhaustion of the convex ball show how the definitions of pseudoconvexity and strong plurisubharmonicity are verified in coordinates, while the Hartogs domain ${∣ w ∣^{2} e^{2 ∣ z ∣^{2}} < 1}$ exhibits a pseudoconvexity statement proved through an explicit exhaustion rather than a boundary expansion.

On the estimate side, the Gaussian-weight examples solve $\overset{ˉ}{\partial} u = f$ explicitly on $C$ and on $C^{n}$ , compute both weighted squared norms by polar coordinates and Gamma integrals, and show the $q = 1$ weighted bound with the reciprocal $w^{- 1}$ of the smallest Levi eigenvalue. The final example glues the two-chart first-Cousin data $m_{1} = 1 / z$ , $m_{2} = 0$ on $C$ with the explicit witness $G = 1 / z$ , exhibiting the local-quotient conventions on which the Cousin theorem is stated.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-10-02Open item page →

Hörmander estimate with a Gaussian weight

Statement

Assume the Axiom of Choice (AC). Let $n \geq 1$ and use one-based labels $z_{j} : = z_{j - 1}^{c a n}$ for $1 \leq j \leq n$ , also for derivatives and forms. On $C^{n}$ with the Gaussian weight $φ (z) : = ∣ z ∣^{2}$ the $(0, 1)$ -form $f : = d {\overset{ˉ}{z}}_{1}$ is $\overset{ˉ}{\partial}$ -closed and the function $u : = {\overset{ˉ}{z}}_{1}$ satisfies $\overset{ˉ}{\partial} u = f, ∥ u ∥_{φ}^{2} = π^{n} = E (f) = \int_{C^{n}} ∣ f ∣^{2} e^{- φ} d V,$ where $E$ is the weighted energy of Hörmander's weighted L2 existence theorem for the dbar equation with $q = 1$ ; here $w = λ_{1} = 1$ , so the explicit solution attains equality in the $q = 1$ estimate rather than merely satisfying its bound.

Facts & Assumptions

Given: The Axiom of Choice; an integer $n \geq 1$ ; the domain $Ω : = C^{n}$ ; the weight $φ (z) : = ∣ z ∣^{2}$ ; the $(0, 1)$ -form $f = d {\overset{ˉ}{z}}_{1}$ ; the function $u : = {\overset{ˉ}{z}}_{1}$ .

[F1]

A $(0, q)$ -form coefficient tuple $u = (u_{J})_{∣ J ∣ = q}$ carries the inner product $⟨ u, v ⟩_{φ} : = \int_{Ω} \sum_{∣ J ∣ = q} u_{J} \overline{v_{J}} e^{- φ} d V, ∥ u ∥_{φ}^{2} : = ⟨ u, u ⟩_{φ},$ where $d V$ is Lebesgue measure on $C^{n} ≅ R^{2 n}$ (Weighted L2 spaces and maximal dbar operators); the pointwise norm of a smooth $(0, q)$ -form is the Euclidean norm of its coefficient tuple (Bigraded complex forms and the Dolbeault operators).

[F2]

For a $C^{1}$ function $g$ the smooth $\overset{ˉ}{\partial}$ is $\overset{ˉ}{\partial} g = \sum_{j} (\partial_{{\overset{ˉ}{z}}_{j}} g) d {\overset{ˉ}{z}}_{j}$ , the distributional $\overset{ˉ}{\partial}$ restricts to it on smooth forms, and $d {\overset{ˉ}{z}}_{j}$ is the $(0, 1)$ -form with coefficient tuple $δ_{j}$ of the ordered pair index (Bigraded complex forms and the Dolbeault operators, The d, partial and dbar identities, Weighted L2 spaces and maximal dbar operators).

[F3]

At a point where the real partial derivatives exist, $\partial_{{\overset{ˉ}{z}}_{j}} = \frac{1}{2} (\partial_{x_{j}} + i \partial_{y_{j}})$ (Wirtinger operators in $C^{m}$ ), and the Wirtinger operators obey the chain rule (The Wirtinger chain rule for compositions of real-differentiable complex-valued maps).

[F4]

(Hörmander's weighted L2 existence theorem for the dbar equation.) Let $Ω \subseteq C^{n}$ be Hartogs pseudoconvex, $φ \in C^{2} (Ω)$ strictly plurisubharmonic, $1 \leq q \leq n$ , $λ_{1} \leq \dots \leq λ_{n}$ the eigenvalues of $(φ_{j \overset{ˉ}{k}})$ , $w : = λ_{1} + \dots + λ_{q} > 0$ and $E (f) : = \int_{Ω} ∣ f ∣^{2} w^{- 1} e^{- φ} d V$ . Every $\overset{ˉ}{\partial}$ -closed $f \in Dom {\overset{ˉ}{\partial}}_{q}$ with $E (f) < + \infty$ has a solution $v \in Dom {\overset{ˉ}{\partial}}_{q - 1}$ with $∥ v ∥_{φ}^{2} \leq E (f)$ .

[F5]

(Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma, $n = 2$ .) For every Borel measurable $F : R^{2} \to [0, \infty]$ , $\int_{R^{2}} F d λ_{2} = \int_{0}^{\infty} \int_{S^{1}} F (r ω) r d σ (ω) d r,$ with $σ$ the finite Borel measure of The polar surface set function on the unit sphere, and $σ (S^{1}) = 2 λ_{2} ({x \in R^{2} : ∣ x ∣ \leq 1}) = 2 π$ by the disc area $π$ (A disc of radius r has Riemann area pi r squared; in particular the unit disc has area pi), all identifications of $C$ with $R^{2}$ being those of Complex $m$ -space and its real coordinate dictionary.

[F6]

For $0 < r_{0} < R$ , let $ψ$ be $C^{1}$ and injective on a neighborhood of $[r_{0}, R]$ with $ψ^{'} > 0$ there. If $h$ is continuous on an interval containing $ψ ([r_{0}, R])$ , then $\int_{ψ (r_{0})}^{ψ (R)} h (t) d t = \int_{r_{0}}^{R} h (ψ (r)) ψ^{'} (r) d r$ (In one dimension the compact-Jordan formula is substitution over the unoriented image interval with the absolute derivative). This is a finite-interval assertion.

[F7]

$Γ (t) = \int_{0}^{\infty} x^{t - 1} e^{- x} d x$ for $t > 0$ and $Γ (k + 1) = k!$ for every integer $k \geq 0$ (The real Gamma function by Euler's integral, $Γ (n + 1) = n!$ for every natural number $n$ ).

[F8]

On $C^{n}$ the Euclidean Lebesgue measure $d V$ is, on Borel sets, the product of the plane Lebesgue measures $d A$ of the $n$ coordinate copies (On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n}, Complex $m$ -space and its real coordinate dictionary), and for a product-measurable $F \geq 0$ the product integral equals the iterated integral (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).

[F9]

AC is the assertion that every family of nonempty sets has a choice function (The Axiom of Choice).

[F10]

For nonnegative measurable functions increasing pointwise, their integrals increase to the integral of their limit (Monotone convergence for the integral).

[F11]

The whole space $C^{n}$ is Hartogs pseudoconvex by convention (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).

Choice use. AC is the ambient hypothesis recorded in the Statement and cited as [F9]; it is consumed only inside the supplier theorems [F4], [F5] and [F8], whose proofs carry their own choice hypotheses. The example exhibits $f$ and $u$ by explicit formulas and selects nothing.

Proof

technique · direct

1.1F2F3givenalgebra

(The $\overset{ˉ}{\partial}$ computation.) By [F3], $\partial_{{\overset{ˉ}{z}}_{1}} {\overset{ˉ}{z}}_{1} = \frac{1}{2} (\partial_{x_{1}} {\overset{ˉ}{z}}_{1} + i \partial_{y_{1}} {\overset{ˉ}{z}}_{1}) = \frac{1}{2} (1 + i (- i)) = 1$ and $\partial_{{\overset{ˉ}{z}}_{j}} {\overset{ˉ}{z}}_{1} = 0$ for $j \neq 1$ ; hence the coefficient formula of [F2] gives $\overset{ˉ}{\partial} u = \sum_{j} (\partial_{{\overset{ˉ}{z}}_{j}} {\overset{ˉ}{z}}_{1}) d {\overset{ˉ}{z}}_{j} = d {\overset{ˉ}{z}}_{1} = f$ at every point of $C^{n}$ .

1.2F1givenalgebra

(Pointwise norms.) In the coefficient-tuple norm of [F1] the form $f = d {\overset{ˉ}{z}}_{1}$ has the single coefficient $1$ and the function $u$ has the single coefficient ${\overset{ˉ}{z}}_{1}$ , so $∣ f (z) ∣^{2} = 1$ and $∣ u (z) ∣^{2} = ∣ z_{1} ∣^{2}$ for every $z \in C^{n}$ .

1.3F3F4givenalgebra

(The weight.) The function $φ = ∣ z ∣^{2} = \sum_{j = 1}^{n} z_{j} {\overset{ˉ}{z}}_{j}$ is $C^{\infty}$ , and [F3] with $\partial_{{\overset{ˉ}{z}}_{j}} {\overset{ˉ}{z}}_{j} = 1$ , $\partial_{{\overset{ˉ}{z}}_{j}} {\overset{ˉ}{z}}_{k} = 0$ for $k \neq j$ gives $\partial_{{\overset{ˉ}{z}}_{j}} φ = z_{j}$ and $φ_{j \overset{ˉ}{k}} = \partial_{z_{j}} z_{k} = δ_{j k}$ ; the Hermitian matrix $(φ_{j \overset{ˉ}{k}})$ of [F4] is therefore the identity matrix, so all its eigenvalues equal $1$ , and with $q = 1$ the weight of [F4] is $w = λ_{1} = 1$ and $E (f) = \int_{C^{n}} ∣ f ∣^{2} e^{- φ} d V$ .

1.4F5F6F7F10algebra

(Plane moments.) For $a > 0$ and integers $k \geq 0$ , [F5] applies to the nonnegative continuous radial integrand and gives $\int_{C} ∣ w ∣^{2 k} e^{- a ∣ w ∣^{2}} d A = 2 π \int_{0}^{\infty} r^{2 k + 1} e^{- a r^{2}} d r .$ For $0 < ε < R$ , apply [F6] to $ψ (r) = a r^{2}$ and $h (t) = t^{k} e^{- t} / (2 a^{k + 1})$ ; its hypotheses hold on a neighborhood of $[ε, R]$ , and $\int_{ε}^{R} r^{2 k + 1} e^{- a r^{2}} d r = \frac{1}{2 a^{k + 1}} \int_{a ε^{2}}^{a R^{2}} t^{k} e^{- t} d t .$ Take $ε = 1 / m$ , $R = m$ , $m \geq 2$ . Both truncated nonnegative integrands increase to the respective full integrands, so [F10] passes to the limit; [F7] identifies the right integral with the finite value $Γ (k + 1) = k!$ . Hence $\int_{C} ∣ w ∣^{2 k} e^{- a ∣ w ∣^{2}} d A = \frac{π k!}{a^{k + 1}} .$ This proves convergence along with the formula.

2.1step 1.4algebra

With $k = 0$ and $k = 1$ at $a = 1$ , step 1.4 gives $\int_{C} e^{- ∣ w ∣^{2}} d A = π$ and $\int_{C} ∣ w ∣^{2} e^{- ∣ w ∣^{2}} d A = π$ .

3.1F8step 2.1algebra

Consequently $\int_{C^{n}} e^{- ∣ z ∣^{2}} d V = π^{n}$ and $\int_{C^{n}} ∣ z_{1} ∣^{2} e^{- ∣ z ∣^{2}} d V = π^{n}$ : writing $z = (z_{1}, z^{'})$ and using [F8], the nonnegative Borel functions $e^{- ∣ z ∣^{2}} = e^{- ∣ z_{1} ∣^{2}} \prod_{j \geq 2} e^{- ∣ z_{j} ∣^{2}}$ and $∣ z_{1} ∣^{2} e^{- ∣ z ∣^{2}}$ have product integrals equal to the iterated integrals over $C \times C^{n - 1}$ , and iterating the product decomposition $n$ times (with the empty remaining product equal to $1$ when $n = 1$ ) turns each into the corresponding product of the plane integrals of step 2.1, namely $π \cdot π^{n - 1} = π^{n}$ in both cases.

4.1step 1.2step 1.3step 3.1algebra

By steps 1.2, 1.3 and 3.1, $∥ u ∥_{φ}^{2} = \int_{C^{n}} ∣ z_{1} ∣^{2} e^{- ∣ z ∣^{2}} d V = π^{n}$ and $E (f) = \int_{C^{n}} e^{- ∣ z ∣^{2}} d V = π^{n}$ ; in particular $u \in L_{0, 0}^{2} (C^{n}, e^{- φ})$ and $f \in L_{0, 1}^{2} (C^{n}, e^{- φ})$ .

5.1F2F4F9F11step 1.1step 4.1algebra∎

The claims of the Statement hold: $\overset{ˉ}{\partial} u = f$ by step 1.1 and $∥ u ∥_{φ}^{2} = π^{n} = E (f)$ by step 4.1. Moreover $\overset{ˉ}{\partial} f = \sum_{j} (\partial_{{\overset{ˉ}{z}}_{j}} 1) d {\overset{ˉ}{z}}_{j} \land d {\overset{ˉ}{z}}_{1} = 0$ by [F2], since the coefficient $1$ of $f$ is constant and $d {\overset{ˉ}{z}}_{1} \land d {\overset{ˉ}{z}}_{1} = 0$ , so $f \in Dom {\overset{ˉ}{\partial}}_{1}$ is $\overset{ˉ}{\partial}$ -closed with finite energy and the whole-space convention [F11] and the positive identity Levi matrix of step 1.3 show that the hypotheses of [F4] hold with $q = 1$ ; the explicit solution $u$ realises the bound $∥ u ∥_{φ}^{2} \leq E (f)$ of [F4] with equality, that is, it attains the right-hand side $π^{n}$ of the $q = 1$ estimate.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-02Open item page →

Levi form of the unit ball

Example

Assume the Axiom of Choice (AC). Let $m \geq 1$ and put $ρ (z) : = ∣ z ∣^{2} - 1$ on $C^{m}$ , where $∣ z ∣^{2} = \sum_{j < m} ∣ z_{j} ∣^{2}$ . Then $L_{ρ} (a; ξ) = ∣ ξ ∣^{2} = \sum_{j < m} ∣ ξ_{j} ∣^{2}$ for every $a \in C^{m}$ and every $ξ \in C^{m}$ . In particular, at every point $p$ of the unit sphere ${∣ z ∣ = 1}$ and for every nonzero complex tangent vector $ξ$ at $p$ one has $L_{ρ} (p; ξ) = ∣ ξ ∣^{2} > 0$ . Consequently the unit ball $B = {z \in C^{m} : ρ (z) < 0}$ is strongly pseudoconvex, that is: $B$ is a domain, and at every boundary point $p$ of $B$ the function $ρ$ is a $C^{\infty}$ defining function with $d ρ (p) \neq 0$ and with $L_{ρ} (p; ξ) > 0$ for every nonzero complex tangent vector $ξ$ at $p$ . In the terminology of Levi pseudoconvex domains, $B$ is Levi pseudoconvex with strict positivity on complex tangents.

Facts & Assumptions

Given: The Axiom of Choice; an integer $m \geq 1$ ; the function $ρ (z) : = ∣ z ∣^{2} - 1 = \sum_{j < m} ∣ z_{j} ∣^{2} - 1$ on $C^{m}$ ; and the unit ball $B : = {z \in C^{m} : ρ (z) < 0}$ .

[F1]

For $u \in C^{2}$ on an open set, the Levi form is $L_{u} (a; v) : = \sum_{j < m} \sum_{k < m} \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$ and every $v \neq 0$ (The Levi form and strict plurisubharmonicity, with its coordinate labels relabeled from $1, \dots, m$ to the canonical $0, \dots, m - 1$ ).

[F2]

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

[F3]

The Wirtinger operators are $\partial_{z_{k}} f : = \frac{1}{2} (\partial_{x_{k}} f - i \partial_{y_{k}} f), \partial_{{\overset{ˉ}{z}}_{k}} f : = \frac{1}{2} (\partial_{x_{k}} f + i \partial_{y_{k}} f) (k < m),$ and for real totally differentiable $f$ the differential is recovered by $D f (a) h = \sum_{k < m} (\partial_{z_{k}} f (a) h_{k} + \partial_{{\overset{ˉ}{z}}_{k}} f (a) \overline{h_{k}})$ (Wirtinger operators in $C^{m}$ ).

[F4]

In a metric space every ball $β_{n} = B (x, 1 / n)$ with $n \geq 1$ is an open subset containing $x$ (The balls $B (x, 1 / n)$ , $n \geq 1$ , form a countable neighbourhood base at $x$ , so every metric space is first countable).

[F5]

The open ball of centre $a$ and radius $ρ > 0$ in $C^{m}$ is $B (a, ρ) = {z : ∥ z - a ∥ < ρ}$ for the norm $∥ \cdot ∥$ of [F6] (Balls, polydiscs and the distinguished boundary in $C^{m}$ ).

[F6]

$∥ z ∥ : = (\sum_{k < m} ∣ z_{k} ∣^{2})^{1 / 2}$ is a norm on the real vector space underlying $C^{m}$ , $∥ z - w ∥$ is the metric of $C^{m}$ , and the metric, the balls, the open sets, the convergent sequences and the continuous maps of $C^{m}$ are verbatim those of $R^{2 m}$ under $Φ$ (Complex $m$ -space and its real coordinate dictionary).

[F7]

A norm $N$ satisfies $N (λ v) = ∣ λ ∣ N (v)$ and $N (u + v) \leq N (u) + N (v)$ , and $N (v) = 0$ only for $v = 0$ (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms, claims (N1)–(N3)).

[F8]

Every ball of $R^{n}$ in each of the norms $∥ \cdot ∥_{1}, ∥ \cdot ∥_{2}, ∥ \cdot ∥_{\infty}$ is convex, path-connected and connected (Every convex subset of $R^{n}$ , in particular every ball and $R^{n}$ itself, is path-connected and hence connected).

[F9]

The boundary of a set $A$ in a metric space is $\partial A = \overline{A} ∖ int (A)$ (Interior, closure, boundary, limit point, isolated point and dense subset of a metric space).

[F10]

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 Example, and [F10] is cited as that hypothesis. The proof selects nothing: the coordinate computations, the point $0 \in B$ , the explicit radius $r = (∥ p ∥ - 1) / 2$ and the radial points $(1 - t) p$ studied in the boundary step below are all formulas, so no family of nonempty sets is ever presented for selection.

Verification

technique · direct

1.1F3F10givenalgebra

Writing $z_{j} = x_{j} + i y_{j}$ , the coordinate expression $ρ = \sum_{j < m} (x_{j}^{2} + y_{j}^{2}) - 1$ is a polynomial, so $ρ \in C^{\infty} (C^{m}, R)$ ; applying [F3] to the partials $\partial_{x_{j}} ρ = 2 x_{j}$ and $\partial_{y_{j}} ρ = 2 y_{j}$ gives $\partial_{z_{j}} ρ (a) = \frac{1}{2} (2 x_{j} - 2 i y_{j}) = \overline{a_{j}}$ and $\partial_{{\overset{ˉ}{z}}_{j}} ρ (a) = \frac{1}{2} (2 x_{j} + 2 i y_{j}) = a_{j}$ at every $a \in C^{m}$ .

1.2F4F5F6F7F8

The set $B = {z : ρ (z) < 0} = {z : ∥ z ∥ < 1} = B (0, 1)$ is the open ball of radius $1$ about $0$ in the sense of [F5], hence is an open subset of $C^{m}$ by [F4] with $n = 1$ ; it is nonempty because $∥ 0 ∥ = 0 < 1$ by [F7]; and it is connected, because $Φ (B)$ is the unit ball of $R^{2 m}$ for the Euclidean norm, which is path-connected and connected by [F8], while [F6] carries the open sets of $C^{m}$ onto those of $R^{2 m}$ . Thus $B$ is a domain.

2.1F1step 1.1algebra

Differentiating the first-order expressions of step 1.1 gives $\partial^{2} ρ / \partial z_{j} \partial {\overset{ˉ}{z}}_{k} = δ_{j k}$ for all $j, k < m$ , so [F1] yields, for every $a \in C^{m}$ and every $ξ \in C^{m}$ , $L_{ρ} (a; ξ) = \sum_{j, k < m} δ_{j k} ξ_{j} \overline{ξ_{k}} = \sum_{j < m} ∣ ξ_{j} ∣^{2} = ∣ ξ ∣^{2} .$

2.2F7F9step 1.2

The boundary of $B$ is exactly the unit sphere ${∥ z ∥ = 1}$ : if $∥ p ∥ < 1$ then $p \in B$ and $B$ is open by step 1.2, so $p \notin \partial B$ by [F9]; if $∥ p ∥ > 1$ then with $r : = (∥ p ∥ - 1) / 2 > 0$ every $z$ with $∥ z - p ∥ < r$ satisfies $∥ z ∥ \geq ∥ p ∥ - ∥ p - z ∥ > (∥ p ∥ + 1) / 2 > 1$ by [F7], so the ball about $p$ of radius $r$ misses $B$ and $p \notin \overline{B}$ , hence $p \notin \partial B$ by [F9]; and if $∥ p ∥ = 1$ then for $0 < t < 1$ the points $(1 - t) p$ lie in $B$ , since $∥ (1 - t) p ∥ = 1 - t < 1$ by [F7], and converge to $p$ , since $∥ (1 - t) p - p ∥ = t$ , while $p \notin B$ ; hence $p \in \overline{B} ∖ B = \overline{B} ∖ int (B) = \partial B$ by [F9].

3.1F2F3step 1.1step 2.1

At a point $p$ with $∥ p ∥ = 1$ one has $ρ (p) = 0$ ; the complex tangent vectors at $p$ are those $ξ$ with $\sum_{j} \frac{\partial ρ}{\partial z_{j}} (p) ξ_{j} = \sum_{j} \overline{p_{j}} ξ_{j} = 0$ by [F2] and step 1.1, and each nonzero such $ξ$ satisfies $L_{ρ} (p; ξ) = ∣ ξ ∣^{2} > 0$ by step 2.1; also $d ρ (p) \neq 0$ , because if $D ρ (p) = 0$ then [F3] forces every Wirtinger partial $\partial_{z_{j}} ρ (p) = \overline{p_{j}}$ and $\partial_{{\overset{ˉ}{z}}_{j}} ρ (p) = p_{j}$ to vanish, whereas some $p_{j} \neq 0$ since $∥ p ∥ = 1$ .

4.1F1F2step 2.1step 2.2∎

Conclusion: every boundary point of $B$ satisfies $∥ p ∥ = 1$ by step 2.2, so with $U : = C^{m}$ the pair $(U, ρ)$ satisfies $B \cap U = {ρ < 0}$ , $d ρ (p) \neq 0$ and $L_{ρ} (p; ξ) = ∣ ξ ∣^{2} > 0$ for every nonzero complex tangent vector $ξ$ by step 3.1; this is the strict form of the condition in [F2], so the unit ball is strongly pseudoconvex, and in particular, weakening $>$ to $\geq$ , it is Levi pseudoconvex in the sense of [F2]; moreover $ρ$ is strictly plurisubharmonic on all of $C^{m}$ by [F1] and step 2.1, since $L_{ρ} (a; ξ) = ∣ ξ ∣^{2} > 0$ for every $a$ and every $ξ \neq 0$ .

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-10-02Open item page →

An explicit $\overset{ˉ}{\partial}$ solution with an $L^{2}$ estimate

Statement

Assume the Axiom of Choice (AC). On $C$ with the weight $φ (z) : = 2 ∣ z ∣^{2}$ , the $(0, 1)$ -form $f : = \overset{ˉ}{z} d \overset{ˉ}{z}$ and the function $u : = \frac{1}{2} {\overset{ˉ}{z}}^{2}$ satisfy $\overset{ˉ}{\partial} u = f, \int_{C} ∣ u ∣^{2} e^{- φ} d A = \frac{π}{16} \leq \frac{π}{8} = \frac{1}{2} \int_{C} ∣ f ∣^{2} e^{- φ} d A .$ The factor $\frac{1}{2}$ is the reciprocal $w^{- 1}$ of the single weight eigenvalue $w = λ_{1} = 2$ of $φ = 2 ∣ z ∣^{2}$ , so the second display is an instance of the $q = 1$ weighted estimate of Hörmander's weighted L2 existence theorem for the dbar equation on the domain $C$ .

Facts & Assumptions

Given: The Axiom of Choice; the domain $Ω : = C$ ; the weight $φ (z) : = 2 ∣ z ∣^{2}$ ; the $(0, 1)$ -form $f : = \overset{ˉ}{z} d \overset{ˉ}{z}$ ; the function $u : = \frac{1}{2} {\overset{ˉ}{z}}^{2}$ .

[F1]

[F2]

For a $C^{1}$ function $g$ the smooth $\overset{ˉ}{\partial}$ is $\overset{ˉ}{\partial} g = \sum_{j} (\partial_{{\overset{ˉ}{z}}_{j}} g) d {\overset{ˉ}{z}}_{j}$ , and the distributional $\overset{ˉ}{\partial}$ of (b) of the weighted space definition restricts to this smooth expression (Bigraded complex forms and the Dolbeault operators, The d, partial and dbar identities, Weighted L2 spaces and maximal dbar operators).

[F3]

[F4]

[F5]

[F6]

$σ (S^{1}) = 2 λ_{2} ({x \in R^{2} : ∣ x ∣ \leq 1}) = 2 π$ , by the definition $σ (E) = n λ_{n} ({r ω : ω \in E, 0 < r \leq 1})$ with $n = 2$ (The polar surface set function on the unit sphere) and the disc area $π$ (A disc of radius r has Riemann area pi r squared; in particular the unit disc has area pi), the identifications of $C$ with $R^{2}$ being those of Complex $m$ -space and its real coordinate dictionary.

[F7]

[F8]

[F9]

AC is the assertion that every family of nonempty sets has a choice function (The Axiom of Choice).

[F10]

For nonnegative measurable functions increasing pointwise, their integrals increase to the integral of their limit (Monotone convergence for the integral).

[F11]

The whole space $C^{n}$ is Hartogs pseudoconvex by convention (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).

Choice use. AC is the ambient hypothesis recorded in the Statement and cited as [F9]; it is consumed only inside the two supplier theorems [F4] and [F5], whose proofs carry their own choice hypotheses. The example exhibits $f$ and $u$ by explicit formulas and selects nothing.

Proof

technique · direct

1.1F2F3givenalgebra

(The $\overset{ˉ}{\partial}$ computation.) By [F3], $\partial_{\overset{ˉ}{z}} \overset{ˉ}{z} = \frac{1}{2} (\partial_{x} \overset{ˉ}{z} + i \partial_{y} \overset{ˉ}{z}) = \frac{1}{2} (1 + i (- i)) = 1$ , so the chain rule in [F3] gives $\partial_{\overset{ˉ}{z}} {\overset{ˉ}{z}}^{2} = 2 \overset{ˉ}{z} \partial_{\overset{ˉ}{z}} \overset{ˉ}{z} = 2 \overset{ˉ}{z}$ ; hence $\overset{ˉ}{\partial} u = \frac{1}{2} \cdot 2 \overset{ˉ}{z} d \overset{ˉ}{z} = \overset{ˉ}{z} d \overset{ˉ}{z} = f$ at every point of $C$ , by the coefficient formula of [F2] for the associated $(0, 1)$ -coefficient tuple.

1.2F1givenalgebra

(Pointwise norms.) In the coefficient-tuple norm of [F1] the form $f = \overset{ˉ}{z} d \overset{ˉ}{z}$ has the single coefficient $\overset{ˉ}{z}$ and the function $u$ has the single coefficient $\frac{1}{2} {\overset{ˉ}{z}}^{2}$ , so $∣ f (z) ∣^{2} = ∣ \overset{ˉ}{z} ∣^{2} = ∣ z ∣^{2}$ and $∣ u (z) ∣^{2} = \frac{1}{4} ∣ {\overset{ˉ}{z}}^{2} ∣^{2} = \frac{1}{4} ∣ z ∣^{4}$ for every $z$ .

1.3F3F4givenalgebra

(The weight.) The function $φ = 2 z \overset{ˉ}{z}$ is $C^{\infty}$ , and [F3] together with $\partial_{\overset{ˉ}{z}} \overset{ˉ}{z} = 1$ , $\partial_{\overset{ˉ}{z}} z = 0$ gives $\partial_{\overset{ˉ}{z}} φ = 2 z$ and then $φ_{z \overset{ˉ}{z}} = \partial_{z} (2 z) = 2$ ; the Hermitian matrix $(φ_{j \overset{ˉ}{k}})$ of [F4] is therefore the $1 \times 1$ matrix $(2)$ , so with $q = 1$ the weight of [F4] is $w = λ_{1} = 2$ and $E (f) = \frac{1}{2} \int_{C} ∣ f ∣^{2} e^{- φ} d A$ .

1.4F5F6F7F8F10algebra

(Radial moments.) For $a > 0$ and integers $k \geq 0$ , [F5] and [F6] apply to the nonnegative continuous radial integrand and give $\int_{C} ∣ z ∣^{2 k} e^{- a ∣ z ∣^{2}} d A = 2 π \int_{0}^{\infty} r^{2 k + 1} e^{- a r^{2}} d r .$ For $0 < ε < R$ , apply [F7] to $ψ (r) = a r^{2}$ and $h (t) = t^{k} e^{- t} / (2 a^{k + 1})$ ; its hypotheses hold on a neighborhood of $[ε, R]$ , and $\int_{ε}^{R} r^{2 k + 1} e^{- a r^{2}} d r = \frac{1}{2 a^{k + 1}} \int_{a ε^{2}}^{a R^{2}} t^{k} e^{- t} d t .$ Take $ε = 1 / m$ , $R = m$ , $m \geq 2$ . Both truncated nonnegative integrands increase to the respective full integrands, so [F10] passes to the limit; [F8] identifies the right integral with the finite value $Γ (k + 1) = k!$ . Hence $\int_{C} ∣ z ∣^{2 k} e^{- a ∣ z ∣^{2}} d A = \frac{π k!}{a^{k + 1}} .$ This proves convergence along with the formula, rather than assuming an improper substitution identity.

2.1step 1.3step 1.4algebra

The energy is $E (f) = \frac{1}{2} \int_{C} ∣ z ∣^{2} e^{- 2 ∣ z ∣^{2}} d A = \frac{1}{2} \cdot \frac{π \cdot 1!}{2^{2}} = \frac{π}{8}$ by step 1.3 and step 1.4 with $k = 1$ , $a = 2$ ; in particular $\int_{C} ∣ f ∣^{2} e^{- φ} d A = \frac{π}{4}$ is finite.

2.2step 1.2step 1.4algebra

The weighted norm is $∥ u ∥_{φ}^{2} = \int_{C} \frac{1}{4} ∣ z ∣^{4} e^{- 2 ∣ z ∣^{2}} d A = \frac{1}{4} \cdot \frac{π \cdot 2!}{2^{3}} = \frac{π}{16}$ by step 1.2 and step 1.4 with $k = 2$ , $a = 2$ .

3.1F2F4F9F11step 1.1step 2.1step 2.2algebra∎

The claims of the Statement hold: $\overset{ˉ}{\partial} u = f$ by step 1.1, and $∥ u ∥_{φ}^{2} = \frac{π}{16} < \frac{π}{8} = E (f) = \frac{1}{2} \int_{C} ∣ f ∣^{2} e^{- φ} d A$ by steps 2.1 and 2.2, the comparison $\frac{1}{16} < \frac{1}{8}$ being arithmetic. Moreover $u \in L_{0, 0}^{2} (C, e^{- φ})$ and $f \in L_{0, 1}^{2} (C, e^{- φ})$ by these finite values, and $\overset{ˉ}{\partial} f = (\partial_{\overset{ˉ}{z}} \overset{ˉ}{z}) d \overset{ˉ}{z} \land d \overset{ˉ}{z} = 0$ by [F2], so $f \in Dom {\overset{ˉ}{\partial}}_{1}$ is $\overset{ˉ}{\partial}$ -closed with finite energy and the whole-space convention [F11] and the positive scalar Levi coefficient of step 1.3 show that the hypotheses of [F4] hold with $q = 1$ ; the explicit solution $u$ satisfies the bound $∥ u ∥_{φ}^{2} \leq E (f)$ of [F4] with strict room.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-02Open item page →

A strictly plurisubharmonic exhaustion of the convex unit ball

Example

Assume the Axiom of Choice (AC). Fix $m \geq 1$ , let $B : = {z \in C^{m} : ∥ z ∥ < 1}$ be the unit ball, put $u (z) : = 1 - ∥ z ∥^{2}$ , and set $ψ (z) : = - \log u (z) = - \log (1 - ∥ z ∥^{2}) .$ Then $B$ is a nonempty convex domain in $C^{m}$ and $ψ$ is a $C^{\infty}$ strictly plurisubharmonic exhaustion of $B$ : at every $a \in B$ and every $ξ \in C^{m} ∖ {0}$ the Levi form is $L_{ψ} (a; ξ) = \frac{∥ ξ ∥^{2}}{u (a)} + \frac{∣ \sum_{j < m} \overline{a_{j}} ξ_{j} ∣^{2}}{u (a)^{2}} > 0,$ and every sublevel set ${ψ \leq c}$ , $c \in R$ , is a compact subset of $B$ .

Facts & Assumptions

Given: The Axiom of Choice; the unit ball $B = {z \in C^{m} : ∥ z ∥ < 1}$ with $m \geq 1$ ; the functions $u = 1 - ∥ z ∥^{2}$ and $ψ = - \log u$ .

[F1]

For open $Ω \subseteq C^{m}$ and $u \in C^{2} (Ω, R)$ the Levi form is $L_{u} (a; v) : = \sum_{j < m} \sum_{k < m} \frac{\partial^{2} u}{\partial z_{j} \partial {\overline{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$ (The Levi form and strict plurisubharmonicity, with its coordinate labels relabeled from $1, \dots, m$ to the canonical $0, \dots, m - 1$ ).

[F2]

A $C^{2}$ function is plurisubharmonic on $Ω$ exactly when $L_{u} (a; v) \geq 0$ for every $a \in Ω$ and every $v \in C^{m}$ (The C^2 Levi criterion for plurisubharmonicity).

[F3]

A continuous plurisubharmonic exhaustion of a domain $Ω$ is a continuous plurisubharmonic $u$ on $Ω$ with ${u \leq c}$ compact in $Ω$ for every real $c$ (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).

[F4]

The open ball and closed ball of centre $a$ and radius $ρ > 0$ are $B (a, ρ) = {z : ∥ z - a ∥ < ρ}$ and $\overline{B} (a, ρ) = {z : ∥ z - a ∥ \leq ρ}$ (Balls, polydiscs and the distinguished boundary in $C^{m}$ ).

[F5]

In a metric space $(X, d)$ the open ball $B (x, r)$ is open and the closed ball $\overset{ˉ}{B} (x, r)$ is closed, for every $x$ and every $r > 0$ (Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed).

[F6]

Through the dictionary $Φ : C^{m} \to R^{2 m}$ one has $∥ z ∥ = (\sum_{k < m} ∣ z_{k} ∣^{2})^{1 / 2}$ with $∣ z_{k} ∣^{2} = x_{k}^{2} + y_{k}^{2}$ , the balls, open sets and continuous maps of $C^{m}$ are verbatim those of $R^{2 m}$ , and a subset of $C^{m}$ is compact exactly when it is closed and bounded (Complex $m$ -space and its real coordinate dictionary).

[F7]

A subset $A$ of a metric space is bounded when $A = \emptyset$ or $A \subseteq B (x_{0}, r)$ for some point $x_{0}$ and some real $r > 0$ (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space).

[F8]

A norm $N$ satisfies $N (v) = 0$ if and only if $v = 0$ , absolute homogeneity $N (λ v) = ∣ λ ∣ N (v)$ , and the triangle inequality $N (u + v) \leq N (u) + N (v)$ (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms).

[F9]

A subset $U \subseteq R^{m}$ is convex when for all $x, y \in U$ and all $t \in [0, 1]$ the point $(1 - t) x + t y$ lies in $U$ (A convex subset of $R^{m}$ contains every line segment between two of its points).

[F10]

A subset $A$ of a topological space is a compact subset when the subspace $(A, T_{A})$ is a compact topological space (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

[F11]

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

[F12]

For $x > 0$ , $\log$ is differentiable with $\log^{'} (x) = 1 / x$ (The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t).

[F13]

For every real $α$ the function $x \mapsto x^{α}$ is differentiable on $(0, \infty)$ with $(x^{α})^{'} = α x^{α - 1}$ (Continuity and derivatives of positive-base real powers).

[F14]

The exponential function is continuous and strictly increasing on $R$ (The exponential function is strictly increasing).

[F15]

$\log$ is the inverse function of $\exp$ , so that $\exp (\log x) = x$ for every $x > 0$ (The natural logarithm as the inverse of the exponential function).

[F16]

A set $X$ is path-connected when every pair of its points is joined by a path in $X$ (Paths, path-connected spaces and path components); every path-connected space is connected (Every path-connected space is connected, and every path component lies inside a component).

[F17]

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 Example and [F17] is cited as that hypothesis. The proof selects nothing: the ball, the function $ψ$ , the straight-line paths and the radii $r = (1 - \exp (- c))^{1 / 2}$ are explicit formulas.

Verification

technique · direct

1.1F4F5F6F8F9F16F17givenalgebra

By [F6] one has $∥ z ∥^{2} = \sum_{j < m} ∣ z_{j} ∣^{2} = \sum_{j < m} (x_{j}^{2} + y_{j}^{2})$ , and $B$ is the open ball $B (0, 1)$ in the sense of [F4]; it is open by [F5] and nonempty because $∥ 0 ∥ = 0 < 1$ by [F8]. It is convex: for $z, w \in B$ and $t \in [0, 1]$ , [F8] gives $∥ (1 - t) z + t w ∥ \leq (1 - t) ∥ z ∥ + t ∥ w ∥ < (1 - t) + t = 1$ since $1 - t \geq 0$ and $t \geq 0$ , so $(1 - t) z + t w \in B$ , which is the straight-line condition of [F9] transported by the $R$ -linear dictionary [F6]. The segments $t \mapsto (1 - t) z + t w$ are continuous paths in $B$ from $z$ to $w$ , so $B$ is path-connected by [F16] and connected by [F16]; hence $B$ is a nonempty convex domain in $C^{m}$ .

2.1F6F11F12F13inductionalgebra

The function $u = 1 - \sum_{j < m} (x_{j}^{2} + y_{j}^{2})$ is a polynomial in the real coordinates, hence $C^{\infty}$ on $C^{m}$ , and $u > 0$ on $B$ by step 1.1, so $ψ = - \log u$ is real-valued on $B$ . Moreover $\log$ is $C^{\infty}$ on $(0, \infty)$ : $\log^{'} = 1 / t$ by [F12], and $t \mapsto t^{- 1}$ has $k$ -th derivative $(- 1)^{k} k! t^{- k - 1}$ , a continuous function on $(0, \infty)$ , by induction from [F13], so every higher derivative of $\log$ exists and is continuous there. Hence $ψ \in C^{\infty} (B)$ , and differentiating the composition along the real coordinate directions gives $\partial_{x_{j}} ψ = 2 x_{j} / u$ and $\partial_{y_{j}} ψ = 2 y_{j} / u$ on $B$ ; applying the Wirtinger operators of [F11] gives $\partial_{z_{j}} ψ = \frac{1}{2} (2 x_{j} - 2 i y_{j}) / u = (x_{j} - i y_{j}) / u = \overline{z_{j}} / u$ and $\partial_{{\overset{ˉ}{z}}_{j}} ψ = \frac{1}{2} (2 x_{j} + 2 i y_{j}) / u = (x_{j} + i y_{j}) / u = z_{j} / u$ at every point of $B$ .

3.1step 2.1algebra

Differentiating the first-order expressions of step 2.1 once more gives $\partial^{2} ψ / \partial z_{j} \partial {\overset{ˉ}{z}}_{k} = δ_{j k} / u + \overline{z_{j}} z_{k} / u^{2}$ : indeed $\partial_{{\overset{ˉ}{z}}_{k}} (\overline{z_{j}} / u) = (\partial_{{\overset{ˉ}{z}}_{k}} \overline{z_{j}}) / u - \overline{z_{j}} (\partial_{{\overset{ˉ}{z}}_{k}} u) / u^{2} = δ_{j k} / u + \overline{z_{j}} z_{k} / u^{2}$ , because $\partial_{{\overset{ˉ}{z}}_{k}} u = - z_{k}$ .

3.2F4F5F6F7F10F14F15step 2.1algebra

For $z \in B$ and real $c$ , since $\log$ is the inverse of the strictly increasing function $\exp$ by [F14] and [F15], one has $ψ (z) \leq c ⟺ u (z) \geq \exp (- c) ⟺ ∥ z ∥^{2} \leq 1 - \exp (- c)$ ; hence ${ψ \leq c} = {z : ∥ z ∥^{2} \leq 1 - \exp (- c)}$ . If $1 - \exp (- c) < 0$ this set is empty; if $1 - \exp (- c) = 0$ it is the compact singleton ${0}$ ; otherwise it is the closed ball $\overline{B} (0, r)$ of [F4] with $r : = (1 - \exp (- c))^{1 / 2} \in (0, 1)$ , which is closed by [F5] and bounded in the sense of [F7] because it is contained in $B (0, r + 1)$ , hence compact in $C^{m}$ by [F6]. As it is contained in $B$ , and compactness of a subset is intrinsic by [F10] with the subspace topology inherited from $B$ equal to that inherited from $C^{m}$ , it is a compact subset of $B$ .

4.1F1F2step 2.1step 3.1algebra

Substituting step 3.1 into [F1] gives, at every $a \in B$ and every $ξ \in C^{m}$ , the Levi form $L_{ψ} (a; ξ) = \sum_{j, k} (δ_{j k} / u (a) + \overline{a_{j}} a_{k} / u (a)^{2}) ξ_{j} \overline{ξ_{k}} = ∥ ξ ∥^{2} / u (a) + ∣ \sum_{j < m} \overline{a_{j}} ξ_{j} ∣^{2} / u (a)^{2}$ , because $u (a) > 0$ by step 2.1; this is $\geq ∥ ξ ∥^{2} / u (a) > 0$ for every $ξ \neq 0$ , so $ψ$ is strictly plurisubharmonic on $B$ by [F1], and in particular plurisubharmonic there by [F2].

5.1F3step 1.1step 2.1step 3.2step 4.1∎

Conclusion: by step 1.1 the ball $B$ is a nonempty convex domain in $C^{m}$ ; by step 2.1 the function $ψ$ is $C^{\infty}$ on $B$ ; by step 4.1 it is strictly plurisubharmonic, hence plurisubharmonic; and by step 3.2 every sublevel set ${ψ \leq c}$ is a compact subset of $B$ . Therefore $ψ$ is a continuous strictly plurisubharmonic exhaustion of the convex unit ball in the sense of [F3].

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-02Open item page →

A Hartogs domain with a strictly plurisubharmonic exhaustion

Example

Assume the Axiom of Choice (AC). Put $s (z, w) : = ∣ w ∣^{2} e^{2 ∣ z ∣^{2}}$ and $Ω : = {(z, w) \in C^{2} : s (z, w) < 1} = {(z, w) : ∣ w ∣ < e^{- ∣ z ∣^{2}}} .$ Then $Ω$ is a domain, the function $ψ (z, w) : = ∣ z ∣^{2} + ∣ w ∣^{2} + (1 - s (z, w))^{- 1}$ is a $C^{\infty}$ strictly plurisubharmonic exhaustion of $Ω$ , and $Ω$ is Levi pseudoconvex with strict positivity on complex tangents: $L_{s} (p; ξ) > 0$ for every nonzero complex tangent vector $ξ$ at every boundary point $p$ of $Ω$ . In particular $Ω$ carries the continuous plurisubharmonic exhaustion function $ψ$ .

Facts & Assumptions

Given: The Axiom of Choice; the functions $s (z, w) = ∣ w ∣^{2} e^{2 ∣ z ∣^{2}}$ and $ψ = ∣ z ∣^{2} + ∣ w ∣^{2} + (1 - s)^{- 1}$ ; and the domain $Ω = {(z, w) : s (z, w) < 1} = {(z, w) : ∣ w ∣ < e^{- ∣ z ∣^{2}}}$ .

[F1]

The Levi form of a $C^{2}$ function $u$ 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$ and every $v \neq 0$ (The Levi form and strict plurisubharmonicity).

[F2]

A domain $Ω$ with $C^{2}$ boundary is Levi pseudoconvex when every boundary point $p$ has a neighbourhood $U$ and a $C^{2}$ function $ρ$ with $Ω \cap U = {ρ < 0}$ , $d ρ (p) \neq 0$ , and $L_{ρ} (p; v) \geq 0$ for every complex tangent vector $v$ with $\sum_{j} \frac{\partial ρ}{\partial z_{j}} (p) v_{j} = 0$ (Levi pseudoconvex domains).

[F3]

A $C^{2}$ function on an open set is plurisubharmonic exactly when its Levi form is semipositive everywhere (The C^2 Levi criterion for plurisubharmonicity).

[F4]

A continuous plurisubharmonic exhaustion of $Ω$ is a continuous plurisubharmonic $u$ with ${u \leq c}$ compact in $Ω$ for every real $c$ (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).

[F5]

[F6]

A path in a set $A$ from $x$ to $y$ is a continuous $γ : [0, 1] \to A$ with $γ (0) = x$ , $γ (1) = y$ , and $A$ is path-connected when every two of its points are joined by a path (Paths, path-connected spaces and path components); every path-connected space is connected (Every path-connected space is connected, and every path component lies inside a component).

[F7]

A subset of $R^{N}$ is compact exactly when it is closed and bounded (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ 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).

[F8]

Through $Φ (z, w) = (Re z, Im z, Re w, Im w)$ , the metric, the balls, the open sets and the compact sets of $C^{2}$ are verbatim those of $R^{4}$ (Complex $m$ -space and its real coordinate dictionary).

[F9]

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 Example, and [F9] is cited as that hypothesis. The proof selects nothing: the star-shaped paths, the function $ψ$ , the open sublevel bounds and the halving radius arguments are explicit formulas.

Verification

technique · direct

1.1F5F9givenalgebra

Put $E : = e^{2 ∣ z ∣^{2}}$ , so that $s = ∣ w ∣^{2} E$ is $C^{\infty}$ on $C^{2}$ ; the Wirtinger operators of [F5] give $\partial_{z} s = 2 \overset{ˉ}{z} s$ , $\partial_{\overset{ˉ}{z}} s = 2 z s$ , $\partial_{w} s = \overset{ˉ}{w} E$ , $\partial_{\overset{ˉ}{w}} s = w E$ , and differentiating once more gives $\partial^{2} s / \partial z \partial \overset{ˉ}{z} = 2 s (1 + 2 ∣ z ∣^{2})$ , $\partial^{2} s / \partial w \partial \overset{ˉ}{w} = E$ , $\partial^{2} s / \partial z \partial \overset{ˉ}{w} = 2 \overset{ˉ}{z} w E$ , $\partial^{2} s / \partial w \partial \overset{ˉ}{z} = 2 z \overset{ˉ}{w} E$ .

1.2F6givenalgebra

$Ω = {s < 1}$ is open and nonempty ( $s (0, 0) = 0 < 1$ ), and it is star-shaped about the origin: if $(z, w) \in Ω$ and $0 < t \leq 1$ , then $∣ w ∣ < e^{- ∣ z ∣^{2}}$ gives $∣ t w ∣ = t ∣ w ∣ < t e^{- ∣ z ∣^{2}} \leq e^{- t^{2} ∣ z ∣^{2}}$ , since $t \leq 1$ and $t^{2} ∣ z ∣^{2} \leq ∣ z ∣^{2}$ , so $(t z, t w) \in Ω$ ; at $t = 0$ the point is $(0, 0) \in Ω$ . Thus each radial segment $t \mapsto (t z, t w)$ lies in $Ω$ and joins $(z, w)$ to the origin, so $Ω$ is path-connected and, by [F6], connected. Hence $Ω$ is a domain.

1.3givenalgebra

The function $h (t) : = (1 - t)^{- 1}$ is $C^{\infty}$ and satisfies $h^{'} (t) = (1 - t)^{- 2} > 0$ and $h^{''} (t) = 2 (1 - t)^{- 3} > 0$ on $(- \infty, 1)$ , so $h$ is strictly increasing and convex there; since $s < 1$ on $Ω$ , the function $ψ = ∣ z ∣^{2} + ∣ w ∣^{2} + h (s)$ is $C^{\infty}$ and real-valued on $Ω$ .

1.4F1F5algebra

For a real-valued $C^{2}$ function $u$ and a $C^{2}$ function $ϕ$ of one real variable one has $\partial \overset{ˉ}{\partial} (ϕ \circ u) = ϕ^{'} (u) \partial \overset{ˉ}{\partial} u + ϕ^{''} (u) \partial u \land \overset{ˉ}{\partial} u$ , hence at every point $L_{ϕ \circ u} (a; ξ) = ϕ^{'} (u (a)) L_{u} (a; ξ) + ϕ^{''} (u (a)) ∣ \sum_{j} \partial_{z_{j}} u (a) ξ_{j} ∣^{2}$ .

2.1F3step 1.1algebra

The Hermitian matrix of the coefficients of step 1.1 is $M = (\begin{array}{cc} 2 s (1 + 2 ∣ z ∣^{2}) & 2 \overset{ˉ}{z} w E \\ 2 z \overset{ˉ}{w} E & E \end{array})$ : its diagonal entries are nonnegative, its determinant is $2 s (1 + 2 ∣ z ∣^{2}) E - 4 ∣ z ∣^{2} ∣ w ∣^{2} E^{2} = 2 ∣ w ∣^{2} E^{2} \geq 0$ , and for $w = 0$ it is $diag (0, E)$ with $E > 0$ ; hence $L_{s} (a; ξ) = \sum_{j, k} ξ_{j} M_{j k} {\overset{ˉ}{ξ}}_{k} \geq 0$ for all $a, ξ$ , so [F3] makes $s$ plurisubharmonic on $C^{2}$ , and at every point with $w \neq 0$ the matrix $M$ is even positive definite (trace at least $E > 0$ , determinant $2 ∣ w ∣^{2} E^{2} > 0$ ).

2.2step 1.1step 1.2algebra

The boundary of $Ω$ is ${s = 1}$ : a point with $s (p) < 1$ lies in the open set $Ω$ and a point with $s (p) > 1$ has a neighbourhood disjoint from $Ω$ , so neither is a boundary point; and if $s (p) = 1$ then $w \neq 0$ , so $\partial_{\overset{ˉ}{w}} s (p) = w E \neq 0$ and $d s (p) \neq 0$ , and the points $p - t \nabla s (p)$ for small $t > 0$ satisfy $s (p - t \nabla s (p)) = 1 - t ∣ \nabla s (p) ∣^{2} + O (t^{2}) < 1$ , hence lie in $Ω$ and converge to $p$ , while $p \notin Ω$ ; therefore $p \in \partial Ω$ .

3.1F1step 2.1step 1.3step 1.4algebra

Applying step 1.4 to $ϕ = h$ and $u = s$ , and adding the strictly plurisubharmonic term $∣ z ∣^{2} + ∣ w ∣^{2}$ with $L_{∣ z ∣^{2} + ∣ w ∣^{2}} (a; ξ) = ∣ ξ_{1} ∣^{2} + ∣ ξ_{2} ∣^{2}$ , gives at every $a \in Ω$ and every $ξ \neq 0$ the bound $L_{ψ} (a; ξ) = ∣ ξ_{1} ∣^{2} + ∣ ξ_{2} ∣^{2} + h^{'} (s (a)) L_{s} (a; ξ) + h^{''} (s (a)) ∣ \partial s (a; ξ) ∣^{2} \geq ∣ ξ ∣^{2} > 0$ , because $h^{'} > 0$ , $h^{''} > 0$ and $L_{s} \geq 0$ by step 2.1; hence $ψ$ is strictly plurisubharmonic on $Ω$ by [F1].

3.2F2step 2.1step 2.2

On ${s = 1}$ the matrix $M$ of step 2.1 is positive definite, because $w \neq 0$ there; hence with the global defining function $ρ : = s - 1$ , the neighbourhood $U = C^{2}$ and $L_{ρ} = L_{s}$ one has $Ω = {ρ < 0}$ , $d ρ (p) \neq 0$ and $L_{ρ} (p; ξ) > 0$ for every nonzero complex tangent vector $ξ$ at every boundary point $p$ ; in particular $Ω$ is Levi pseudoconvex in the sense of [F2].

4.1F4F7F8step 1.2step 1.3step 3.1step 3.2algebra∎

For $c \leq 0$ the sublevel set ${ψ \leq c}$ is empty; for $c > 0$ it is contained in ${∣ z ∣^{2} + ∣ w ∣^{2} \leq c} \cap {s \leq 1 - c^{- 1}}$ , on which $ψ$ is continuous, so ${ψ \leq c}$ is a closed subset of $C^{2}$ ; it is bounded, and it lies in $Ω$ because $s \leq 1 - c^{- 1} < 1$ ; by [F8] it is a closed and bounded subset of $R^{4}$ , hence compact by [F7], and a compact subset of $C^{2}$ contained in $Ω$ is compact in $Ω$ . Thus every sublevel set of $ψ$ is compact, and with steps 1.2, 1.3 and 3.1 the function $ψ$ is a continuous strictly plurisubharmonic exhaustion of $Ω$ in the sense of [F4].

Remarks

Relation to the boundary-distance formulation. The library defines Hartogs pseudoconvexity by plurisubharmonicity of $- \log δ_{Ω}$ (Plurisubharmonic exhaustions and Hartogs pseudoconvexity), and the direction Hartogs pseudoconvexity implies the existence of a continuous plurisubharmonic exhaustion is Hartogs pseudoconvexity yields a continuous plurisubharmonic exhaustion. The converse direction, which would upgrade the exhaustion $ψ$ constructed here to plurisubharmonicity of $- \log δ_{Ω}$ , is not part of the published statement of that theorem. This example therefore establishes the exhaustion and the strict Levi boundary condition, and records the identification with Hartogs pseudoconvexity as an obligation rather than assuming it.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-10-02Open item page →

First Cousin gluing on the pseudoconvex domain $C$

Statement

Assume the Axiom of Choice (AC). On $C$ the sets $U_{1} : = {z : ∣ z ∣ < 2}, U_{2} : = {z : ∣ z ∣ > 1}$ and the functions $m_{1} : = 1 / z$ on $U_{1}$ and $m_{2} : = 0$ on $U_{2}$ form compatible first-Cousin data on the Hartogs pseudoconvex domain $C$ in the sense of First Cousin problem on a pseudoconvex domain: the cover is finite, each $m_{i}$ is meromorphic on $U_{i}$ , and $m_{1} - m_{2} = 1 / z$ is holomorphic on $U_{1} \cap U_{2} = {1 < ∣ z ∣ < 2}$ . The global meromorphic function $G : = 1 / z$ satisfies $G - m_{1} = 0 \in O (U_{1})$ and $G - m_{2} = 1 / z \in O (U_{2})$ , so it realizes the prescribed simple pole at $0$ .

Facts & Assumptions

Given: The Axiom of Choice; the plane $C$ ; the sets $U_{1}$ , $U_{2}$ ; the functions $m_{1} = 1 / z$ on $U_{1}$ and $m_{2} = 0$ on $U_{2}$ ; the candidate $G = 1 / z$ .

[F1]

(First Cousin problem on a pseudoconvex domain.) If $Ω$ is a Hartogs pseudoconvex domain, $(U_{i})_{i \in I}$ a locally finite open cover of $Ω$ and $m_{i}$ meromorphic on $U_{i}$ with $m_{i} - m_{j}$ holomorphic on $U_{i} \cap U_{j}$ for all $i, j$ , then there is a meromorphic $G$ on $Ω$ with $G - m_{i}$ holomorphic on $U_{i}$ for every $i$ .

[F2]

A meromorphic function on an open $U$ is a function on an open dense $D \subseteq U$ , holomorphic there, which near each point of $U$ equals a quotient $f / g$ of holomorphic functions with $g$ not identically zero on any component; every holomorphic function is meromorphic, and " $F - G$ is holomorphic on $V$ " means that the difference admits a holomorphic extension to $V$ (Meromorphic functions on an open set in complex Euclidean space).

[F3]

When $Ω = C^{m}$ one has $δ_{Ω} \equiv + \infty$ , the boundary function is by convention the constant function $0$ , and the whole space is Hartogs pseudoconvex (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).

[F4]

If $g : U \to C$ is complex differentiable at $a$ with $g (a) \neq 0$ , then $1 / g$ is complex differentiable at $a$ with $(1 / g)^{'} (a) = - g^{'} (a) / g (a)^{2}$ , and the identity function has derivative $1$ (Linearity, product, reciprocal, and quotient rules for complex derivatives); a function is holomorphic on $U$ when it is complex differentiable at every point of $U$ (Holomorphic functions on an open subset of $C^{m}$ ).

[F5]

The Euclidean ball $B (0, 2) \subseteq C$ is convex and hence path-connected, and path-connected sets are connected (Every convex subset of $R^{n}$ , in particular every ball and $R^{n}$ itself, is path-connected and hence connected, Every path-connected space is connected, and every path component lies inside a component), while the exterior ${z : ∣ z ∣ > 1}$ is open and path-connected (The exterior of a closed disc in the plane is path-connected); balls are open and closed balls are closed in a metric space (Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed).

[F6]

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 [F6]; it is consumed only inside the supplier theorem [F1], whose proof carries its own choice hypotheses. The example exhibits $G$ by an explicit formula and selects nothing.

Proof

technique · direct

1.1F5givenalgebra

(The cover.) By [F5] the set $U_{1} = B (0, 2)$ is open, convex, path-connected and connected, and $U_{2} = {z : ∣ z ∣ > 1} = C ∖ \overline{B} (0, 1)$ is open and path-connected, hence connected; moreover $U_{1} \cup U_{2} = C$ and $U_{1} \cap U_{2} = {z : 1 < ∣ z ∣ < 2}$ , so $(U_{1}, U_{2})$ is a finite, hence locally finite, open cover of $C$ by domains.

1.2F2F4givenalgebra

(The meromorphic data.) By [F4] the identity $z \mapsto z$ is holomorphic on $C$ and $z \mapsto 1 / z$ is holomorphic on $C ∖ {0}$ ; hence $m_{1} = 1 / z$ is meromorphic on $U_{1}$ in the sense of [F2]: its domain $U_{1} ∖ {0}$ is open and dense in $U_{1}$ , $m_{1}$ is holomorphic there, and at every point of $U_{1}$ it equals $f / g$ with $f : = 1$ and $g : = z$ , the denominator $g$ not vanishing identically on any component of $U_{1}$ . Likewise $m_{2} = 0$ is holomorphic, hence meromorphic, on $U_{2}$ .

2.1F1F2F3F4step 1.2algebra

(Compatibility.) On the overlap $U_{1} \cap U_{2} = {1 < ∣ z ∣ < 2}$ , which does not contain $0$ , the difference $m_{1} - m_{2} = 1 / z$ is holomorphic by [F4]; this is the compatibility clause of [F1], and $C$ is Hartogs pseudoconvex by [F3], so the data satisfy the hypotheses of [F1].

3.1F1step 2.1

(Existence by the Cousin theorem.) By [F1] there is a meromorphic function $G$ on $C$ with $G - m_{i}$ holomorphic on $U_{i}$ for $i = 1, 2$ .

4.1F1F2F4step 1.2step 3.1algebra

(The explicit solution.) The function $G = 1 / z$ is meromorphic on $C$ with domain $C ∖ {0}$ by [F2] and [F4]; moreover $G - m_{1} = 0$ is holomorphic on $U_{1}$ , and $G - m_{2} = 1 / z$ is holomorphic on $U_{2}$ because $0 \notin U_{2}$ and $z \mapsto 1 / z$ is holomorphic on $C ∖ {0}$ by [F4]. So $G = 1 / z$ is a solution in the sense of [F1]: it differs from $m_{i}$ by a holomorphic function on each $U_{i}$ , and its only pole is the simple pole at $0$ with principal part $1 / z$ , which is exactly the pole prescribed by the data.

5.1F6step 4.1∎

(Conclusion.) The sets $U_{1}, U_{2}$ and the functions $m_{1}, m_{2}$ are compatible first-Cousin data on the Hartogs pseudoconvex domain $C$ , and the global meromorphic function $G = 1 / z$ realizes the prescribed simple pole at the origin, as claimed under the ambient Axiom of Choice [F6].

Hörmander Estimates and the Levi Problem — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

Hörmander estimate with a Gaussian weight

Statement

Facts & Assumptions

Proof

Levi form of the unit ball

Example

Facts & Assumptions

Verification

An explicit ∂ˉ∂ˉ solution with an L2L2 estimate

Statement

Facts & Assumptions

Proof

A strictly plurisubharmonic exhaustion of the convex unit ball

Example

Facts & Assumptions

Verification

A Hartogs domain with a strictly plurisubharmonic exhaustion

Example

Facts & Assumptions

Verification

Remarks

First Cousin gluing on the pseudoconvex domain CC

Statement

Facts & Assumptions

Proof

Sources

An explicit $\overset{ˉ}{\partial}$ solution with an $L^{2}$ estimate

First Cousin gluing on the pseudoconvex domain $C$