Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26
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.

Locally bounded and separately holomorphic implies holomorphic

Statement

Let m≥1, let U⊆Cm be open and let f:U→C be separately holomorphic and locally bounded: every point of U has a neighbourhood on which ∣f∣ is bounded. Then f is continuous on U and holomorphic on U.

The local-boundedness hypothesis is used, and it is not shown here to be removable: this page carries no theorem that separate holomorphy alone implies holomorphy, and none of its results is applied as if it did.

Facts & Assumptions

Given: An open U⊆Cm and a separately holomorphic, locally bounded f:U→C; Cm is read through Complex m-space and its real coordinate dictionary.

[L1]

If f is separately holomorphic on Δρ(a) with ∣f∣≤M there and 0<θ<1, then ∣f(w)−f(z)∣≤M1−θ(∑k<mρk−1)∥w−z∥ for z,w∈Δ‾θρ(a), so f is Lipschitz there (A bounded separately holomorphic function on a polydisc is Lipschitz on every smaller polydisc).

[L2]

A continuous separately holomorphic function on an open subset of Cm is holomorphic (Osgood's lemma: continuous and separately holomorphic implies holomorphic).

[L3]

Separate holomorphy is a condition on the slices through each point of the domain (Separately holomorphic functions), and holomorphic means complex differentiable at every point (Holomorphic functions on an open subset of Cm).

[L4]

A function whose restrictions to the members of an open cover are continuous is continuous (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous).

[L5]

Δr(a) and Δ‾r(a) are defined coordinatewise by ∣zk−ak∣<rk and ≤rk (Balls, polydiscs and the distinguished boundary in Cm).

Proof

technique · direct
1.1givenL5L6L7

Fix a∈U. Local boundedness and [L6] give ε>0 and M≥0 with B(a,ε)⊆U and ∣f∣≤M on B(a,ε), after intersecting the bounding neighbourhood with a ball inside U. Put ρk=ε/(2m); then Δρ(a)⊆B(a,ε)⊆U, since ∥z−a∥2=∑k<m∣zk−ak∣2<mρ02=ε2/4 for z∈Δρ(a) by [L5] and the dictionary.

2.1step 1.1L3L5

The restriction of f to Δρ(a) is separately holomorphic by [L3], since a slice domain inside Δρ(a) is an open subset of the corresponding slice domain inside U and a restriction of a one-variable holomorphic function to an open subset is holomorphic; and ∣f∣≤M there by step 1.1.

3.1step 1.1step 2.1L1L5L6

Applying [L1] with θ=12, the function f is Lipschitz, hence continuous, on Δ‾ρ/2(a), and in particular on the open set Δρ/2(a), which contains a and is open by [L5] and [L6].

4.1step 3.1L4L6

The sets Δρ/2(a) obtained in step 3.1 as a ranges over U form an open cover of U on each member of which f is continuous, so f is continuous on U by [L4].

5.1givenstep 4.1L1L2L3∎

By step 4.1 the function f is continuous on U and separately holomorphic by hypothesis, so [L2] makes it holomorphic on U. The bound M entered only through step 1.1 and [L1]; nothing above removes it, and this page proves no statement that would.

Depends on

Used by

Dependency tree · two levels

64 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