TheoremStatement: 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.

For a nonincreasing nonnegative sequence, $\sum a_{k}$ converges iff $\sum 2^{k} a_{2^{k}}$ converges

Statement

Let $(a_{k})_{k \geq 1}$ be a family from $1$ (Series, partial sums, convergence and the sum, divergence, and the tail series) with

$a_{k} \geq 0 (k \geq 1) and a_{j} \geq a_{k} whenever 1 \leq j \leq k .$

Then

$\sum_{k \geq 1} a_{k} converges ⟺ \sum_{j \geq 0} 2^{j} a_{2^{j}} converges .$

Every term of the condensed series is defined, because $2^{j} \geq 1$ for every $j \in N$ (Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ ), and the condensed series starts at $j = 0$ , its first term being $2^{0} a_{2^{0}} = a_{1}$ .

The monotonicity hypothesis is equivalent to the consecutive form $a_{k + 1} \leq a_{k}$ for every $k \geq 1$ , since it says that the sequence $b_{i} : = a_{i + 1}$ , $i \in N$ , is nonincreasing (Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences). It cannot be dropped: the companion page exhibits a nonnegative non-monotone family for which the two series behave differently.

Facts & Assumptions

Given: A family $(a_{k})_{k \geq 1}$ of reals with $a_{k} \geq 0$ for $k \geq 1$ and $a_{j} \geq a_{k}$ whenever $1 \leq j \leq k$ ; the partial sums $A_{n} = \sum_{k = 1}^{n} a_{k}$ of $\sum_{k \geq 1} a_{k}$ , with $A_{0} = 0$ ; and the partial sums $C_{n} = \sum_{j < n} 2^{j} a_{2^{j}}$ of the condensed series (Series, partial sums, convergence and the sum, divergence, and the tail series, Finite sums and finite products, by recursion).

[L1]

Splitting of finite sums, and the meaning of a sum with general bounds: for $m \leq n$ , $\sum_{k = 1}^{n} a_{k} = \sum_{k = 1}^{m} a_{k} + \sum_{k = m + 1}^{n} a_{k}$ , and $\sum_{k = p}^{q} a_{k} = \sum_{t < q + 1 - p} a_{p + t}$ (Laws of finite sums and finite products, Finite sums and finite products, by recursion).

[L2]

Monotonicity and scaling of finite sums: if $x_{t} \leq y_{t}$ for all $t < d$ then $\sum_{t < d} x_{t} \leq \sum_{t < d} y_{t}$ ; and a constant sum is $\sum_{t < d} λ = d λ$ (Laws of finite sums and finite products).

[L3]

Powers of $2$ : $2^{j} \geq 1$ for every $j \in N$ , $2^{j + 1} = 2 \cdot 2^{j}$ , and $2^{j} < 2^{j + 1}$ (Integer powers $a^{m}$ , Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ ).

[L4]

The principle of induction (The principle of mathematical induction).

[L5]

For a series of nonnegative terms: its partial sums are nondecreasing, it converges if and only if the range of its partial sums is bounded above, and in the convergent case every partial sum is at most the sum (A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum, Lower bound, bounded below, bounded set).

Proof

technique · direct

1.1

Every term of the condensed series is nonnegative, since $2^{j} \geq 1 > 0$ and $a_{2^{j}} \geq 0$ ; and every $A_{n}$ , every $C_{n}$ is nonnegative, both series having nonnegative terms.

givenL3L5

1.2

For every $n \in N$ the block from $2^{n}$ to $2^{n + 1} - 1$ is $\sum_{k = 2^{n}}^{2^{n + 1} - 1} a_{k} = \sum_{t < 2^{n}} a_{2^{n} + t}$ , since the number of terms is $(2^{n + 1} - 1) + 1 - 2^{n} = 2^{n}$ .

L1L3algebra

1.3

For every $n \in N$ the block from $2^{n} + 1$ to $2^{n + 1}$ is $\sum_{k = 2^{n} + 1}^{2^{n + 1}} a_{k} = \sum_{t < 2^{n}} a_{2^{n} + 1 + t}$ , since the number of terms is $2^{n + 1} + 1 - (2^{n} + 1) = 2^{n}$ .

L1L3algebra

1.4

Index growth: $n \leq 2^{n} - 1$ for every $n \in N$ , by induction on $n$ . At $n = 0$ this reads $0 \leq 0$ ; and if $n \leq 2^{n} - 1$ , that is $n + 1 \leq 2^{n}$ , then $n + 1 \leq 2^{n} \leq 2 \cdot 2^{n} - 1 = 2^{n + 1} - 1$ , the second inequality being $2^{n} \geq 1$ .

L3L4algebra

2.1

In the first block every index satisfies $2^{n} \leq 2^{n} + t$ , so $a_{2^{n} + t} \leq a_{2^{n}}$ , and therefore $\sum_{k = 2^{n}}^{2^{n + 1} - 1} a_{k} \leq \sum_{t < 2^{n}} a_{2^{n}} = 2^{n} a_{2^{n}}$ .

