Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 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.

Holomorphic functions of several variables are smooth and their complex derivatives are holomorphic

Statement

Let m≥1, let U⊆Cm be open and let f:U→C be holomorphic. Then:

  1. every point a∈U has a polydisc Δr(a)⊆U on which f(z)=∑αcα(z−a)α with the series absolutely convergent, and the coefficients are cα=∂zαf(a)α!,∂zα:=∂z0α0⋯∂zm−1αm−1;
  2. every iterated complex partial derivative ∂zαf exists and is holomorphic on U;
  3. ∂xkf=∂zkf and ∂ykf=i ∂zkf for every k<m, and f is of class Cn in the real coordinates for every natural n, hence smooth.

Facts & Assumptions

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

[L1]

A continuous separately holomorphic function on an open set is holomorphic, and for a continuous function holomorphy, separate holomorphy and local power-series representability agree (Osgood's lemma: continuous and separately holomorphic implies holomorphic).

[L2]

For f continuous and separately holomorphic on Δρ(a) and rk<ρk, there are coefficients with ∣cα∣≤M∏k<mrk−αk and f=∑αcα(z−a)α on Δr(a) (A continuous separately holomorphic function is the sum of an absolutely convergent power series with Cauchy-integral coefficients on every smaller polydisc).

[L3]

Under such a coefficient bound the sum is holomorphic on Δr(a), differentiates termwise with ∂zk, the derived series obeys a bound of the same shape on every smaller polyradius, every iterated ∂zβ of the sum exists, and ∂zβ(sum)(a)=β! cβ (An absolutely convergent multi-indexed power series is holomorphic and differentiates termwise).

[L4]

A holomorphic function of several variables is continuous and separately holomorphic, with Df(a)h=∑k<m(∂zkf(a))hk (A holomorphic function of several variables is continuous and separately holomorphic).

[L5]

∂zkf=12(∂xkf−i∂ykf) and ∂zˉkf=12(∂xkf+i∂ykf) (Wirtinger operators in Cm).

[L6]

An R-linear T has the unique representation T(h)=∑kck′hk+∑kdk′hk‾ and is C-linear exactly when every dk′=0; for a real totally differentiable f these coefficients are ∂zkf and ∂zˉkf (A real-linear functional on Cm is complex linear exactly when its antiholomorphic part vanishes).

[L7]

If a property holds at 0 and passes from n to n+1, it holds for every natural number (The principle of mathematical induction).

[L8]

Complex differentiability at a gives real total differentiability at a with the same differential (Holomorphic functions on an open subset of Cm).

[L9]

f is of class Cn on an open subset of R2m when every iterated coordinate partial derivative of order at most n exists and is continuous (Ck maps and multi-index derivative notation in Euclidean space), and α!=∏k<mαk! with 0!=1 (The factorial n! and the falling factorial nk‾, defined by recursion in N).

[L10]

A complex differentiable function is continuous (Complex differentiability at a point implies continuity there).

[L11]

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

Proof

technique · direct
1.1givenL1L2L4L11

By [L4] the function f is continuous and separately holomorphic on U, so the construction inside the proof of [L1] gives, at each a∈U, a polydisc Δρ(a)⊆U and then rk=ρk/2 for which [L2] supplies coefficients with ∣cα∣≤M∏k<mrk−αk and f=∑αcα(z−a)α on Δr(a).

1.2givenL4L5L6L8

By [L6] and [L8] the C-linearity of Df(a) makes every ∂zˉkf(a) vanish, so [L5] gives ∂xkf=∂zkf+∂zˉkf=∂zkf and ∂ykf=i(∂zkf−∂zˉkf)=i ∂zkf at every point of U.

2.1step 1.1L3L9

By [L3] applied to that series, f differentiates termwise on Δr(a), every iterated ∂zαf exists there, and ∂zαf(a)=α! cα; dividing by α!≠0 ([L9]) gives claim 1.

3.1step 1.1step 2.1L3L7

By [L3] the derived series for ∂zkf again obeys a bound of the same shape on a smaller polyradius, so its sum is holomorphic there; since that sum is ∂zkf by step 2.1, each ∂zkf is holomorphic on a polydisc about every point of U, hence holomorphic on U. An induction on ∣α∣ ([L7]) repeats this for every iterated derivative, giving claim 2.

4.1step 1.2step 3.1L7L9L10∎

By step 1.2 each first-order real partial derivative of f is ∂zkf or i ∂zkf, which step 3.1 makes holomorphic and [L10] makes continuous; applying step 1.2 to those functions in turn, an induction on the order ([L7]) shows every iterated real coordinate partial derivative of f exists and is continuous on U. Taking real and imaginary parts, which are continuous together with f, [L9] makes f of class Cn for every natural n, which is claim 3.

Depends on

Used by

Dependency tree · two levels

84 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