Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicableSession-authored (Fable 5 assisted)judge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

Multi-indexed power series in Cm and their absolute convergence

Definition

Fix m1 and read Cm through Complex m-space and its real coordinate dictionary. A multi-index is αNm, with α=k<mαk and α!=k<mαk! as in Ck maps and multi-index derivative notation in Euclidean space, every index running over k<m from 0. For wCm the complex monomial is

wα:=k<mwkαk,

a finite product in the multiplicative commutative monoid of C (The product g0g1gn1 of a finite list in a monoid, by recursion, with the empty product (n=0) equal to the identity, C=R[x]/(x2+1) is a field, every element is uniquely a+bi, and every nonzero element has inverse (abi)/(a2+b2)) of natural powers in C (Integer powers in the complex field); for the zero multi-index w0=1.

Enumerating the index set. N is countable and Every finite power of an at most countable set is at most countable makes Nm at most countable; it is infinite, so there is a bijection σ:NNm (Injection, surjection, bijection, Finite, countably infinite, countable, uncountable).

Let c:NmC and a,zCm. The multi-indexed power series αcα(za)α converges absolutely at z when the complex series ncσ(n)(za)σ(n) 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 αcα(za)α and no other notion of unordered sum is introduced.

Box partial sums. For NN put BN:={αNm:αkN for every k<m}, a finite set, and let SN(z):=αBNcα(za)α be the corresponding finite sum (A finite sum in a commutative monoid indexed by an arbitrary finite set). If the series converges absolutely at z with sum S, then SN(z)S. Given ε>0, absolute convergence supplies n0 with nn0cσ(n)(za)σ(n)<ε and n<n0cσ(n)(za)σ(n)Sε; taking N large enough that BN contains σ(0),,σ(n01), every index of BN outside that finite list is σ(n) for some nn0, so SN(z)S2ε. The same argument bounds SN(z) and the tail of the series by the corresponding tails of the series of moduli.

The series converges absolutely and uniformly on a set SCm when there are reals Mα0 with cα(za)αMα for every zS and every α, and with nMσ(n) convergent. By Weierstrass M-test for complex-valued function series the partial sums along σ then converge uniformly on S (Uniform convergence and the uniformly Cauchy condition for complex-valued functions, with the componentwise dictionary) and the series converges absolutely at every point of S.

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 Nm 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 Cm rather than balls. If every zkak is positive, absolute convergence at z 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

Used by

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