LemmaStatement: AI-adaptedProof: AI-adaptedprecheck 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 $C$ , and $c_{n} = \sum_{k \leq n} a_{k} b_{n - k}$ , then $\sum c_{n}$ converges absolutely and has sum $A B$ . 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 $R [x] / (x^{2} + 1)$ , with the real embedding and imaginary unit $i$ , The product $g_{0} g_{1} \dots 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 $A B$ , If $0 \leq a_{k} \leq 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 is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive.

Facts & Assumptions

Given: Absolutely convergent complex series $(a_{n})$ and $(b_{n})$ .

Proof

technique · direct

1.1given

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

1.2algebra

Put $d_{n} = \sum_{k \leq n} ∣ a_{k} ∣ ∣ b_{n - k} ∣$ . The triangle and multiplicative modulus laws give $∣ c_{n} ∣ \leq d_{n}$ .

1.3given

The real absolute Cauchy-product theorem makes $\sum d_{n}$ converge; comparison therefore makes $\sum ∣ c_{n} ∣$ converge.

2.1given∎

Expanding real and imaginary parts gives four real Cauchy products. Their sums combine by real series linearity to the two coordinates of $A B$ , and componentwise convergence identifies $\sum c_{n} = A B$ .

Depends on

Dependency tree · 2 levels

Sources

J. Lebl, Basic Analysis I: Complex Numbers and the Complex Exponential