LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

Abel summation by parts: with $A_{n} = \sum_{k < n} a_{k}$ one has $\sum_{k < n} a_{k} b_{k} = A_{n} b_{n - 1} - \sum_{k < n - 1} A_{k + 1} (b_{k + 1} - b_{k})$ for every $n \geq 1$

Statement

Let $(a_{k})$ and $(b_{k})$ be sequences of reals and let

$A_{n} : = \sum_{k < n} a_{k} (n \in N)$

be the partial sums of $\sum a_{k}$ (Series, partial sums, convergence and the sum, divergence, and the tail series, Finite sums and finite products, by recursion), so that $A_{0} = 0$ and $a_{k} = A_{k + 1} - A_{k}$ for every $k$ . Then for every natural number $n \geq 1$

$\sum_{k < n} a_{k} b_{k} = A_{n} b_{n - 1} - \sum_{k < n - 1} A_{k + 1} (b_{k + 1} - b_{k}) .$

Both sides are finite sums in the sense of Finite sums and finite products, by recursion; at $n = 1$ the right-hand sum is empty and the identity reads $a_{0} b_{0} = A_{1} b_{0}$ .

The hypothesis $n \geq 1$ is what makes the statement legitimate, not merely convenient: the index $n - 1$ occurs on the right, and $n - 1$ is a natural number exactly when $n \geq 1$ . At $n = 0$ there is nothing to state, both the left-hand side and $A_{0}$ being $0$ .

Facts & Assumptions

Given: Sequences $(a_{k})$ and $(b_{k})$ of reals and the partial sums $A_{n} = \sum_{k < n} a_{k}$ (Series, partial sums, convergence and the sum, divergence, and the tail series).

[L1]

Finite sums are defined by the recursion $\sum_{k < 0} x_{k} = 0$ and $\sum_{k < n + 1} x_{k} = \sum_{k < n} x_{k} + x_{n}$ (Finite sums and finite products, by recursion).

[L2]

The partial sums satisfy $A_{0} = 0$ and $A_{n + 1} = A_{n} + a_{n}$ for every $n$ , those being the two clauses of [L1] applied to $(a_{k})$ (Series, partial sums, convergence and the sum, divergence, and the tail series).

[L3]

Finite sums are additive and may be split at any intermediate index (Laws of finite sums and finite products).

[L4]

The principle of induction on $N$ (The principle of mathematical induction).

Proof

technique · induction

1.1L4

The claim to be proved by induction is the statement $P (m)$ : the displayed identity holds at $n = m + 1$ , that is $\sum_{k < m + 1} a_{k} b_{k} = A_{m + 1} b_{m} - \sum_{k < m} A_{k + 1} (b_{k + 1} - b_{k})$ . Every $n \geq 1$ is $m + 1$ for exactly one $m \in N$ , so proving $P (m)$ for all $m$ proves the lemma.

1.2L1L2base

$P (0)$ holds: the left-hand side is $\sum_{k < 1} a_{k} b_{k} = a_{0} b_{0}$ by [L1], while $A_{1} = A_{0} + a_{0} = a_{0}$ by [L2] and $\sum_{k < 0} A_{k + 1} (b_{k + 1} - b_{k}) = 0$ by [L1], so the right-hand side is $a_{0} b_{0} - 0$ .

1.3ih

Assume $P (m)$ for a fixed $m \in N$ .

1.4L1

By [L1], $\sum_{k < m + 2} a_{k} b_{k} = \sum_{k < m + 1} a_{k} b_{k} + a_{m + 1} b_{m + 1}$ .

1.5L1L3

By [L1], $\sum_{k < m + 1} A_{k + 1} (b_{k + 1} - b_{k}) = \sum_{k < m} A_{k + 1} (b_{k + 1} - b_{k}) + A_{m + 1} (b_{m + 1} - b_{m})$ .

1.6L2

By [L2], $A_{m + 2} = A_{m + 1} + a_{m + 1}$ , so $a_{m + 1} = A_{m + 2} - A_{m + 1}$ .

2.1step 1.3step 1.4

