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

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.

Dolbeault green operator is compact on the orthogonal complement of the kernel

Statement

Assume the Axiom of Choice (The Axiom of Choice). It enters through the Sobolev localization and local compactness interfaces, and it supplies Dependent Choice for the sequential compact-operator criterion; the Lax–Milgram and compact self-adjoint norm-attainment arguments use only Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ ), AC implies DC implies countable choice). Let $X$ be a compact Riemann surface, let $E \to X$ be a holomorphic line bundle with Hermitian metric $h$ , and let $g$ be a compatible Riemannian metric. Use the Hilbert spaces, maximal Dolbeault operator $\overset{ˉ}{D}$ , Hilbert adjoint ${\overset{ˉ}{D}}^{*}$ , and nonnegative self-adjoint Dolbeault Laplacian $Δ^{''}$ of The maximal Dolbeault operator and its Hilbert adjoint on a compact Riemann surface. Write $H : = \ker Δ^{''}$ and $H^{⊥}$ for its orthogonal complement in $L^{2} : = L_{0}^{2} \oplus L_{1}^{2}$ . For $u = u_{0} + u_{1}$ set $V : = dom \overset{ˉ}{D} \oplus dom {\overset{ˉ}{D}}^{*}, ∥ u ∥_{V}^{2} : = ∥ u ∥_{L^{2}}^{2} + ∥ \overset{ˉ}{D} u_{0} ∥_{L^{2}}^{2} + ∥ {\overset{ˉ}{D}}^{*} u_{1} ∥_{L^{2}}^{2} .$ By Gårding estimates for the Dolbeault Laplacian on a compact Riemann surface, $V = H^{1} (X, Λ^{0, ∙} T^{*} X \otimes E)$ with equivalent norms. Give $V$ the first-variable-linear form inner product $a (u, v) : = ⟨ u, v ⟩_{L^{2}} + ⟨ \overset{ˉ}{D} u_{0}, \overset{ˉ}{D} v_{0} ⟩_{L^{2}} + ⟨ {\overset{ˉ}{D}}^{*} u_{1}, {\overset{ˉ}{D}}^{*} v_{1} ⟩_{L^{2}} .$

Boundary operator. There is a unique bounded linear operator $B : L^{2} \to V$ (A bounded linear operator between normed spaces) satisfying $a (B f, v) = ⟨ f, v ⟩_{L^{2}} (f \in L^{2}, v \in V) .$ It obeys $∥ B f ∥_{V} \leq ∥ f ∥_{L^{2}}$ and $∥ B f ∥_{H^{2}} \leq C ∥ f ∥_{L^{2}}$ , lies in $dom Δ^{''}$ , and satisfies $(I + Δ^{''}) B f = f$ . As an operator on $L^{2}$ , $B$ is injective, self-adjoint and positive; $B ∣_{H} = I$ , $\ker (I - B) = H$ , and $B (H^{⊥}) \subseteq H^{⊥}$ .
Compactness. The operator $B : L^{2} \to L^{2}$ is compact.
Green operator. The restriction of $I - B$ to $H^{⊥}$ is boundedly invertible. The operator $G : = B (I - B)^{- 1} : H^{⊥} ⟶ H^{⊥}$ is compact, self-adjoint and positive, has trivial kernel, and obeys $ran G = dom Δ^{''} \cap H^{⊥}, \overline{ran G} = H^{⊥} .$ It satisfies the Green identities $Δ^{''} G f = f (f \in H^{⊥}), G Δ^{''} u = u (u \in dom Δ^{''} \cap H^{⊥}),$ and maps $H^{⊥}$ boundedly into $H^{2}$ .

Facts & Assumptions

Given: The compact Riemann surface, the supplied Hermitian and Riemannian metrics, the operators and spaces in the Statement, and full AC.

[F1]

The pointwise Hermitian $L^{2}$ pairing is first-variable-linear, its completion is a complex Hilbert space, and smooth forms are dense; Hilbert space means a complete inner-product space (Hermitian metric and $L^{2}$ pairing on a compact Riemann surface, Hilbert space).

[F2]

The maximal operator and its adjoint are densely defined and closed, $Δ^{''}$ is self-adjoint and nonnegative with the block-composition domain, and for $u \in dom Δ^{''}$ , $⟨ Δ^{''} u, u ⟩ = ∥ \overset{ˉ}{D} u_{0} ∥_{L^{2}}^{2} + ∥ {\overset{ˉ}{D}}^{*} u_{1} ∥_{L^{2}}^{2}$ (The maximal Dolbeault operator and its Hilbert adjoint on a compact Riemann surface).

