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.
Complex series, absolute convergence, complex power series, and radius of convergence
Definition
A complex sequence is a function . Since the additive reduct of the complex field is a commutative monoid, the finite-list construction of The product of a finite list in a monoid, by recursion, with the empty product () equal to the identity, read additively, defines its complex partial sums by The superscript is omitted when the summands already make the codomain clear.
The complex series converges to when in the metric of The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane; then is its sum. This is the same finite sum and convergence as the vector-series definition on in Series of vectors in , absolute convergence, rearrangement, and the set of rearrangement sums. The series converges absolutely when the real series of Series, partial sums, convergence and the sum, divergence, and the tail series converges. For a bijection , its rearrangement along is the complex series .
Let be a complex sequence and . The complex power series centered at with coefficients is with powers from Integer powers in the complex field and the preceding complex partial sums. To define its radius without ambiguity, form the specific real power series centered at . The radius of convergence of the complex power series is, by definition, the radius of this in A real power series about a centre, its interval of convergence, and its radius in . Thus the coefficient sequence, real variable, and center of the comparison series are all explicit.
Depends on
- $\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)$
- 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
- The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane
- Integer powers in the complex field
- Series of vectors in $\mathbb{R}^n$, absolute convergence, rearrangement, and the set of rearrangement sums
- A real power series about a centre, its interval of convergence, and its radius in $[0,+\infty]$
- Series, partial sums, convergence and the sum, divergence, and the tail series
Used by
- A locally uniformly convergent series of holomorphic functions may be differentiated term by term Corollary
- Uniform convergence on the closed unit disc does not give a holomorphic extension to a larger disc Counterexample
- Complex analytic functions as locally representable by convergent power series Definition
- Formal complex polynomials, evaluation, degree, leading coefficient, and monic polynomials Definition
- Multi-indexed power series in ℂᵐ and their absolute convergence Definition
- The complex exponential by its power series Definition
- The Taylor series of a holomorphic function at a point Definition
- A complex power series, its formal derivative, and its zero-constant-term formal antiderivative have the same radius Lemma
- Abel summation by parts for complex coefficients and their partial sums Lemma
- The Cauchy kernel expands as an absolutely and uniformly convergent multi-indexed geometric series Lemma
- Cauchy-Hadamard for complex power series, including zero and infinite radius Theorem
- Every absolutely convergent complex series converges, and rearrangements preserve its sum Theorem
- Gleason Kahane Zelazko Theorem
Dependency tree · two levels
51 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, Basic Analysis I: Complex Numbers and the Complex Exponential (standard reference, not scraped)