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.
For , , and for the series diverges
Statement
Let and let be the integer power (Integer powers ), so that for every , including .
- If then the series converges (Series, partial sums, convergence and the sum, divergence, and the tail series) and
- If then diverges.
The series starts at and its first term is ; in particular , while the series starting at sums to . Which starting index is meant has to be said, and it is said here.
Statement references
Facts & Assumptions
Given: A real number , the integer powers (Integer powers ), and the partial sums of (Series, partial sums, convergence and the sum, divergence, and the tail series, Finite sums and finite products, by recursion).
Factorisation of a difference of powers: for and natural , (Factorisation of , and the resulting Lipschitz estimate).
For the sequence is null, that is (For the sequence is null, and for the sequence diverges to ).
Algebra of limits: sums, differences and quotients of convergent sequences converge to the corresponding combination, the quotient rule requiring a nonzero limit and nonzero denominators (Algebra of limits: sums, scalar multiples, products and quotients, Limits and Cauchy sequences of reals).
Absolute value: , , and exactly when ; also , since (The multiplicative identity is positive, Basic properties of the absolute value).
Powers and order: for every ; if and then ; and for every (Monotonicity of and of , Integer powers ).
The principle of induction (The principle of mathematical induction).
If a series converges then its terms tend to (If a series converges then its terms tend to ).
Notation of Finite sums and finite products, by recursion: is , and the empty sum is .
Integer-power laws: for natural ; if , then and , with at . (Laws of integer exponents, Integer powers ).
Proof
Assume .
Assume instead .
For every natural , applying [L1] with and gives , using and the notation of [L8].
At the identity also holds, both sides being because and is the empty sum.
In the case we have , since and ; hence .
In the case , an induction gives for every : at both sides are , and if then .
In the case we get for every : at this reads , and for it is the comparison .
In the case , dividing by gives for every .
In the case , combining the two previous steps gives for every .
In the case the sequence is null, so and therefore , the denominator being the nonzero constant ; hence converges with sum , which is claim 1.
In the case the sequence does not converge to , since the rational tolerance admits no index with for all ; so by the term test diverges, which is claim 2.
For the stated special case, . For every natural , [L9] gives , so . Applying step 4.1 at gives . The partial sums starting at are the corresponding partial sums starting at minus their first term ; [L3] therefore gives .
The two cases and exhaust the possibilities, since the order on is total, so claims 1 and 2 together cover every real ; step 4.3 proves the two stated special sums and their starting indices.
Remarks
-
The divergence half needs no separate treatment of and . Both are covered by , and the single reason is the same in every case: the terms have absolute value at least , so they cannot tend to . For the partial sums are and run to ; for they oscillate between and . The theorem says only that neither converges, which is all that "diverges" means here (Series, partial sums, convergence and the sum, divergence, and the tail series).
-
Why the identity is proved at separately. Factorisation of , and the resulting Lipschitz estimate requires , since its right-hand side is a sum over of a term involving , and is not a natural number at . The identity is still true at , but by inspection of two empty objects rather than by that lemma, and step 1.4 says so rather than letting the reader assume the citation covers it.
Depends on
- Series, partial sums, convergence and the sum, divergence, and the tail series
- Factorisation of $b^n - a^n$, and the resulting Lipschitz estimate
- For $|r| < 1$ the sequence $r^k$ is null, and for $|r| > 1$ the sequence $|r|^k$ diverges to $+\infty$
- If a series converges then its terms tend to $0$
- Integer powers $a^m$
- Algebra of limits: sums, scalar multiples, products and quotients
- Finite sums and finite products, by recursion
- Basic properties of the absolute value
- Monotonicity of $x \mapsto x^n$ and of $n \mapsto a^n$
- The principle of mathematical induction
- Limits and Cauchy sequences of reals
- The multiplicative identity is positive
- Laws of integer exponents
Used by
- Every closed subset of a manifold is the zero set of a smooth nonnegative function Corollary
- Polynomial and exponential minimax estimation rates Corollary
- 1-2+3-4+⋯ is Abel summable to 1/4 but is not Cesaro summable Counterexample
- 1/4 lies in the Cantor set and is the endpoint of no removed interval, so the endpoints do not exhaust it Counterexample
- A boundary line need not have uniform convergence behavior Counterexample
- A null set can fail to be the discontinuity set of any function Counterexample
- A spiky scale prior defeats an arbitrary degenerate-Gaussian concentration rate Counterexample
- Analytic heat data need not give a time-analytic germ Counterexample
- Grandi's series is Abel summable to 1/2 but its partial sums do not converge Counterexample
- Identifiability and KL support do not replace testability Counterexample
- ℝ is the union of a meager set and a set of measure zero, so smallness of category and smallness of measure are independent notions Counterexample
- Taking out an unbounded factor needs integrability Counterexample
- The geometric series converges pointwise but not uniformly on (-1,1) Counterexample
- Borel master codes for null and meagre sets Definition
- Normalized discounted state occupancy Definition
- Sets defined by permitted binary digit positions Definition
- Star discrepancy, digital nets, and digital sequences Definition
- The Cantor function on [0,1], defined on the Cantor set through ternary digits and extended constantly across each removed interval Definition
- The classical Weierstrass function Definition
- The Jacobi theta function θ(t)=∑_n∈ℤ e^-π n² t for t>0 Definition
- The Smith-Volterra-Cantor set: the same construction removing, at stage n ≥ 1, an open middle interval of length 4⁻ⁿ from each of the 2ⁿ⁻¹ remaining intervals Definition
- Uniform-on-compacts metric on continuous path space Definition
- 0.999… = 1 and 0.4999… = 0.5: the second expansion of a number is exactly an eventually-all-(b-1) digit sequence Example
- A bounded nondecreasing f : ℝ → ℝ whose set of discontinuities is exactly ℚ, obtained from the prescribed-jump construction applied to one fixed enumeration of the rationals Example
- A finite identifiable model with posterior consistency Example
- A measurable loss can have an infinite normalizer Example
- A positive continuous integrand can have finite integral while unbounded on every tail Example
- A positive-measure compact set can miss part of every interval Example
- A rational function with nonvanishing denominator is locally represented by geometric-series expansions Example
- A Sierpinski gasket computed by hand Example
- A small expected cost can coexist with frequent finite-horizon violations Example
- A standard-Borel posterior kernel for countable data Example
- A unit reward on a self-loop has no finite undiscounted return Example
- An atomic sinusoid and an AR(1) process have different spectra Example
- An improper counting prior can have finite evidence at one datum Example
- An open dense set of measure less than 1 is the monotone L¹-limit of Riemann integrable indicators, but its indicator is not Riemann integrable Example
- Borel-Cantelli for the shrinking intervals (0,2⁻ᵏ) under a dyadic atomic measure Example
- Condensation reduces ∑ 1/kᵖ to a geometric series with ratio 2¹⁻ᵖ Example
- Diagonal trace-class Fredholm determinant Example
- Equispaced interpolation of Runge's function diverges Example
…and 134 more results.
Dependency tree · two levels
60 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Geometric series (Wikipedia) (standard reference, not scraped)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (standard reference, not scraped)
- John K. Hunter, An Introduction to Real Analysis (standard reference, not scraped)