step 1.2givenL2

2.2

In the second block every index satisfies $2^{n} + 1 + t \leq 2^{n + 1}$ for $t < 2^{n}$ , so $a_{2^{n} + 1 + t} \geq a_{2^{n + 1}}$ , and therefore $\sum_{k = 2^{n} + 1}^{2^{n + 1}} a_{k} \geq \sum_{t < 2^{n}} a_{2^{n + 1}} = 2^{n} a_{2^{n + 1}}$ .

step 1.3givenL2L3

2.3

Suppose the condensed series converges, with sum $C$ ; then $C_{n} \leq C$ for every $n$ .

givenstep 1.1L5

2.4

Suppose conversely that $\sum_{k \geq 1} a_{k}$ converges, with sum $A$ ; then $A_{n} \leq A$ for every $n$ .

givenstep 1.1L5

3.1

Upper estimate: $A_{2^{n} - 1} \leq C_{n}$ for every $n \in N$ , by induction on $n$ . At $n = 0$ both sides are $0$ , since $2^{0} - 1 = 0$ and $C_{0}$ is the empty sum; and if $A_{2^{n} - 1} \leq C_{n}$ , then splitting at $2^{n} - 1$ gives $A_{2^{n + 1} - 1} = A_{2^{n} - 1} + \sum_{k = 2^{n}}^{2^{n + 1} - 1} a_{k} \leq C_{n} + 2^{n} a_{2^{n}} = C_{n + 1}$ .

step 2.1L1L3L4

3.2

Lower estimate: $2 A_{2^{n}} \geq \sum_{j = 1}^{n} 2^{j} a_{2^{j}}$ for every $n \in N$ , by induction on $n$ . At $n = 0$ the right-hand side is the empty sum $0$ and the left-hand side is $2 a_{1} \geq 0$ ; and if the inequality holds at $n$ , then splitting at $2^{n}$ gives $A_{2^{n + 1}} = A_{2^{n}} + \sum_{k = 2^{n} + 1}^{2^{n + 1}} a_{k} \geq A_{2^{n}} + 2^{n} a_{2^{n + 1}}$ , whence $2 A_{2^{n + 1}} \geq 2 A_{2^{n}} + 2^{n + 1} a_{2^{n + 1}} \geq \sum_{j = 1}^{n + 1} 2^{j} a_{2^{j}}$ .

step 2.2step 1.1L1L3L4

4.1

For every $N \in N$ we have $N \leq 2^{N} - 1$ , so $A_{N} \leq A_{2^{N} - 1} \leq C_{N} \leq C$ , the first inequality because the partial sums $A_{n}$ are nondecreasing.

step 1.4step 3.1step 2.3step 1.1L5

4.2

For every $n \in N$ , $\sum_{j = 1}^{n} 2^{j} a_{2^{j}} \leq 2 A_{2^{n}} \leq 2 A$ , and splitting the condensed partial sum at $j = 1$ gives $C_{n + 1} = a_{1} + \sum_{j = 1}^{n} 2^{j} a_{2^{j}} \leq a_{1} + 2 A$ .

step 3.2step 2.4L1L3

5.1

So the partial sums of $\sum_{k \geq 1} a_{k}$ are bounded above by $C$ , and that series converges.

step 4.1L5

5.2

Also $C_{0} = 0 \leq a_{1} + 2 A$ , so every condensed partial sum is at most $a_{1} + 2 A$ , and the condensed series converges.

step 4.2step 1.1L5

6.1

The two implications just established combine, so the two series converge or diverge together.

step 5.1step 5.2∎

Remarks

What monotonicity buys, in one sentence. It lets a block of $2^{n}$ consecutive terms be squeezed between $2^{n}$ copies of its last term and $2^{n}$ copies of its first, which is exactly the pair of estimates in steps 2.1 and 2.2. Without it a block carries no information about any single term in it, and the two series decouple entirely.
The factor $2$ in the lower estimate is not an artefact. The blocks used for the two estimates are different: the upper estimate groups $2^{n}, \dots, 2^{n + 1} - 1$ and the lower estimate groups $2^{n} + 1, \dots, 2^{n + 1}$ , and the second grouping produces $2^{n} a_{2^{n + 1}}$ , which is half of the condensed term $2^{n + 1} a_{2^{n + 1}}$ . Since only boundedness of the partial sums is at stake, a constant factor is harmless.
Base $2$ is a choice, not a necessity. The same argument with blocks of length $c^{n}$ gives the analogous test for any integer $c \geq 2$ . Base $2$ is taken here because it is the one every later application uses, and because the arithmetic of $2^{n + 1} = 2 \cdot 2^{n}$ keeps the induction free of extra bookkeeping.

Depends on

Used by

Dependency tree · two levels

42 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

Cauchy condensation test (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (3.27) (standard reference, not scraped)
Stephen Semmes, Elements of Analysis (standard reference, not scraped)

For a nonincreasing nonnegative sequence, ∑ak∑ak​ converges iff ∑2ka2k∑2ka2k​ converges