Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 m1, let UCm be open and let f:UC 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 UCm and a separately holomorphic, locally bounded f:UC; Cm is read through Complex m-space and its real coordinate dictionary.

[L1]

If f is separately holomorphic on Δρ(a) with fM there and 0<θ<1, then f(w)f(z)M1θ(k<mρk1)wz 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 zkak<rk and rk (Balls, polydiscs and the distinguished boundary in Cm).

Proof

technique · direct
1.1

Fix aU. Local boundedness and [L6] give ε>0 and M0 with B(a,ε)U and fM on B(a,ε), after intersecting the bounding neighbourhood with a ball inside U. Put ρk=ε/(2m); then Δρ(a)B(a,ε)U, since za2=k<mzkak2<mρ02=ε2/4 for zΔρ(a) by [L5] and the dictionary.

givenL5L6L7
2.1

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 fM there by step 1.1.

step 1.1L3L5
3.1

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

step 1.1step 2.1L1L5L6
4.1

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

step 3.1L4L6
5.1

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.

givenstep 4.1L1L2L3

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