LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generated

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.

Cauchy products of absolutely convergent series multiply their sums

Statement

Let $\sum_{n \geq 0} a_{n} = A$ and $\sum_{n \geq 0} b_{n} = B$ be absolutely convergent real series. Define

c_{n} = \sum_{j = 0}^{n} a_{j} b_{n - j} .

Then $\sum_{n \geq 0} c_{n}$ converges absolutely and has sum $A B$ . Thus the product of the two series can be grouped by total degree without changing its sum.

Facts & Assumptions

Given: A Dedekind-complete ordered field and two absolutely convergent series.

[F1]

Dedekind-complete ordered real field: every nonempty bounded-above set has a least upper bound.

[L1]

Real and complex modulus product and triangle inequalities: $∣ x y ∣ = ∣ x ∣ ∣ y ∣$ and the triangle inequality holds.

Proof

1.1givenF1L1algebra

Put $A_{a b s} = \sum_{n \geq 0} ∣ a_{n} ∣$ and $B_{a b s} = \sum_{n \geq 0} ∣ b_{n} ∣$ . For every $N$ , the finite triangle inequality and [L1] give $\sum_{n = 0}^{N} ∣ c_{n} ∣ \leq \sum_{j + ℓ \leq N} ∣ a_{j} ∣ ∣ b_{ℓ} ∣ \leq (\sum_{j = 0}^{N} ∣ a_{j} ∣) (\sum_{ℓ = 0}^{N} ∣ b_{ℓ} ∣) \leq A_{a b s} B_{a b s} .$ These partial sums are increasing and bounded, so [F1] gives their supremum $S$ . For any $ε > 0$ , some partial sum exceeds $S - ε$ , since otherwise $S - ε$ would be an upper bound; monotonicity then puts every later partial sum between $S - ε$ and $S$ . Hence $\sum c_{n}$ converges absolutely.

2.1givenL1step 1.1algebra∎

Let $A_{N} = \sum_{j = 0}^{N} a_{j}$ , $B_{N} = \sum_{ℓ = 0}^{N} b_{ℓ}$ , and $C_{N} = \sum_{n = 0}^{N} c_{n} = \sum_{j + ℓ \leq N} a_{j} b_{ℓ}$ . The difference $A_{N} B_{N} - C_{N}$ is the sum over pairs $0 \leq j, ℓ \leq N$ with $j + ℓ > N$ . For each such pair, $j > N / 2$ or $ℓ > N / 2$ , so by [L1] $∣ A_{N} B_{N} - C_{N} ∣ \leq B_{a b s} \sum_{j > N / 2} ∣ a_{j} ∣ + A_{a b s} \sum_{ℓ > N / 2} ∣ b_{ℓ} ∣ ⟶ 0.$ Absolute convergence makes both tails tend to zero. The convergent sequence $A_{N}$ is bounded: beyond some index $∣ A_{N} - A ∣ < 1$ , and the finitely many earlier values have a finite maximum absolute value. Therefore $∣ A_{N} B_{N} - A B ∣ \leq ∣ A_{N} ∣ ∣ B_{N} - B ∣ + ∣ B ∣ ∣ A_{N} - A ∣ ⟶ 0.$ Together with $∣ A_{N} B_{N} - C_{N} ∣ \to 0$ , this gives $C_{N} \to A B$ . Thus the sum of the Cauchy product is $A B$ , proving the claim.

Depends on

Used by

Dependency tree · two levels

4 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

Jiří Lebl, Basic Analysis: Introduction to Real Analysis, Volume I, §2.6.4, Theorem 2.6.5 (standard reference, not scraped)