LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-07-31

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.

If $\iota(n+1)a_n\to0$ , short multiplicative blocks of the coefficients have uniformly small sums

Statement

Suppose $\iota(n+1)a_n\to0$ . For every $\varepsilon>0$ there is $N_0$ such that, whenever $q\ge p\ge N_0$ ,

$\sum_{n=p}^{q}|a_n|\le\varepsilon\frac{\iota(q-p+1)}{\iota(p+1)}.$

Moreover, for $N\ge N_0$ and $x_N:=1-1/\iota(N+1)$ ,

$\sum_{n=N_0}^{N}|a_n|(1-x_N^n)\le\varepsilon,\qquad \sum_{n>N}|a_n|x_N^n\le\varepsilon.$

Facts & Assumptions

Given: The Tauber condition $\iota(n+1)a_n\to0$ .

[L1]

The canonical naturals $\iota(n+1)$ are positive and strictly increasing, positive reciprocals reverse order, and $|uv|=|u||v|$ (Canonical naturals are positive and strictly increasing, Inverses of positives are positive, and reciprocation reverses order, Basic properties of the absolute value).

[L2]

Real-sequence convergence is tested with positive rational tolerances, and below every positive real lies a positive rational (Limits and Cauchy sequences of reals, The rationals embed densely in the reals).

[L3]

For $0\le x\le1$ , multiplying out the finite sum gives $1-x^n=(1-x)\sum_{k=0}^{n-1}x^k\le\iota(n)(1-x)$ .

[L4]

For $0\le x<1$ , the geometric-series formula gives $\sum_{n>N}x^n=x^{N+1}/(1-x)$ (For $|r| < 1$ , $\sum_{k \ge 0} r^k = 1/(1-r)$ , and for $|r| \ge 1$ the series diverges).

Proof

technique · direct

1.1

Choose a positive rational $\delta<\varepsilon$ . By the limit hypothesis and [L2], choose $N_0$ so that $|\iota(n+1)a_n|<\delta$ for $n\ge N_0$ . Positivity and multiplicativity in [L1] give $|a_n|<\delta/\iota(n+1)<\varepsilon/\iota(n+1)$ there. Since $1/\iota(n+1)\le1/\iota(p+1)$ on $p\le n\le q$ , summing proves the block estimate.

L1L2choosealgebra

2.1

For $N_0\le n\le N$ , [L3] gives $|a_n|(1-x_N^n)\le\varepsilon(1-x_N)$ . There are at most $N+1$ terms and $\iota(N+1)(1-x_N)=1$ , proving the first weighted estimate.

step 1.1L3algebra

3.1

For $n>N$ , step 1.1 gives $|a_n|\le\varepsilon/\iota(N+2)$ . Summing the geometric tail yields $\sum_{n>N}|a_n|x_N^n\le\varepsilon x_N^{N+1}\iota(N+1)/\iota(N+2)\le\varepsilon$ .

step 1.1L4algebra∎

Depends on

Used by

Tauber's theorem: an Abel-summable series with ι(n+1)aₙ→0 converges ordinarily to its Abel sum Theorem

Dependency tree · next 3 levels

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

Tauberian theorem, Encyclopedia of Mathematics (standard reference, not scraped)
Tauberian theorems, Encyclopedia of Mathematics (standard reference, not scraped)

If ι(n+1)an→0\iota(n+1)a_n\to0ι(n+1)an​→0, short multiplicative blocks of the coefficients have uniformly small sums