ExampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27

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.

For $|r| < 1$ the Cauchy product of $\sum r^{k}$ with itself is $\sum (k+1) r^{k}$ , with sum $1/(1-r)^{2}$

Example

Let $r \in \mathbb{R}$ with $|r| < 1$ and take $a_k = b_k = r^{k}$ (Integer powers $a^m$ ). Their Cauchy product (The Cauchy product of two series: $c_n = \sum_{k=0}^{n} a_k b_{n-k}$ ) is

$c_n \;=\; \sum_{k=0}^{n} r^{k} r^{\,n-k} \;=\; \sum_{k=0}^{n} r^{n} \;=\; \iota(n+1)\,r^{n},$

the sum of $n+1$ copies of the same number. Both factors converge absolutely (Absolutely convergent and conditionally convergent series, and the general starting index), so by If $\sum a_k$ and $\sum b_k$ both converge absolutely then their Cauchy product converges absolutely, with sum $AB$ the product series converges absolutely, with

$\sum_{n=0}^{\infty} (n+1)\,r^{n} \;=\; \Bigl(\sum_{k=0}^{\infty} r^{k}\Bigr)^{2} \;=\; \frac{1}{(1-r)^{2}} .$

This is the cheapest way to sum $\sum (n+1)r^{n}$ available at this point in the reading order: no differentiation of a power series is needed, only the geometric series and Mertens' theorem.

Facts & Assumptions

Given: A real $r$ with $|r| < 1$ , the sequences $a_k = b_k = r^{k}$ , and their Cauchy product $c_n = \sum_{k=0}^{n} a_k b_{n-k}$ (The Cauchy product of two series: $c_n = \sum_{k=0}^{n} a_k b_{n-k}$ ).

[L1]

Geometric series: for $|x| < 1$ , $\sum x^{k}$ converges with sum $1/(1-x)$ , the first term being $x^{0} = 1$ (For $|r| < 1$ , $\sum_{k \ge 0} r^k = 1/(1-r)$ , and for $|r| \ge 1$ the series diverges, Series, partial sums, convergence and the sum, divergence, and the tail series).

[L2]

Powers: $x^{0} = 1$ , $x^{n+1} = x^{n}x$ , and $x^{m+n} = x^{m}x^{n}$ (Integer powers $a^m$ , Laws of integer exponents).

[L3]

Absolute value: $|xy| = |x|\,|y|$ and $|1| = 1$ (Basic properties of the absolute value).

[L4]

Finite sums: $\sum_{k<n} \lambda = \iota(n)\lambda$ for a constant $\lambda$ , and $\sum_{k=0}^{n}x_k = \sum_{k<n+1}x_k$ (Laws of finite sums and finite products, Finite sums and finite products, by recursion, Canonical naturals are positive and strictly increasing).

[L5]

The principle of induction on $\mathbb{N}$ (The principle of mathematical induction).

[L6]

If both factors converge absolutely, the Cauchy product converges absolutely with sum the product of the sums (If $\sum a_k$ and $\sum b_k$ both converge absolutely then their Cauchy product converges absolutely, with sum $AB$ , Mertens' theorem: if $\sum a_k$ converges absolutely to $A$ and $\sum b_k$ converges to $B$ , their Cauchy product converges to $AB$ , Absolutely convergent and conditionally convergent series, and the general starting index).

Verification

technique · direct

1.1

An induction gives $|r^{k}| = |r|^{k}$ for every $k$ : at $k = 0$ both sides are $1$ , and $|r^{k+1}| = |r^{k}r| = |r^{k}|\,|r| = |r|^{k}|r| = |r|^{k+1}$ .

L2L3L5

1.2

For $k \le n$ , $r^{k}r^{\,n-k} = r^{k + (n-k)} = r^{n}$ , so $c_n = \sum_{k=0}^{n} r^{n} = \sum_{k<n+1} r^{n} = \iota(n+1)\,r^{n}$ , a sum of $n+1$ copies of the constant $r^{n}$ .

L2L4

2.1

Since $|r| < 1$ , both $\sum_k r^{k}$ and $\sum_k |r^{k}| = \sum_k |r|^{k}$ converge, the first with sum $1/(1-r)$ ; so $\sum_k r^{k}$ converges absolutely.

step 1.1L1

3.1

Both factors of the Cauchy product converge absolutely, so $\sum_n c_n$ converges absolutely with sum $\bigl(1/(1-r)\bigr)^{2} = 1/(1-r)^{2}$ .

step 2.1L6

4.1

By step 1.2 that series is $\sum_{n\ge0}(n+1)r^{n}$ , so it converges absolutely with sum $1/(1-r)^{2}$ .

step 1.2step 3.1∎

Remarks

The coefficient $n+1$ counts the antidiagonal. There are exactly $n+1$ pairs $(k, n-k)$ with $k \le n$ , and every one of them contributes the same product $r^{n}$ ; that is the whole computation of step 1.2, and it is why the answer is a count rather than a new expression.
Absolute convergence is available for free here. The terms are powers of a fixed $r$ , so $\sum |r^{k}|$ is again a geometric series. That is what lets If $\sum a_k$ and $\sum b_k$ both converge absolutely then their Cauchy product converges absolutely, with sum $AB$ apply rather than only Mertens' theorem: if $\sum a_k$ converges absolutely to $A$ and $\sum b_k$ converges to $B$ , their Cauchy product converges to $AB$ , and it gives absolute convergence of the product as well as its value.
Compare the failing case. In The Cauchy product of $\sum_{k \ge 0} (-1)^{k}/\sqrt{k+1}$ with itself has $|c_n| \ge 1$ for every $n$ , so it diverges the two factors again coincide, but neither converges absolutely, and the antidiagonal of $c_n$ has $n+1$ terms all of the same sign and not small enough; there the count $n+1$ is what destroys convergence rather than what produces a clean answer.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 100 results over 30 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

Cauchy product (Wikipedia) (standard reference, not scraped)
Geometric series (Wikipedia) (standard reference, not scraped)
John K. Hunter, An Introduction to Real Analysis, Chapter 4 (standard reference, not scraped)

For ∣r∣<1|r| < 1∣r∣<1 the Cauchy product of ∑rk\sum r^{k}∑rk with itself is ∑(k+1)rk\sum (k+1) r^{k}∑(k+1)rk, with sum 1/(1−r)21/(1-r)^{2}1/(1−r)2