CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 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.

First Cousin problem on a pseudoconvex domain

Statement

Assume the Axiom of Choice (AC). Let $n \geq 1$ and let $Ω \subseteq C^{n}$ be a Hartogs pseudoconvex domain (Plurisubharmonic exhaustions and Hartogs pseudoconvexity). Let $(U_{i})_{i \in I}$ be a locally finite open cover of $Ω$ and, for every $i \in I$ , let $m_{i}$ be a meromorphic function on $U_{i}$ (Meromorphic functions on an open set in complex Euclidean space) such that for all $i, j \in I$ the difference $m_{i} - m_{j}$ is holomorphic on $U_{i} \cap U_{j}$ (clause (c) of the definition of a meromorphic function).

Then there is a meromorphic function $G$ on $Ω$ such that $G - m_{i}$ is holomorphic on $U_{i}$ for every $i \in I$ . Equivalently, the first Cousin problem with the locally finite data $(m_{i})_{i \in I}$ is solvable: one global meromorphic function realizes the prescribed principal parts.

Facts & Assumptions

Given: The Axiom of Choice; an integer $n \geq 1$ ; a Hartogs pseudoconvex domain $Ω \subseteq C^{n}$ ; a locally finite open cover $(U_{i})_{i \in I}$ of $Ω$ ; meromorphic functions $m_{i}$ on $U_{i}$ with $m_{i} - m_{j}$ holomorphic on $U_{i} \cap U_{j}$ for all $i, j \in I$ ; the Wirtinger operators and the operators $\partial, \overset{ˉ}{\partial}$ on smooth forms of Bigraded complex forms and the Dolbeault operators.

[F1]

A domain $Ω \subseteq C^{m}$ is Hartogs pseudoconvex when $z \mapsto - \log δ_{Ω} (z)$ is plurisubharmonic on $Ω$ (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).

[F2]

If $F$ is meromorphic on an open $U \subseteq C^{m}$ with domain $D$ and $h \in O (U)$ , then $F + h$ is meromorphic on $U$ (clause (d) of Meromorphic functions on an open set in complex Euclidean space); and $F$ is holomorphic on an open $V \subseteq U$ when some $H \in O (V)$ agrees with $F$ on $D \cap V$ (clause (c)).

[F3]

Meromorphy is a local condition: if every point of $U$ has a neighbourhood to which $F$ restricts as a meromorphic function, then $F$ is meromorphic on $U$ (Meromorphic functions on an open set in complex Euclidean space).

[F4]

Let $Ω \subseteq C^{n}$ be a domain and let $(U_{i})_{i \in I}$ be an open cover of $Ω$ . Then there are a locally finite open cover $(V_{k})_{k \in N}$ of $Ω$ refining $(U_{i})$ with $V_{k} \subseteq U_{i (k)}$ and smooth functions $χ_{k} \in C^{\infty} (Ω)$ with $0 \leq χ_{k} \leq 1$ , $supp χ_{k} \subseteq V_{k}$ , locally finite supports and $\sum_{k} χ_{k} = 1$ on $Ω$ (Locally finite smooth partitions of unity on domains).

[F5]

Let $Ω \subseteq C^{n}$ be Hartogs pseudoconvex and let $1 \leq q \leq n$ . Every smooth $\overset{ˉ}{\partial}$ -closed $(0, q)$ -form on $Ω$ is exact in the Dolbeault complex: there is a smooth $(0, q - 1)$ -form $ζ$ with $\overset{ˉ}{\partial} ζ = η$ (Positive-degree Dolbeault vanishing on pseudoconvex domains, claim 1).

[F6]

Let $U \subseteq C^{m}$ be open and $f : U \to C$ of class $C^{1}$ . Then $f$ is complex differentiable at $a \in U$ if and only if $\partial_{{\overset{ˉ}{z}}_{k}} f (a) = 0$ for every $k < m$ (clause 3 of For $C^{1}$ functions, holomorphy, complex linearity of the real derivative, and the Cauchy–Riemann system agree); 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}$ ).

[F7]

On smooth complex-valued forms $d = \partial + \overset{ˉ}{\partial}$ and ${\overset{ˉ}{\partial}}^{2} = 0$ (The d, partial and dbar identities); on a $(p, q)$ -form $η = \sum_{I, J} a_{I, J} d z^{I} \land d {\overset{ˉ}{z}}^{J}$ one has $\overset{ˉ}{\partial} η = \sum_{I, J, j} (\partial_{{\overset{ˉ}{z}}_{j}} a_{I, J}) d {\overset{ˉ}{z}}_{j} \land d z^{I} \land d {\overset{ˉ}{z}}^{J}$ , and components outside the bidegree range $0 \leq p, q \leq n$ are zero (Bigraded complex forms and the Dolbeault operators).

