Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

An absolutely convergent multi-indexed power series is holomorphic and differentiates termwise

Statement

Fix m1, aCm, a polyradius r, a real M0 and coefficients c:NmC with

cαMk<mrkαkfor every multi-index α.

Then:

  1. for every θ with 0<θ<1 the series αcα(za)α converges absolutely and uniformly on Δθr(a), so its sum g is defined on Δr(a);
  2. g is holomorphic on Δr(a), with Dg(z)h=k<mbk(z)hk,bk(z)=ααkcα(za)αek, the kth series running over the multi-indices with αk1 and converging absolutely on Δr(a); equivalently zkg=bk;
  3. for every θ with 0<θ<1 the derived coefficients αkcα, re-indexed as a power series, obey a bound of the same shape on the polyradius θr, so the differentiation may be iterated; and every iterated complex partial derivative zβg:=z0β0zm1βm1g exists on Δr(a) with zβg(a)=β!cβ.

Facts & Assumptions

Given: The data above; Cm is read through Complex m-space and its real coordinate dictionary and polydiscs are those of Balls, polydiscs and the distinguished boundary in Cm.

[L1]

A multi-indexed series converges absolutely at z when the series along one, equivalently every, enumeration of Nm converges absolutely; the sum is independent of the enumeration; the box partial sums over BN={α:αkN} converge to it; and a dominated series with summable bounds converges absolutely and uniformly on the set (Multi-indexed power series in Cm and their absolute convergence).

[L2]

f is complex differentiable at z when there is a C-linear L with f(z+h)=f(z)+L(h)+r(h) and r(h)/h0; L is unique and written Df(z) (Holomorphic functions on an open subset of Cm).

[L3]

An R-linear T with T(h)=k<mckhk is C-linear, and for a differentiable f the coefficients are zkf (A real-linear functional on Cm is complex linear exactly when its antiholomorphic part vanishes, Wirtinger operators in Cm).

[L4]

An absolutely convergent complex series converges and every rearrangement has the same sum (Every absolutely convergent complex series converges, and rearrangements preserve its sum).

[L5]

If fn(x)Mn on a set with Mn convergent, then fn converges absolutely and uniformly there (Weierstrass M-test for complex-valued function series).

[L6]

A nonnegative series converges exactly when its partial sums are bounded above (A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum); for real r with r<1, krk=1/(1r) (For r<1, k0rk=1/(1r), and for r1 the series diverges); if 0akbk eventually and bk converges then ak converges (If 0akbk eventually, convergence of bk gives convergence of ak, and divergence of ak gives divergence of bk).

[L7]

For p>0 and rational α>0 the sequence kα/(1+p)k tends to 0, the numerator being the corresponding power of the canonical natural (For every p>0 and every positive rational α, nα/(1+p)n0).

[L8]

