Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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's limit theorem: a convergent complex series is recovered by its power series along every Stolz approach to 1

Statement

If the complex series n0an converges to s, then F(z)=n0anzn converges for z<1 and F(z)s(z1) whenever z remains in one fixed Stolz region Stolz approach regions at the boundary point 1 of the unit disc. In particular the conclusion holds for radial approach z=r1.

Facts & Assumptions

Given: A convergent complex series an=s, its partial sums, and a fixed C1.

[L1]

Abel summation expresses a finite weighted sum in terms of partial sums and successive differences of the weights (Abel summation by parts for complex coefficients and their partial sums).

[L2]

Cauchy–Hadamard gives convergence inside the radius and makes no boundary assertion (Cauchy-Hadamard for complex power series, including zero and infinite radius).

Proof

technique · direct
1.1

Replace a0 by a0s and write tn=k=0nak for the adjusted partial sums; then tn0, and it suffices to prove that the adjusted power series tends to 0.

givenalgebra
1.2

For z<1, [L1] followed by passage to the limit gives n0anzn=(1z)n0tnzn: the endpoint term tNzN tends to 0, and convergence follows from boundedness of (tn) and the geometric majorant, consistently with [L2].

L1L2L3
2.1

Given ε>0, choose N with tn<ε/(2C) for nN. In step 1.2 split the sum before N: the finite head times 1z tends to 0, while the tail has modulus at most 1zε(2C)1nNznε/2 because 1z/(1z)C in the Stolz region.

step 1.2L3choose
3.1

Thus the adjusted series tends to 0, so the original tends to s. The point z=1 is used only as a limit endpoint, and radial approach is the case C=1.

step 1.1step 2.1

Depends on

Used by

Dependency tree · next 3 levels

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