[F3]

The first-order estimate identifies $V$ with $H^{1}$ , proves smooth graph-norm density, and identifies the form equation against smooth tests with the distributional equation for $Δ^{''}$ . A distributional solution $u \in H^{1}$ of $Δ^{''} u = f \in L^{2}$ lies in $H^{2}$ and obeys $∥ u ∥_{H^{2}} \leq C_{0} (∥ f ∥_{L^{2}} + ∥ u ∥_{L^{2}})$ (Gårding estimates for the Dolbeault Laplacian on a compact Riemann surface).

[F4]

The local formulas for $\overset{ˉ}{D}$ and ${\overset{ˉ}{D}}^{*}$ have smooth coefficients. If $u \in H^{2}$ , then their local coefficients applied to $u$ lie in $H^{1}$ : weak derivatives of an $H^{2}$ coefficient are $H^{1}$ , and multiplication by a smooth coefficient preserves $H^{1}$ by the distributional Leibniz rule. Consequently $\overset{ˉ}{D} u_{0} \in dom {\overset{ˉ}{D}}^{*}$ and ${\overset{ˉ}{D}}^{*} u_{1} \in dom \overset{ˉ}{D}$ , so $u \in dom Δ^{''}$ (The Dolbeault adjoint and Laplacian: local formulas and ellipticity, Leibniz rule for distributions).

[F5]

On a Hilbert space, a bounded coercive sesquilinear form and a bounded conjugate-linear functional have a unique Lax–Milgram solution; if the coercivity constant is $1$ , its form norm is at most the functional norm. A linear map is bounded when a constant controls its output norm by its input norm. Cauchy–Schwarz bounds the form and functional, and Lax–Milgram uses Countable Choice (Bounded, coercive and symmetric sesquilinear forms, The Lax--Milgram theorem, The Axiom of Countable Choice ( ${A C}_{ω}$ ), A bounded linear operator between normed spaces, Cauchy–Schwarz: $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ , with equality exactly for linearly dependent vectors).

[F6]

A sequence bounded in $W_{l o c}^{1, 2}$ on a Euclidean open set has a subsequence converging in $L_{l o c}^{2}$ under AC (Local $L^{p}$ compactness of $W_{l o c}^{1, p}$ -bounded sequences).

[F7]

A bounded linear operator is compact when every bounded sequence has an image subsequence converging in norm; the sequential characterization assumes DC, and AC implies DC (Compact linear operator, Sequential characterization of compact operators, AC implies DC implies countable choice).

[F8]

For a nonzero compact self-adjoint operator $T$ on a Hilbert space, one of $∥ T ∥$ and $- ∥ T ∥$ is an eigenvalue; self-adjointness and positivity have their bounded-operator meanings, and $∥ T ∥$ is the operator norm. This fact assumes Countable Choice (Norm point of a compact self adjoint operator is an eigenvalue up to sign, Self-adjoint, positive, unitary and normal operators, The operator norm as the least bound and as the unit-sphere or unit-ball supremum, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F9]

If $T$ is bounded with $∥ T ∥ < 1$ on a Banach space, $I - T$ has inverse $\sum_{n \geq 0} T^{n}$ with norm at most $(1 - ∥ T ∥)^{- 1}$ (Neumann series and small perturbations of bounded inverses).

[F10]

An orthogonal complement is the subspace of vectors orthogonal to the given set and is closed (Orthogonality and the orthogonal complement, Orthogonal complements are closed).

[F11]

Every closed subspace of a Hilbert space is complete (Closed subspaces of complete metric spaces are complete; the converse under countable choice).

[F12]

Full AC supplies the Countable Choice instances used by Lax–Milgram and norm attainment (The Axiom of Choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F13]

For a linear subspace of a Hilbert space, its double orthogonal complement is its closure (The double orthogonal complement of a subspace is its closure).

Proof

technique · Solve the positive form equation by Lax–Milgram, use the local Rellich theorem to prove compactness, then invert $I-B$ on the orthogonal complement of the harmonic kernel

1.1F1F3F5F12algebra