If f is holomorphic on D(a,R), 0<r<R and fK on the circle ζa=r, then f(n)(a)n!K/rn for every natural n (Cauchy's inequalities bound every derivative by a boundary bound on a compactly contained circle).

[L9]

(z+w)n=kn(nk)zkwnk for complex z,w and natural n, the binomial coefficients read as complex numbers (The binomial theorem over the complex field).

[L10]

Linear combinations and products of functions complex differentiable at a point are complex differentiable there with the usual formulas; constants have derivative 0 and the identity derivative 1 (Linearity, product, reciprocal, and quotient rules for complex derivatives); such functions are continuous (Complex differentiability at a point implies continuity there).

[L11]

Multi-indices satisfy α=k<mαk and α!=k<mαk! (Ck maps and multi-index derivative notation in Euclidean space), with 0!=1 and (j+1)!=j!(j+1) (The factorial n! and the falling factorial nk, defined by recursion in N).

[L12]

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

[L13]

Natural powers satisfy w0=1 and wj+1=wjw; negative integer powers need a nonzero base (Integer powers in the complex field).

[L14]

zw=zw and z+wz+w (Conjugation is an involutive real-field automorphism, zz=z2, and modulus is definite, multiplicative, and subadditive); finite sums and products satisfy the additivity, scaling and product laws (Laws of finite sums and finite products).

Proof

technique · direct
1.1

Fix θ with 0<θ<1. For zΔθr(a) the hypothesis and [L14] give cα(za)αMk<mθαk; the box sums of the right side are Mk<mjNθjM(1θ)m by [L14] and [L6], and every finite subset of Nm lies in a box, so [L6] makes the majorant series convergent and [L1] and [L5] give absolute and uniform convergence on Δθr(a). Since each zΔr(a) lies in some such closed polydisc, g is defined on Δr(a). This is claim 1.

givenL1L5L6L14
1.2

For 0<θ<θ1<1 and every k<m the series ααkθα1 converges: by [L7] the sequence j(θ/θ1)j1 is null, hence bounded by some Kθ, so jθj1Kθθ1j1 and [L6] with [L14] bounds the box sums of ααkθα1 by Kθ(1θ1)1(1θ)(m1); [L6] then gives convergence.

givenL6L7L14
1.3

Fix θ with 0<θ<1, a point z0Δθr(a) and θ with θ<θ<1; write w=z0a, so wkθrk. For hCm with h0 put η=maxk<mhk/rk and assume η(θθ)/2, which holds for all small h because hkh; then z0+hΔθr(a)Δr(a) by [L14].

givenL14
2.1

For each α let ϕα(τ)=k<m(wk+τhk)αk, a polynomial in τ of degree at most α by [L9] and [L13], hence entire, with ϕα(τ)=jαϕα,jτj and ϕα,j=ϕα(j)(0)/j! by [L10] and [L11]. In particular ϕα,0=wα and, by the product rule of [L10] and an induction on the number of factors ([L12]), ϕα,1=k<mαkwαekhk, terms with αk=0 being 0.

step 1.3L9L10L11L12L13
2.2

The series bk(z0)=ααkcαwαek converges absolutely: αkcαwαekMrk1αkθα1 by the hypothesis and [L14], and step 1.2 makes that majorant summable.

step 1.2step 1.3L1L14
3.1

Put T=(θθ)/η, so T2 by step 1.3. For τT and every k, wk+τhkθrk+Thkθrk by [L14], so ϕα(τ)k<m(θrk)αk there. Applying [L8] to ϕα on the disc of radius T gives ϕα,jk<m(θrk)αkTj.

step 1.3step 2.1L8L14
4.1

Hence Rα:=ϕα(1)ϕα,0ϕα,1=2jαϕα,j satisfies Rαk<m(θrk)αkj2Tj2T2k<m(θrk)αk, using T2 and [L6]. With T2=η2(θθ)2 this is 2η2(θθ)2k<m(θrk)αk.

step 3.1L6L14
5.1

Summing against the coefficients, the hypothesis on cα gives αcαRα2η2M(θθ)2αk<mθαk=2η2M(θθ)2(1θ)m by [L6] and [L14]; since ηh/mink<mrk, this is at most a constant times h2.

step 1.3step 4.1L6L14
6.1

By steps 2.1, 5.1 and 2.2, and by [L1] and [L4] which allow the absolutely convergent series to be split term by term, g(z0+h)g(z0)k<mbk(z0)hk=αcαRα, whose modulus is O(h2) and therefore o(h). The map hk<mbk(z0)hk is C-linear by [L3] and [L15], so [L2] makes g complex differentiable at z0 with that differential, and zkg(z0)=bk(z0) by [L3]. As θ<1 and z0 were arbitrary, this is claim 2.

step 2.1step 5.1step 2.2L1L2L3L4L15
7.1

For claim 3 fix k<m and θ with 0<θ<1, and re-index the derived series by β=αek, so its coefficient at β is (βk+1)cβ+ek, of modulus at most M(βk+1)θβ+1l<m(θrl)βlrk1 by the hypothesis and [L14]. By [L7] the numbers (βk+1)θβ+1 are bounded by a constant M, so the derived coefficients satisfy a bound of the same shape with polyradius θr and constant MM/rk.

step 6.1L7L14
8.1

Iterating step 7.1 and step 6.1, an induction on β ([L12]) shows that every zβg exists on Δr(a) and is the termwise β-fold derived series, whose coefficient at αβ is (k<mαk(αk1)(αkβk+1))cα and which vanishes unless αβ componentwise. Evaluating at z=a, [L13] kills every monomial (za)αβ except the one with α=β, whose coefficient is β!cβ by [L11]; so zβg(a)=β!cβ.

step 6.1step 7.1L11L12L13L14

Depends on

Used by

Dependency tree · two levels

136 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