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 $\mathbb{C}^m$ and their absolute convergence
- Holomorphic functions on an open subset of $\mathbb{C}^m$
- A real-linear functional on $\mathbb{C}^m$ is complex linear exactly when its antiholomorphic part vanishes
- Wirtinger operators in $\mathbb{C}^m$
- 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 $|r| < 1$, $\sum_{k \ge 0} r^k = 1/(1-r)$, and for $|r| \ge 1$ the series diverges
- For every $p > 0$ and every positive rational $\alpha$, $n^{\alpha}/(1+p)^n \to 0$
- If $0 \le a_k \le b_k$ eventually, convergence of $\sum b_k$ gives convergence of $\sum a_k$, and divergence of $\sum a_k$ gives divergence of $\sum b_k$
- 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
- $C^k$ maps and multi-index derivative notation in Euclidean space
- The factorial $n!$ and the falling factorial $n^{\underline{k}}$, defined by recursion in $\mathbb{N}$
- The principle of mathematical induction
- Integer powers in the complex field
- Balls, polydiscs and the distinguished boundary in $\mathbb{C}^m$
- Conjugation is an involutive real-field automorphism, $z\overline z=|z|^2$, and modulus is definite, multiplicative, and subadditive
- Laws of finite sums and finite products
- Complex $m$-space and its real coordinate dictionary
- The standard list $e : n \to F^{n}$ with $e_i(i) = 1_F$ and $e_i(j) = 0_F$ for $j \ne i$ is an ordered basis of $F^{n}$; hence $\dim_F F^{n} = n$, and $F^{0}$ is the zero space with basis $\varnothing$ and dimension $0$
Used by
- Holomorphic functions of several variables are smooth and their complex derivatives are holomorphic Corollary
- The coefficients of a convergent multi-indexed power series are its derivative coefficients, hence unique Corollary
- Cauchy estimates on a bidisc, computed and compared with the exact derivatives Example
- The power series of exp(z₀+z₁) on every bidisc Example
- The power series of z₀/(1-z₁) and the shape of its domain of convergence Example
- Osgood's lemma: continuous and separately holomorphic implies holomorphic Theorem
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
- J. Lebl, Tasty Bits of Several Complex Variables, §1.2 (standard reference, not scraped)