LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16

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 for complex coefficients and their partial sums

Statement

Let $a_{0}, \dots, a_{N} \in C$ , let $s_{n} = \sum_{k = 0}^{n} a_{k}$ , and put $s_{- 1} = 0$ . For complex weights $b_{0}, \dots, b_{N}$ , $\sum_{n = 0}^{N} a_{n} b_{n} = s_{N} b_{N} + \sum_{n = 0}^{N - 1} s_{n} (b_{n} - b_{n + 1}) .$ More generally, for $0 \leq p \leq q$ , $\sum_{n = p}^{q} a_{n} b_{n} = s_{q} b_{q} - s_{p - 1} b_{p} + \sum_{n = p}^{q - 1} s_{n} (b_{n} - b_{n + 1}) .$

Facts & Assumptions

Given: Finite complex sequences $(a_{n})$ and $(b_{n})$ with partial sums $s_{n}$ .

[L1]

Complex partial sums are the finite sums in the additive monoid of $C$ (Complex series, absolute convergence, complex power series, and radius of convergence).

[L2]

Finite products, read additively, have the empty and one-term conventions and obey the recursion defining finite sums (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).

Proof

technique · direct

1.1L1algebra

Since $a_{n} = s_{n} - s_{n - 1}$ , distributivity gives $\sum_{n = p}^{q} a_{n} b_{n} = \sum_{n = p}^{q} s_{n} b_{n} - \sum_{n = p}^{q} s_{n - 1} b_{n}$ .

2.1step 1.1L2algebra

Shift the second finite index and collect equal $s_{n}$ terms; the endpoints are $s_{q} b_{q}$ and $- s_{p - 1} b_{p}$ , while the interior terms are $s_{n} (b_{n} - b_{n + 1})$ .

3.1step 2.1L2∎

This is the tail identity. Taking $p = 0$ and $s_{- 1} = 0$ gives the first display; when $p = q$ the interior sum is empty and the identity remains valid.

Depends on

Used by

Dependency tree · two levels

14 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

L. Ahlfors, Complex Analysis, 3rd ed., Ch. 2, Abel's theorem (standard reference, not scraped)