The form $a$ is Hermitian and bounded by $∥ u ∥_{V} ∥ v ∥_{V}$ , and $a (u, u) = ∥ u ∥_{V}^{2}$ , so it is coercive with constant $1$ . For each $f \in L^{2}$ , $v \mapsto ⟨ f, v ⟩_{L^{2}}$ is conjugate-linear and has norm at most $∥ f ∥_{L^{2}}$ on $V$ . Since $V$ is Hilbert by [F3], Lax–Milgram [F5] gives a unique $B f \in V$ with $a (B f, v) = ⟨ f, v ⟩$ for every $v \in V$ , and $∥ B f ∥_{V} \leq ∥ f ∥_{L^{2}}$ . Uniqueness makes $f \mapsto B f$ linear, and this estimate makes it bounded into both $V$ and $L^{2}$ .

1.2F2F3F4algebra

For every smooth test form $v$ , the defining equation of $B f$ gives $⟨ \overset{ˉ}{D} (B f)_{0}, \overset{ˉ}{D} v_{0} ⟩ + ⟨ {\overset{ˉ}{D}}^{*} (B f)_{1}, {\overset{ˉ}{D}}^{*} v_{1} ⟩ = ⟨ f - B f, v ⟩$ . By [F3] this is the distributional equation $Δ^{''} B f = f - B f$ ; the $H^{2}$ estimate in [F3] applies because $B f \in V = H^{1}$ and $f - B f \in L^{2}$ , yielding $∥ B f ∥_{H^{2}} \leq C_{0} (∥ f - B f ∥ + ∥ B f ∥) \leq 3 C_{0} ∥ f ∥$ . Fact [F4] now puts $B f$ in $dom Δ^{''}$ , so the distributional identity is the operator identity $(I + Δ^{''}) B f = f$ . Conversely, for $u \in dom Δ^{''}$ , set $f = (I + Δ^{''}) u$ . Then $z = B f - u$ lies in $dom Δ^{''}$ and $(I + Δ^{''}) z = 0$ ; taking its pairing with $z$ and using [F2] gives $0 = ∥ z ∥^{2} + ∥ \overset{ˉ}{D} z_{0} ∥^{2} + ∥ {\overset{ˉ}{D}}^{*} z_{1} ∥^{2}$ , so $z = 0$ and $B (I + Δ^{''}) u = u$ .

1.3F1algebra

The equation with $v = B g$ gives $a (B f, B g) = ⟨ f, B g ⟩$ ; Hermitian symmetry of $a$ then gives $⟨ B f, g ⟩ = ⟨ f, B g ⟩$ , so $B$ is self-adjoint. Taking $g = f$ shows $⟨ B f, f ⟩ = a (B f, B f) \geq 0$ , so $B$ is positive. If $B f = 0$ , its defining equation gives $⟨ f, v ⟩ = 0$ for every $v \in V$ ; smooth forms are dense in $L^{2}$ by [F1], hence $f = 0$ and $B$ is injective. Also $∥ B f ∥_{L^{2}} \leq ∥ B f ∥_{V} \leq ∥ f ∥_{L^{2}}$ , so $∥ B ∥ \leq 1$ .

2.1F1F2F10step 1.3algebra

If $h \in H$ , the energy identity [F2] gives $\overset{ˉ}{D} h_{0} = 0$ and ${\overset{ˉ}{D}}^{*} h_{1} = 0$ , whence $h \in V$ and $a (h, v) = ⟨ h, v ⟩$ for all $v \in V$ ; uniqueness gives $B h = h$ . Conversely, if $B x = x$ , then $x \in V$ and testing its defining equation with $v = x$ gives $∥ x ∥_{V}^{2} = ∥ x ∥_{L^{2}}^{2}$ , so both first-order terms vanish. The block domain in [F2] then gives $x \in dom Δ^{''}$ and $Δ^{''} x = 0$ . Thus $\ker (I - B) = H$ . Self-adjointness and $B ∣_{H} = I$ imply $B (H^{⊥}) \subseteq H^{⊥}$ .

2.2F3F6F7F12step 1.2algebra

Let $(f_{n})$ be bounded in $L^{2}$ and put $u_{n} = B f_{n}$ . Step 1.2 bounds $(u_{n})$ in the fixed finite-chart $H^{2}$ norm, so every partitioned local coefficient is bounded in $W_{l o c}^{1, 2}$ ; [F6] gives a subsequence converging in $L_{l o c}^{2}$ for each chart coefficient. Successively taking subsequences over the finitely many charts and degrees gives one subsequence converging in $L^{2}$ on every compact support of the fixed partition; summing these finitely many weighted coefficient norms gives convergence in global $L^{2}$ . Thus $B$ takes every bounded sequence to a sequence with a norm-convergent subsequence. By [F7] and [F12], the sequential characterization proves that $B : L^{2} \to L^{2}$ is compact.

