LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Separately holomorphic functions vanishing on a real box are zero

Statement

Let $n \geq 1$ and let $G : C^{n} \to C$ be separately holomorphic: for every $j$ and every fixed $w \in C^{n}$ , the one-variable map $z \mapsto G (w_{1}, \dots, w_{j - 1}, z, w_{j + 1}, \dots, w_{n})$ is entire on $C$ . If there are nondegenerate intervals $I_{1}, \dots, I_{n} \subseteq R$ with $G = 0$ on $I_{1} \times \dots \times I_{n}$ , then $G \equiv 0$ on $C^{n}$ .

Facts & Assumptions

Given: An integer $n \geq 1$ , a separately holomorphic $G : C^{n} \to C$ , and nondegenerate intervals $I_{1}, \dots, I_{n}$ (that is, each $I_{j}$ contains a nonempty open subinterval, so it has more than one point) with $G = 0$ on $I_{1} \times \dots \times I_{n}$ .

[F1]

Identity theorem: if two functions holomorphic on a complex domain $Ω \subseteq C$ agree on a set having an accumulation point in $Ω$ , then they agree on $Ω$ (Identity theorem for holomorphic functions).

[F2]

A function is entire when it is complex differentiable on all of $C$ , that is, holomorphic on the domain $C$ ; a separately holomorphic $G$ has every one-variable slice entire by hypothesis (Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions).

[F3]

If $J \subseteq R$ has nonempty interior and $p$ lies in that interior, then $p$ is an accumulation point of $J$ in $C$ : some open ball $(p - ε, p + ε)$ is contained in $J$ , and for every neighbourhood radius $r > 0$ , $p + \min (ε, r) / 2$ is a point of $J$ different from $p$ within that neighbourhood. Every coordinate slice of a separately holomorphic function is determined by the values it takes on such a set.

Proof

technique · induction on $n$

1.1baseF1F2F3given

Base case $n = 1$ . Here $G$ is an entire function of one variable and vanishes on the nondegenerate interval $I_{1}$ . Choose $p$ in the interior of $I_{1}$ ; by [F3], $p$ is an accumulation point in $C$ of the set where $G$ and the zero function agree, and both are entire [F2]. The identity theorem [F1] on the domain $C$ gives $G \equiv 0$ .

1.2ihgivenchoose

Inductive hypothesis and setup. Assume $n \geq 2$ and that the assertion holds for $n - 1$ variables. Choose $p \in int I_{1}$ , which is possible because $I_{1}$ is nondegenerate, and fix an arbitrary $z^{'} \in C^{n - 1}$ ; it remains to show $G (p, z^{'}) = 0$ .

2.1F2givenstep 1.2

The slice in the last $n - 1$ variables. The map $z^{'} \mapsto G (p, z^{'})$ on $C^{n - 1}$ is separately holomorphic, because each of its one-variable slices is a slice of $G$ with all other coordinates fixed, hence entire by [F2]. It vanishes on the box $I_{2} \times \dots \times I_{n}$ , whose factors are nondegenerate, so the induction hypothesis of step 1.2 applies and gives $G (p, z^{'}) = 0$ .

3.1step 2.1

Vanishing on a slab. The point $p \in int I_{1}$ in step 1.2 was chosen arbitrarily in the interior, so step 2.1 gives $G = 0$ on $int I_{1} \times C^{n - 1}$ .

4.1F1F2F3step 1.2step 3.1

The slice in the first variable. For the fixed $z^{'}$ of step 1.2, the one-variable map $w \mapsto G (w, z^{'})$ is entire by [F2] and vanishes on the nondegenerate interval $int I_{1}$ by step 3.1. Its zero set therefore has the accumulation point $p$ of [F3] inside the domain $C$ , and [F1] gives $G (w, z^{'}) = 0$ for every $w \in C$ .

5.1step 1.2step 4.1discharge-induction∎

Conclusion. Since $z^{'} \in C^{n - 1}$ was arbitrary in step 1.2, step 4.1 gives $G \equiv 0$ on $C^{n}$ , which discharges the induction step and completes the induction.

Depends on

Used by

Dependency tree · two levels

12 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

Calder Sheagren, Uncertainty Principles with Fourier Analysis (University of Chicago REU 2017, author PDF) (standard reference, not scraped)