[F8]

AC is the statement that every family of nonempty sets has a choice function (The Axiom of Choice); in ZF, AC implies the Axiom of Countable Choice (AC implies DC implies countable choice), which selects one element from each family of nonempty sets indexed by $N$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Choice use. AC is the ambient hypothesis of the corollary. The partition-of-unity lemma [F4] selects cover members over its shell construction using AC and uses its countable instance for the finite lists and bumps; [F8] supplies that implication. This proof makes no additional selection.

Proof

technique · direct

1.1F4F8given

Apply [F4] to the cover $(U_{i})_{i \in I}$ : let $(V_{k})_{k \in N}$ be the resulting locally finite refinement with $V_{k} \subseteq U_{i (k)}$ , and let $χ_{k} \in C^{\infty} (Ω)$ be the associated smooth partition of unity with $0 \leq χ_{k} \leq 1$ , $supp χ_{k} \subseteq V_{k}$ , locally finite supports and $\sum_{k} χ_{k} = 1$ on $Ω$ . The countable-choice hypothesis of [F4] is discharged by the implication $A C \Rightarrow {A C}_{ω}$ from [F8].

1.2F2F4givenalgebra

For each fixed $j \in I$ define $f_{j} : = \sum_{k} χ_{k} (m_{j} - m_{i (k)})$ on $U_{j}$ as follows. By hypothesis the difference $m_{j} - m_{i (k)}$ is holomorphic on $U_{j} \cap U_{i (k)}$ , a set containing $V_{k} \cap U_{j}$ ; multiplying by the cutoff $χ_{k}$ , which vanishes outside $V_{k}$ , extends it by zero to a smooth function on $U_{j}$ , and the family $(supp χ_{k})$ is locally finite, so every point of $U_{j}$ has a neighbourhood on which only finitely many terms are nonzero; hence the sum $f_{j}$ is a well-defined element of $C^{\infty} (U_{j})$ .

2.1F2step 1.2givenalgebra

For $j, l \in I$ , evaluate on the dense open set where all relevant meromorphic representatives are defined. There each summand of $f_{j} - f_{l}$ equals $χ_{k} (m_{j} - m_{l})$ , so $f_{j} - f_{l} = (\sum_{k} χ_{k}) (m_{j} - m_{l}) = m_{j} - m_{l}$ there. The left side is continuous, and the right side has the given holomorphic extension to $U_{j} \cap U_{l}$ . Equality on the dense set and continuity give equality everywhere with that extension; in particular $f_{j} - f_{l}$ is holomorphic on the overlap.

3.1F6F7step 2.1step 1.2

Define $η$ on $U_{j}$ by $η : = \overset{ˉ}{\partial} f_{j}$ , a smooth $(0, 1)$ -form on $U_{j}$ by [F7] and step 1.2. For $j, l \in I$ the identity $f_{j} - f_{l} = m_{j} - m_{l}$ of step 2.1 gives $\overset{ˉ}{\partial} f_{j} - \overset{ˉ}{\partial} f_{l} = \overset{ˉ}{\partial} (m_{j} - m_{l})$ on $U_{j} \cap U_{l}$ , and $m_{j} - m_{l}$ is holomorphic there, so $\overset{ˉ}{\partial} (m_{j} - m_{l}) = 0$ by the Cauchy-Riemann system [F6] and [F7]. Hence $\overset{ˉ}{\partial} f_{j} = \overset{ˉ}{\partial} f_{l}$ on every overlap, so the local definitions glue to a well-defined smooth $(0, 1)$ -form $η \in Ω^{0, 1} (Ω)$ .

4.1F7step 3.1

On each $U_{j}$ one has $η = \overset{ˉ}{\partial} f_{j}$ with $f_{j}$ smooth, hence $\overset{ˉ}{\partial} η = {\overset{ˉ}{\partial}}^{2} f_{j} = 0$ on $U_{j}$ by [F7]; therefore $η$ is a smooth $\overset{ˉ}{\partial}$ -closed $(0, 1)$ -form on $Ω$ .

5.1F1F5F7step 4.1

