Alphabeta Math

Complex Power Series and Analytic Functions

About this page
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.

✓ 26 results · all verified · 16 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 10 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.
1 · Prerequisites
Abstract Algebra
Combinatorics
Complex Analysis
Linear Algebra
Real Analysis
Set Theory
Topology
2 · Logical flowchart

3 · Items

Definition

Complex analytic functions as locally representable by convergent power series

Definition

Uniform convergence and the uniformly Cauchy condition for complex-valued functions, with the componentwise dictionary

Theorem

A sequence of complex-valued functions converges uniformly if and only if it is uniformly Cauchy

Theorem

A uniform limit of continuous complex-valued functions is continuous

Theorem

Weierstrass M-test for complex-valued function series

Theorem

A complex power series converges absolutely and uniformly on every closed subdisc strictly inside its disc of convergence

Lemma

A complex power series, its formal derivative, and its zero-constant-term formal antiderivative have the same radius

Theorem

Inside its disc of convergence a complex power series is holomorphic and may be differentiated term by term

Corollary

A complex power-series sum has complex derivatives of every order, obtained by repeated termwise differentiation

Corollary

The coefficients of a complex power series are its derivatives at the centre divided by the corresponding factorials

Corollary

A complex power-series representation about a fixed centre has unique coefficients

Theorem

Every complex analytic function is holomorphic

Lemma

The binomial double series for re-expanding a complex power series is absolutely convergent and may be regrouped

Theorem

A complex power-series sum re-expands about every interior point, at least to the distance from that point to the original boundary

Corollary

The sum of a complex power series is analytic throughout its open disc of convergence

Proposition

Sums and scalar multiples of convergent complex power series are represented coefficientwise on the common disc

Proposition

Products of convergent complex power series are represented by their Cauchy-product coefficients on the common disc

Lemma

A composition of convergent complex power series has a convergent local power-series expansion when the inner sum maps the centre to the outer centre

Lemma

A convergent complex power series with nonzero constant term has a convergent reciprocal power series locally

Theorem

Complex analytic functions are closed under finite linear combinations, products, quotients with nonzero denominator, and composition

Corollary

Every complex analytic function has a primitive on a neighbourhood of each point

Theorem

The exponential definitions of complex sine, cosine, hyperbolic sine, and hyperbolic cosine equal their entire power series

Corollary

Complex sine, cosine, hyperbolic sine, and hyperbolic cosine are entire with their standard derivatives

Corollary

The addition formulas for complex trigonometric and hyperbolic functions

Theorem

Complex sine and cosine are unbounded on the complex plane

Theorem

The zeros of complex sine are the integer multiples of pi, and the zeros of complex cosine are the odd half-integer multiples of pi

Definition

Stolz approach regions at the boundary point 1 of the unit disc

Lemma

Abel summation by parts for complex coefficients and their partial sums

Theorem

Abel's limit theorem: a convergent complex series is recovered by its power series along every Stolz approach to 1

Sources