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.

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]

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}$ , 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]

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,$ where $σ$ is the finite Borel measure of The polar surface set function on the unit sphere.

[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]

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.

[F8]

$Γ (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$ ).

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

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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

An explicit ∂ˉ∂ˉ solution with an L2L2 estimate