Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicableSession-authored (Fable 5 assisted)judge 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.

Series, partial sums, convergence and the sum, divergence, and the tail series

Definition

Throughout, R\mathbb{R} is the complete ordered field (The real numbers) and a sequence of reals is a function a:NRa : \mathbb{N} \to \mathbb{R} (Sequences of reals: bounded, eventually, frequently, tails, subsequences), written (ak)(a_k); recall that N\mathbb{N} contains 00.

Partial sums. Let (ak)(a_k) be a sequence of reals. Its sequence of partial sums is

sn  :=  k<nak(nN),s_n \;:=\; \sum_{k < n} a_k \qquad (n \in \mathbb{N}),

the finite sum of Finite sums and finite products, by recursion. In particular s0=0s_0 = 0, the empty sum, and sn+1=sn+ans_{n+1} = s_n + a_n for every nn, those being exactly the two recursion clauses that define the finite sum. Note that sns_n is the sum of the nn terms a0,,an1a_0, \dots, a_{n-1}, so the index nn counts terms rather than naming the last one.

Convergence, the sum, divergence. The series of (ak)(a_k), written ak\sum a_k, converges when the sequence (sn)(s_n) of partial sums converges (Limits and Cauchy sequences of reals), and then the sum of the series is

k=0ak  :=  limnsn.\sum_{k=0}^{\infty} a_k \;:=\; \lim_{n} s_n .

The series diverges when (sn)(s_n) does not converge. A convergent sequence of reals has exactly one limit (A sequence has at most one limit), so the displayed symbol names a single real number and nothing further has to be checked for it to be well defined.

Series with a general starting index. Let mNm \in \mathbb{N} and let aa be a function on {kN:km}\{\, k \in \mathbb{N} : k \ge m \,\}, which we call a family from mm and write (ak)km(a_k)_{k \ge m}. The series

kmak\sum_{k \ge m} a_k

is by definition the series of the sequence bj:=aj+mb_j := a_{j + m}, jNj \in \mathbb{N}, which is a genuine sequence of reals; it converges exactly when that series converges, and its sum is then written k=mak\sum_{k = m}^{\infty} a_k. Its partial sums are

k=mn1ak  =  j<nmam+j(nm),\sum_{k=m}^{n-1} a_k \;=\; \sum_{j < n-m} a_{m+j} \qquad (n \ge m),

in the notation of Finite sums and finite products, by recursion, the value at n=mn = m being the empty sum 00. A sequence on N\mathbb{N} is the case m=0m = 0, and the two readings of ak\sum a_k agree there, since bj=ajb_j = a_j.

This clause is not a convenience. Sequences in this library are functions on N\mathbb{N} and N\mathbb{N} contains 00 (Sequences of reals: bounded, eventually, frequently, tails, subsequences), while many of the classical series are built from expressions that are undefined at the index 00: 1/k1/k, 1/kp1/k^{p} and ak1/k|a_k|^{1/k} all require k1k \ge 1. Writing such a series as k1ak\sum_{k \ge 1} a_k names an honest object, whereas writing it as a sequence on N\mathbb{N} would require a value at an index where the defining expression has none. Every statement on this page says which starting index it uses.

Tail series. For NNN \in \mathbb{N}, the NN-th tail series of ak\sum a_k is kNak\sum_{k \ge N} a_k, that is the series of the NN-th tail a(N)a^{(N)} of Sequences of reals: bounded, eventually, frequently, tails, subsequences, whose terms are aj(N)=aj+Na^{(N)}_j = a_{j+N}. The 00-th tail series is the series itself.

Remarks

  • "Diverges" here means "does not converge", and nothing more. A divergent series may have partial sums that run away to ++\infty, or to -\infty, or that oscillate without settling anywhere. The three behaviours are not distinguished by the word, and no statement on this page uses "diverges" to mean "the partial sums are unbounded" unless it says so.

  • The symbol k=0ak\sum_{k=0}^{\infty} a_k is defined only for a convergent series. It denotes a real number, not a formal object, and it is illegitimate to write it down before convergence has been established. Where a proof needs to speak of the series without knowing whether it converges, it speaks of (ak)(a_k) and of (sn)(s_n).

  • Two indices, doing different work. The index kk runs over the terms and is bound; the index nn runs over the partial sums and is the variable in which the limit is taken. Confusing them is the commonest slip in the subject, and it is the reason the definition above fixes sn=k<naks_n = \sum_{k<n} a_k rather than knak\sum_{k \le n} a_k: with this choice the recursion sn+1=sn+ans_{n+1} = s_n + a_n is the one supplied by Finite sums and finite products, by recursion, with no shift anywhere.

Depends on

Used by

…and 81 more results.

Dependency tree · next 3 levels

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