Substituting the induction hypothesis into step 1.4 gives $\sum_{k < m + 2} a_{k} b_{k} = A_{m + 1} b_{m} - \sum_{k < m} A_{k + 1} (b_{k + 1} - b_{k}) + a_{m + 1} b_{m + 1}$ .

2.2step 1.6algebra

Using step 1.6, $A_{m + 1} b_{m} + a_{m + 1} b_{m + 1} = A_{m + 1} b_{m} + A_{m + 2} b_{m + 1} - A_{m + 1} b_{m + 1} = A_{m + 2} b_{m + 1} - A_{m + 1} (b_{m + 1} - b_{m})$ .

3.1step 2.1step 2.2step 1.5algebra

Combining step 2.1 and step 2.2 and then step 1.5 gives $\sum_{k < m + 2} a_{k} b_{k} = A_{m + 2} b_{m + 1} - A_{m + 1} (b_{m + 1} - b_{m}) - \sum_{k < m} A_{k + 1} (b_{k + 1} - b_{k}) = A_{m + 2} b_{m + 1} - \sum_{k < m + 1} A_{k + 1} (b_{k + 1} - b_{k})$ , which is $P (m + 1)$ .

4.1step 1.2step 3.1L4discharge-induction∎

By [L4] applied to step 1.2 and step 3.1, $P (m)$ holds for every $m \in N$ , that is, the displayed identity holds for every $n \geq 1$ .

Remarks

What the identity is for. It converts a series $\sum a_{k} b_{k}$ , about which nothing is assumed, into a boundary term $A_{n} b_{n - 1}$ and a series $\sum A_{k + 1} (b_{k + 1} - b_{k})$ whose terms carry the differences of $(b_{k})$ . If $(A_{n})$ is bounded and $(b_{k})$ is monotone, those differences have one sign and telescope, which is exactly the situation of Dirichlet's test: if the partial sums of $\sum a_{k}$ are bounded and $(b_{k})$ is nonincreasing with $b_{k} \to 0$ , then $\sum a_{k} b_{k}$ converges. The transformation is the discrete analogue of integration by parts, and the boundary term is the analogue of the boundary term there.
The block form needs no separate proof. For $1 \leq M \leq n$ , subtracting the identity at $M$ from the identity at $n$ gives $\sum_{k = M}^{n - 1} a_{k} b_{k} = A_{n} b_{n - 1} - A_{M} b_{M - 1} - \sum_{k = M - 1}^{n - 2} A_{k + 1} (b_{k + 1} - b_{k})$ , using only splitting of finite sums (Laws of finite sums and finite products). Nothing on this page needs that form, so it is recorded here rather than stated as a result.
Two conventions are doing work. $A_{n}$ sums the $n$ terms $a_{0}, \dots, a_{n - 1}$ , so $A_{0} = 0$ and $a_{k} = A_{k + 1} - A_{k}$ with no shift (Series, partial sums, convergence and the sum, divergence, and the tail series); and the empty sum is $0$ (Finite sums and finite products, by recursion), which is what makes $n = 1$ a genuine instance of the identity rather than a case to be excluded.

Abel summation by parts: with $A_{n} = \sum_{k < n} a_{k}$ one has $\sum_{k < n} a_{k} b_{k} = A_{n} b_{n - 1} - \sum_{k < n - 1} A_{k + 1} (b_{k + 1} - b_{k})$ for every $n \geq 1$

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

Abel summation by parts: with An=∑k<nakAn​=∑k<n​ak​ one has ∑k<nakbk=Anbn−1−∑k<n−1Ak+1 (bk+1−bk)∑k<n​ak​bk​=An​bn−1​−∑k<n−1​Ak+1​(bk+1​−bk​) for every n≥1n≥1

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

Abel summation by parts: with $A_{n} = \sum_{k < n} a_{k}$ one has $\sum_{k < n} a_{k} b_{k} = A_{n} b_{n - 1} - \sum_{k < n - 1} A_{k + 1} (b_{k + 1} - b_{k})$ for every $n \geq 1$