Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-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.

Abel's limit theorem: if a real series converges to ss, then its power series tends to ss as x↑1x\uparrow1

Statement

If the real series ∑n≥0an\sum_{n\ge0}a_n converges ordinarily to ss, then it is Abel summable to ss:

lim⁡x↑1∑n=0∞anxn=s.\lim_{x\uparrow1}\sum_{n=0}^{\infty}a_nx^n=s.

Facts & Assumptions

Given: Inclusive partial sums Sn:=∑k=0nakS_n:=\sum_{k=0}^{n}a_k with Sn→sS_n\to s.

[L1]

Finite Abel summation gives ∑k=0Nakxk=SNxN+(1−x)∑k=0N−1Skxk\sum_{k=0}^{N}a_kx^k=S_Nx^N+(1-x)\sum_{k=0}^{N-1}S_kx^k (Abel summation by parts: with An=∑k<nakA_n = \sum_{k<n} a_k one has ∑k<nakbk=Anbn−1−∑k<n−1Ak+1 (bk+1−bk)\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≥1n \ge 1).

[L2]

A convergent sequence is bounded (Every convergent sequence is bounded).

[L3]

∑n≥0xn=1/(1−x)\sum_{n\ge0}x^n=1/(1-x) for 0≤x<10\le x<1 (For ∣r∣<1|r| < 1, ∑k≥0rk=1/(1−r)\sum_{k \ge 0} r^k = 1/(1-r), and for ∣r∣≥1|r| \ge 1 the series diverges).

[L4]

A nonnegative series dominated termwise by a convergent nonnegative series converges (If 0≤ak≤bk0 \le a_k \le b_k eventually, convergence of ∑bk\sum b_k gives convergence of ∑ak\sum a_k, and divergence of ∑ak\sum a_k gives divergence of ∑bk\sum b_k).

Proof

technique · direct
1.1

By [L2], choose MM with ∣Sn∣≤M|S_n|\le M for every nn. For fixed 0≤x<10\le x<1, one has ∣Snxn∣≤Mxn|S_nx^n|\le Mx^n, so [L3] and [L4] give absolute convergence of ∑nSnxn\sum_nS_nx^n; the same bound gives SNxN→0S_Nx^N\to0.

L2L3L4choose
2.1

Apply [L1] and let N→∞N\to\infty. Step 1.1 gives convergence of the Abel series and A(x)=(1−x)∑n≥0SnxnA(x)=(1-x)\sum_{n\ge0}S_nx^n. Subtracting s=(1−x)∑n≥0sxns=(1-x)\sum_{n\ge0}sx^n gives A(x)−s=(1−x)∑n≥0(Sn−s)xnA(x)-s=(1-x)\sum_{n\ge0}(S_n-s)x^n.

step 1.1L1L3
3.1

Given ε>0\varepsilon>0, choose NN so that ∣Sn−s∣<ε|S_n-s|<\varepsilon for n≥Nn\ge N. The tail of step 2.1 has absolute value at most ε(1−x)∑n≥Nxn≤ε\varepsilon(1-x)\sum_{n\ge N}x^n\le\varepsilon.

givenstep 2.1L3choose
4.1

The finite head (1−x)∑n<N(Sn−s)xn(1-x)\sum_{n<N}(S_n-s)x^n tends to 00 as x↑1x\uparrow1. Thus ∣A(x)−s∣<2ε|A(x)-s|<2\varepsilon for all sufficiently large x<1x<1, proving the asserted one-sided limit and Abel summability.

step 2.1step 3.1∎

Depends on

Used by

Dependency tree · next 3 levels

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