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.
Multi-indexed power series in and their absolute convergence
Definition
Fix and read through Complex -space and its real coordinate dictionary. A multi-index is , with and as in maps and multi-index derivative notation in Euclidean space, every index running over from . For the complex monomial is
a finite product in the multiplicative commutative monoid of (The product of a finite list in a monoid, by recursion, with the empty product () equal to the identity, is a field, every element is uniquely , and every nonzero element has inverse ) of natural powers in (Integer powers in the complex field); for the zero multi-index .
Enumerating the index set. is countable and Every finite power of an at most countable set is at most countable makes at most countable; it is infinite, so there is a bijection (Injection, surjection, bijection, Finite, countably infinite, countable, uncountable).
Let and . The multi-indexed power series converges absolutely at when the complex series converges absolutely (Complex series, absolute convergence, complex power series, and radius of convergence) for one bijection , equivalently for every one. The two conditions agree, and the sums agree, because for bijections the series along is a rearrangement of the series along : applying Every absolutely convergent complex series converges, and rearrangements preserve its sum to the nonnegative series of moduli transfers convergence, and applying it again to the series itself transfers the sum. That common value is written and no other notion of unordered sum is introduced.
Box partial sums. For put , a finite set, and let be the corresponding finite sum (A finite sum in a commutative monoid indexed by an arbitrary finite set). If the series converges absolutely at with sum , then . Given , absolute convergence supplies with and ; taking large enough that contains , every index of outside that finite list is for some , so . The same argument bounds and the tail of the series by the corresponding tails of the series of moduli.
The series converges absolutely and uniformly on a set when there are reals with for every and every , and with convergent. By Weierstrass M-test for complex-valued function series the partial sums along then converge uniformly on (Uniform convergence and the uniformly Cauchy condition for complex-valued functions, with the componentwise dictionary) and the series converges absolutely at every point of .
Remarks
Why a bijection is fixed rather than an unordered sum defined. The library already has one theory of complex series and one rearrangement theorem, and the clause above uses exactly those. Introducing a separate notion of summation over would create a second convergence notion that every later statement would have to be matched against; instead every multi-indexed sum below means the sum of the one-variable series along any enumeration, which the rearrangement theorem makes unambiguous.
Where the series live. The natural regions here are the polydiscs of Balls, polydiscs and the distinguished boundary in rather than balls. If every is positive, absolute convergence at controls the series on the closed polydisc with that polyradius. If some coordinate is zero, the same coordinatewise domination holds on the corresponding degenerate product set, but that radius vector is not called a polyradius. This is exactly the shape the kernel expansion and the Cauchy estimates on this page produce.
Depends on
- Complex $m$-space and its real coordinate dictionary
- Balls, polydiscs and the distinguished boundary in $\mathbb{C}^m$
- $C^k$ maps and multi-index derivative notation in Euclidean space
- Complex series, absolute convergence, complex power series, and radius of convergence
- Every absolutely convergent complex series converges, and rearrangements preserve its sum
- Every finite power of an at most countable set is at most countable
- Injection, surjection, bijection
- Integer powers in the complex field
- Weierstrass M-test for complex-valued function series
- Uniform convergence and the uniformly Cauchy condition for complex-valued functions, with the componentwise dictionary
- Finite, countably infinite, countable, uncountable
- A finite sum in a commutative monoid indexed by an arbitrary finite set
- The product $g_0 g_1 \cdots g_{n-1}$ of a finite list in a monoid, by recursion, with the empty product ($n = 0$) equal to the identity
- $\mathbb C=\mathbb R[x]/(x^2+1)$ is a field, every element is uniquely $a+bi$, and every nonzero element has inverse $(a-bi)/(a^2+b^2)$
Used by
- The coefficients of a convergent multi-indexed power series are its derivative coefficients, hence unique Corollary
- 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
- The power series of z₀z₁ on a bidisc centred away from the origin Example
- The Cauchy kernel expands as an absolutely and uniformly convergent multi-indexed geometric series Lemma
- Conventions on this page, and what the several-variable identity theorem does not say Remark
- A continuous separately holomorphic function is the sum of an absolutely convergent power series with Cauchy-integral coefficients on every smaller polydisc Theorem
- An absolutely convergent multi-indexed power series is holomorphic and differentiates termwise Theorem
- Osgood's lemma: continuous and separately holomorphic implies holomorphic Theorem
Dependency tree · two levels
67 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)
- H. P. Boas, Lecture Notes on Multidimensional Complex Analysis, Ch. 2 (standard reference, not scraped)