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 , , a polyradius , a real and coefficients with
Then:
- for every with the series converges absolutely and uniformly on , so its sum is defined on ;
- is holomorphic on , with the th series running over the multi-indices with and converging absolutely on ; equivalently ;
- for every with the derived coefficients , re-indexed as a power series, obey a bound of the same shape on the polyradius , so the differentiation may be iterated; and every iterated complex partial derivative exists on with
Facts & Assumptions
Given: The data above; is read through Complex -space and its real coordinate dictionary and polydiscs are those of Balls, polydiscs and the distinguished boundary in .
A multi-indexed series converges absolutely at when the series along one, equivalently every, enumeration of converges absolutely; the sum is independent of the enumeration; the box partial sums over converge to it; and a dominated series with summable bounds converges absolutely and uniformly on the set (Multi-indexed power series in and their absolute convergence).
is complex differentiable at when there is a -linear with and ; is unique and written (Holomorphic functions on an open subset of ).
An -linear with is -linear, and for a differentiable the coefficients are (A real-linear functional on is complex linear exactly when its antiholomorphic part vanishes, Wirtinger operators in ).
An absolutely convergent complex series converges and every rearrangement has the same sum (Every absolutely convergent complex series converges, and rearrangements preserve its sum).
If on a set with convergent, then converges absolutely and uniformly there (Weierstrass M-test for complex-valued function series).
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 with , (For , , and for the series diverges); if eventually and converges then converges (If eventually, convergence of gives convergence of , and divergence of gives divergence of ).
For and rational the sequence tends to , the numerator being the corresponding power of the canonical natural (For every and every positive rational , ).
If is holomorphic on , and on the circle , then for every natural (Cauchy's inequalities bound every derivative by a boundary bound on a compactly contained circle).
for complex and natural , the binomial coefficients read as complex numbers (The binomial theorem over the complex field).
Linear combinations and products of functions complex differentiable at a point are complex differentiable there with the usual formulas; constants have derivative and the identity derivative (Linearity, product, reciprocal, and quotient rules for complex derivatives); such functions are continuous (Complex differentiability at a point implies continuity there).
Multi-indices satisfy and ( maps and multi-index derivative notation in Euclidean space), with and (The factorial and the falling factorial , defined by recursion in ).
If a property holds at and passes from to , it holds for every natural number (The principle of mathematical induction).
Natural powers satisfy and ; negative integer powers need a nonzero base (Integer powers in the complex field).
and (Conjugation is an involutive real-field automorphism, , 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).
Every satisfies in the standard basis (The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension ).
Proof
Fix with . For the hypothesis and [L14] give ; the box sums of the right side are by [L14] and [L6], and every finite subset of lies in a box, so [L6] makes the majorant series convergent and [L1] and [L5] give absolute and uniform convergence on . Since each lies in some such closed polydisc, is defined on . This is claim 1.
For and every the series converges: by [L7] the sequence is null, hence bounded by some , so and [L6] with [L14] bounds the box sums of by ; [L6] then gives convergence.
Fix with , a point and with ; write , so . For with put and assume , which holds for all small because ; then by [L14].
For each let , a polynomial in of degree at most by [L9] and [L13], hence entire, with and by [L10] and [L11]. In particular and, by the product rule of [L10] and an induction on the number of factors ([L12]), , terms with being .
The series converges absolutely: by the hypothesis and [L14], and step 1.2 makes that majorant summable.
Put , so by step 1.3. For and every , by [L14], so there. Applying [L8] to on the disc of radius gives .
Hence satisfies , using and [L6]. With this is .
Summing against the coefficients, the hypothesis on gives by [L6] and [L14]; since , this is at most a constant times .
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, , whose modulus is and therefore . The map is -linear by [L3] and [L15], so [L2] makes complex differentiable at with that differential, and by [L3]. As and were arbitrary, this is claim 2.
For claim 3 fix and with , and re-index the derived series by , so its coefficient at is , of modulus at most by the hypothesis and [L14]. By [L7] the numbers are bounded by a constant , so the derived coefficients satisfy a bound of the same shape with polyradius and constant .
Iterating step 7.1 and step 6.1, an induction on ([L12]) shows that every exists on and is the termwise -fold derived series, whose coefficient at is and which vanishes unless componentwise. Evaluating at , [L13] kills every monomial except the one with , whose coefficient is by [L11]; so .
Depends on
Multi-indexed power series in and their absolute convergence
Holomorphic functions on an open subset of
A real-linear functional on is complex linear exactly when its antiholomorphic part vanishes
Wirtinger operators in
Every absolutely convergent complex series converges, and rearrangements preserve its sum
Weierstrass M-test for complex-valued function series
A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum
For , , and for the series diverges
For every and every positive rational ,
If eventually, convergence of gives convergence of , and divergence of gives divergence of
Cauchy's inequalities bound every derivative by a boundary bound on a compactly contained circle
The binomial theorem over the complex field
Linearity, product, reciprocal, and quotient rules for complex derivatives
Complex differentiability at a point implies continuity there
maps and multi-index derivative notation in Euclidean space
The factorial and the falling factorial , defined by recursion in
The principle of mathematical induction
Integer powers in the complex field
Balls, polydiscs and the distinguished boundary in
Conjugation is an involutive real-field automorphism, , and modulus is definite, multiplicative, and subadditive
Laws of finite sums and finite products
Complex -space and its real coordinate dictionary
The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension