ExampleConstruction: Literature-sourcedVerification: 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.

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.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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