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.
A real power series converges absolutely inside its radius and diverges outside it, while either behaviour may occur at an endpoint
Statement
Let have radius . It converges absolutely at every with and diverges at every with . When , no common conclusion holds at either endpoint : power series of radius can converge there, even absolutely, or diverge there.
Facts & Assumptions
Given: A real power series with radius (A real power series about a centre, its interval of convergence, and its radius in ).
Cauchy-Hadamard identifies from the limit superior of the coefficient roots and the root test gives absolute convergence below the reciprocal threshold and divergence above it (Cauchy–Hadamard: the reciprocal radius is , with the zero and infinite cases included).
At root-test boundary value , the coefficient families and both have root limit superior , while the first series diverges and the second converges; changing the coefficient signs does not change their absolute values (Root test: gives absolute convergence and hence convergence, gives divergence, and decides nothing, claim 3).
Proof
The assertions for and are exactly the two strict alternatives supplied by [L1], including the cases and .
For endpoint behaviour at radius , the series with coefficients converges absolutely at both and . The series with coefficients diverges at , while the series with coefficients diverges at . All three have radius by [L2].
Replacing by and multiplying coefficients by the corresponding powers of transports the two radius-one examples to any finite and centre . Thus either behaviour may occur at an endpoint, while no assertion has been made when the endpoints are not real.
Depends on
- Cauchy–Hadamard: the reciprocal radius is $\limsup_{k\to\infty}|a_{k+1}|^{1/(k+1)}$, with the zero and infinite cases included
- A real power series about a centre, its interval of convergence, and its radius in $[0,+\infty]$
- Root test: $\limsup |a_k|^{1/k} < 1$ gives absolute convergence and hence convergence, $> 1$ gives divergence, and $= 1$ decides nothing
Used by
- A composition of convergent real power series has a convergent power-series expansion wherever the inner series maps a neighbourhood into the outer disk of convergence Lemma
- A convergent real power series with nonzero constant term has a convergent reciprocal power series on a smaller neighbourhood Lemma
- At a zero of a real-analytic function, either some first nonzero coefficient makes the zero isolated or every local coefficient vanishes Lemma
- Inside the common radius the product of two power-series sums is represented by the Cauchy product of their coefficients Lemma
- The binomial double series used to re-expand a power series at an interior point is absolutely convergent and may be regrouped Lemma
- A power series converges absolutely and uniformly on every closed interval strictly inside its interval of convergence Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 98 results over 19 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
- Power series, Encyclopedia of Mathematics (standard reference, not scraped)
- MIT 18.100C, Lecture 11: Power Series (standard reference, not scraped)