3.1F1F7F8F9F10F11F12step 1.3step 2.1step 2.2algebra

The closed subspace $H^{⊥}$ is invariant under $B$ by step 2.1. For any bounded sequence in $H^{⊥}$ , compactness of $B$ from step 2.2 gives a subsequence whose images converge in $L^{2}$ ; its limit remains in $H^{⊥}$ by [F10], so [F7] shows that $T : = B ∣_{H^{⊥}}$ is compact on $H^{⊥}$ . This closed subspace is Hilbert by [F1, F11]. It is self-adjoint, positive and has norm at most $1$ by step 1.3. If $T = 0$ , its norm is already less than $1$ ; this includes $H^{⊥} = {0}$ . Otherwise [F8] gives an eigenvalue equal to $∥ T ∥$ or $- ∥ T ∥$ ; positivity excludes the negative value, and if $∥ T ∥ = 1$ its unit eigenvector would lie in $\ker (I - B) \cap H^{⊥} = {0}$ by step 2.1, a contradiction. Hence $r : = ∥ T ∥ < 1$ , and [F9] gives the bounded inverse $C : = (I - T)^{- 1} = \sum_{n \geq 0} T^{n}$ on $H^{⊥}$ , with $∥ C ∥ \leq (1 - r)^{- 1}$ .

4.1F1F7F9step 1.3step 2.1step 3.1algebra

The series $G : = T C = \sum_{n \geq 1} T^{n}$ converges in operator norm by [F9]. Each power $T^{n}$ is self-adjoint and positive: for $n = 2 m$ , $⟨ T^{n} x, x ⟩ = ∥ T^{m} x ∥^{2}$ , and for $n = 2 m + 1$ , it equals $⟨ T (T^{m} x), T^{m} x ⟩ \geq 0$ . Therefore $G$ is self-adjoint and positive. For any bounded sequence $(x_{n})$ in $H^{⊥}$ , boundedness of $C$ makes $(C x_{n})$ bounded; compactness of $T$ from step 3.1 gives a subsequence for which $G x_{n} = T C x_{n}$ converges, so [F7] proves compactness of $G$ . It is injective because both $T$ and $C$ are injective. For $f \in H^{⊥}$ , put $y = C f$ ; step 1.2 gives $G f = B y \in dom Δ^{''} \cap H^{⊥}$ and $Δ^{''} G f = (I - B) y = f$ .

5.1F1F2F9F10F13step 1.2step 4.1algebra∎

If $u \in dom Δ^{''} \cap H^{⊥}$ , self-adjointness of $Δ^{''}$ and $Δ^{''} h = 0$ for $h \in H$ imply $Δ^{''} u \in H^{⊥}$ . Both $u$ and $G Δ^{''} u$ lie in $dom Δ^{''}$ and have the same Laplacian by step 4.1, so their difference belongs to $H \cap H^{⊥} = {0}$ . Thus $G Δ^{''} u = u$ and $ran G = dom Δ^{''} \cap H^{⊥}$ . If $z ⊥ ran G$ , self-adjointness gives $⟨ x, G z ⟩ = 0$ for all $x \in H^{⊥}$ , hence $G z = 0$ and $z = 0$ ; [F13] now gives $\overline{ran G} = H^{⊥}$ . Finally, $∥ G f ∥_{H^{2}} = ∥ B (C f) ∥_{H^{2}} \leq 3 C_{0} ∥ C ∥ ∥ f ∥_{L^{2}}$ by step 1.2 and [F9].

Source notes

Demailly's Ch. VI §2 (2.2) states the compact Rellich inclusion on a compact manifold. The bundle-valued compactness step is assembled chartwise from the library's local compactness theorem. The construction of $B$ , the norm gap on $H^{⊥}$ , and the corrected Green range are established here from the exact operator-theoretic suppliers. Demailly's separate Ch. VI §3.3 Hodge statements assume a flat Hermitian connection and are not used for this result.

Depends on

Used by

Dependency tree · two levels

162 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 (author manuscript, Universite Grenoble Alpes) (standard reference, not scraped)