LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-02

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.

The Cauchy product of two absolutely convergent complex series converges absolutely to the product of their sums

Statement

If $\sum a_n=A$ and $\sum b_n=B$ converge absolutely in $\mathbb C$ , and $c_n=\sum_{k\le n}a_kb_{n-k}$ , then $\sum c_n$ converges absolutely and has sum $AB$ . The conventions and prerequisite facts used below are recorded in Every absolutely convergent complex series converges, and rearrangements preserve its sum, The complex plane is complete, and convergence is equivalent to convergence of real and imaginary parts, The complex numbers as $\mathbb R^2$ , with their arithmetic, real embedding, and imaginary unit, 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, Generalised associativity: in a monoid the product of a finite list does not depend on the bracketing, and in a commutative monoid it does not depend on the order of the factors either, If $\sum a_k$ and $\sum b_k$ both converge absolutely then their Cauchy product converges absolutely, with sum $AB$ , 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$ , Convergent series add and scale termwise, Conjugation laws, $z\overline z=|z|^2$ , multiplicativity of modulus, and the triangle inequality.

Facts & Assumptions

Given: Absolutely convergent complex series $(a_n)$ and $(b_n)$ .

Proof

technique · direct

1.1

Define $c_n$ by the recursive finite complex sum. Componentwise expansion is valid because complex addition and multiplication are coordinatewise polynomial formulas.

given

1.2

Put $d_n=\sum_{k\le n}|a_k||b_{n-k}|$ . The triangle and multiplicative modulus laws give $|c_n|\le d_n$ .

algebra

1.3

The real absolute Cauchy-product theorem makes $\sum d_n$ converge; comparison therefore makes $\sum|c_n|$ converge.

given

2.1

Expanding real and imaginary parts gives four real Cauchy products. Their sums combine by real series linearity to the two coordinates of $AB$ , and componentwise convergence identifies $\sum c_n=AB$ .

given∎

Depends on

Used by

exp(z+w)=exp z exp w, and the complex exponential extends the real exponential Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 132 results over 27 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. Lebl, Basic Analysis I: Complex Numbers and the Complex Exponential (standard reference, not scraped)