Since $Ω$ is Hartogs pseudoconvex and $η \in Ω^{0, 1} (Ω)$ is smooth and $\overset{ˉ}{\partial}$ -closed, [F5] with $q = 1$ provides $ψ \in Ω^{0, 0} (Ω)$ with $\overset{ˉ}{\partial} ψ = η$ ; by the conventions of [F7] the space $Ω^{0, 0} (Ω)$ is the space $C^{\infty} (Ω)$ of smooth functions, so $ψ$ is a smooth function on $Ω$ .

6.1F6step 3.1step 5.1given

For each $j \in I$ put $F_{j} : = f_{j} - ψ$ on $U_{j}$ , a smooth function by step 1.2 and step 5.1; then $\overset{ˉ}{\partial} F_{j} = \overset{ˉ}{\partial} f_{j} - \overset{ˉ}{\partial} ψ = η - η = 0$ on $U_{j}$ by step 3.1 and step 5.1. Since $F_{j}$ is $C^{1}$ , the Cauchy-Riemann system [F6] makes $F_{j}$ complex differentiable at every point of $U_{j}$ , that is, holomorphic on $U_{j}$ .

7.1F2F3step 2.1step 6.1givenalgebra

Let $D_{i} \subseteq U_{i}$ be the open dense domain of the representative $m_{i}$ and put $D_{G} : = ⋃_{i} D_{i}$ , an open dense subset of $Ω$ . Define $G : D_{G} \to C$ by $G (z) : = m_{i} (z) - F_{i} (z)$ when $z \in D_{i}$ . On $D_{i} \cap D_{j}$ , the compatibility of the meromorphic differences and step 2.1 give $(m_{i} - F_{i}) - (m_{j} - F_{j}) = (m_{i} - m_{j}) - (f_{i} - f_{j}) = 0$ , so $G$ is well defined. It is holomorphic on $D_{G}$ because each local expression is holomorphic there. Near any point choose a chart $U_{i}$ and a local ratio $m_{i} = f / g$ on $W \subseteq U_{i}$ . On the dense open set $D_{i} \cap W \cap {g \neq 0}$ one has $G = (f - g F_{i}) / g$ ; both sides are holomorphic on $D_{G} \cap W \cap {g \neq 0}$ , so continuity extends this identity there. Thus $G$ has the required local ratio and [F3] makes it meromorphic on $Ω$ .

8.1

Finally $G - m_{j} = - F_{j}$ on the common domain $D_{G} \cap D_{j} = D_{j}$ for every $j \in I$ by the definition of $G$ , and $- F_{j}$ is a holomorphic extension to $U_{j}$ by step 6.1; thus the meromorphic function $G$ realizes the prescribed principal parts $(m_{i})_{i \in I}$ , as asserted. [step 6.1, step 7.1] $□$

Remarks

Local finiteness is not needed. The proof uses the locally finite cover $(U_{i})$ only as an input to the partition-of-unity lemma [F4], whose output is locally finite for an arbitrary open cover; the argument is verbatim valid for an arbitrary open cover $(U_{i})_{i \in I}$ with compatible meromorphic data, and the locally finite case stated here is the form promised by the scaffold.

Why the pseudoconvexity enters. The only analytic input is the smooth solvability of the $\overset{ˉ}{\partial}$ -equation for $(0, 1)$ -forms on $Ω$ , supplied here by [F5]. On the ball or on a polydisc this is the classical Dolbeault lemma; on a general Hartogs pseudoconvex domain it is the content of the in-pair corollary, and it is exactly the hypothesis that fails on $C^{2} ∖ {0}$ , where the Cousin-I data $1 / (z w)$ on the two coordinate complements is not solvable.

Holomorphy of the correction. The smooth solution $ψ$ of $\overset{ˉ}{\partial} ψ = η$ is used, not merely an $L^{2}$ solution: the local corrections $F_{j} = f_{j} - ψ$ must be $C^{1}$ so that the Cauchy-Riemann system [F6] applies, and this is why the smooth branch of the vanishing corollary [F5] is invoked.

Depends on

Used by

First Cousin gluing on the pseudoconvex domain ℂ Example

Dependency tree · two levels

82 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

Jiří Lebl, Tasty Bits of Several Complex Variables (standard reference, not scraped)
Jean-Pierre Demailly, Complex Analytic and Differential Geometry (standard reference, not scraped)
Harold P. Boas, Lecture Notes on Several Complex Variables (standard reference, not scraped)