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.
The integral test applied to for rational , cross-checked against the published -series theorem
Example
Let with (Order on the rationals) and define
the rational power of the positive base (Rational powers of a positive base). Then is nonnegative and nonincreasing, so The integral test: for nonincreasing on , converges if and only if the sequence is bounded, with applies, and its terms are
The series is exactly the -series in the sense of Series, partial sums, convergence and the sum, divergence, and the tail series, which converges if and only if (For rational , converges iff ). The integral test therefore delivers, with no primitive computed anywhere:
The cross-check. At the integral can also be computed directly: the primitive gives
so the sequence is bounded by , in agreement with the verdict above at . At the verdict is that is unbounded, since the harmonic series diverges. No named logarithmic primitive is available from the current dependency vocabulary, and none is needed for this conclusion.
The exponent must be rational. Real exponents do not exist in this library at this point in the reading order (Why real exponents are deferred on the rational-powers page), so "for " is not a statement that can be made here.
Facts & Assumptions
Given: A rational , the function on , and a natural number .
For and rationals : , , , and (Laws of rational exponents, Rational powers of a positive base).
For rational and : (Monotonicity of and of , claim 2); the nonstrict form follows by adjoining equality.
for , , and is nondecreasing (The canonical natural of a field, Canonical naturals are positive and strictly increasing).
Integral test: for nonincreasing on , converges if and only if is bounded above (The integral test: for nonincreasing on , converges if and only if the sequence is bounded, with , Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of , with the dictionary to monotone sequences, Lower bound, bounded below, bounded set).
converges if and only if , and by Series, partial sums, convergence and the sum, divergence, and the tail series that series is by definition the series of the sequence on (For rational , converges iff ).
, so for a negative integer exponent the rational power of Rational powers of a positive base is the integer power of Integer powers (Existence and uniqueness of -th roots: a unique with ).
For the map has derivative at every ; sums, scalar multiples and composites of differentiable functions differentiate by the usual rules (For a natural the function is differentiable everywhere with derivative ; for it is the constant , with derivative ; for a natural the function is differentiable at every with derivative ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, claim 3, Sums, scalar multiples, products and quotients: , , , and when , The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with , The derivative of at a point that is a limit point of , and differentiability on a set).
If is differentiable at every point of with integrable there, then ; a continuous function on a closed bounded interval is integrable; a continuous function on an interval has a primitive (The second fundamental theorem: if is differentiable on with and is integrable, then , A continuous function on is Riemann integrable, by Heine-Cantor and Riemann's criterion, Every continuous function on an interval has a primitive; two primitives differ by a constant; and for any primitive , Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point, The integral with oriented limits: and ).
A quotient of continuous functions is continuous where the denominator does not vanish, and every polynomial function is continuous (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, claims 4 and 5).
Ordered-field arithmetic: a positive real has a positive inverse, gives , and the order is total and transitive (Ordered field, Complete ordered field (least-upper-bound property), Intervals of : the nine order-convex forms, nondegeneracy, and length).
Verification
For the base is , so is defined and positive by [L1].
The cross-check at . By [L6], is the integer power, and by [L7] the function is differentiable at every with .
is nonincreasing: for one has , so by [L2], and taking reciprocals reverses the inequality by [L9], giving by [L1].
by [L1] and [L3], so the sequence is the one named in [L5].
is a quotient of polynomial functions whose denominator does not vanish on , hence continuous there by [L10], hence integrable there by [L8]; so [L8] applied to gives .
By [L4], converges if and only if is bounded above.
Hence, by [L5] and step 3.1, is bounded above if and only if .
Since , , so for every : the sequence is bounded above by , which agrees with step 4.1 at .
The verdict at . By [L5] the series diverges, so by step 4.1 the sequence is not bounded above. No primitive of is exhibited, and none is needed for this conclusion.
Remarks
-
The test is run backwards here, and that is the point. The usual textbook order computes with a primitive and reads off the convergence of the series. That route is unavailable at in this library, because the primitive is the logarithm and the logarithm is built on a later page. Running the equivalence in the other direction costs nothing: the published For rational , converges iff settles the series for every rational , and The integral test: for nonincreasing on , converges if and only if the sequence is bounded, with transfers the verdict to the integrals.
-
The index shift is real and is checked in step 2.2. The -series starts at because has no reciprocal, while a sequence in this library is a function on , which contains ; the integrand is shifted by exactly one for that reason, and . Substituting for would put an undefined value at and make improper.
-
An independent elementary route to the series verdict. For a nonincreasing nonnegative sequence, converges iff converges applies to the nonnegative nonincreasing family and turns it into , a geometric series; that is the standard elementary route to the same verdict, and it is noted here for orientation only. No claim is made about how For rational , converges iff is itself proved, and nothing above depends on this remark.
Depends on
- The integral test: for $f \ge 0$ nonincreasing on $[0,\infty)$, $\sum_k f(k)$ converges if and only if the sequence $\bigl(\int_0^N f\bigr)_N$ is bounded, with $\int_0^N f \le \sum_{k<N} f(k) \le f(0) + \int_0^N f$
- Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function
- For a nonincreasing nonnegative sequence, $\sum a_k$ converges iff $\sum 2^k a_{2^k}$ converges
- Why real exponents are deferred on the rational-powers page
- For rational $p > 0$, $\sum 1/k^p$ converges iff $p > 1$
- Every continuous function on an interval has a primitive; two primitives differ by a constant; and $\int_a^b f = G(b)-G(a)$ for any primitive $G$
- The second fundamental theorem: if $G$ is differentiable on $[a,b]$ with $G' = f$ and $f$ is integrable, then $\int_a^b f = G(b)-G(a)$
- The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g(c)$, then $f \circ g$ is differentiable at $c$ with $(f \circ g)'(c) = f'(g(c))\,g'(c)$
- For a natural $n \ge 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $\iota(n)\,x^{\,n-1}$; for $n = 0$ it is the constant $1$, with derivative $0$; for a natural $n \ge 1$ the function $x \mapsto x^{-n}$ is differentiable at every $x \ne 0$ with derivative $-\iota(n)\,x^{-n-1}$; consequently every polynomial function is differentiable at every real, with the derivative computed term by term
- Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$, $(\alpha f)'(c) = \alpha f'(c)$, $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$, and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$
- A continuous function on $[a,b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion
- Rational powers $a^r$ of a positive base
- Laws of rational exponents
- Monotonicity of $r \mapsto a^{r}$ and of $a \mapsto a^{r}$
- Existence and uniqueness of $n$-th roots: a unique $a^{1/n} \ge 0$ with $(a^{1/n})^n = a$
- Series, partial sums, convergence and the sum, divergence, and the tail series
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
- Canonical naturals are positive and strictly increasing
- Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $\mathbb{R}$, with the dictionary to monotone sequences
- Integer powers $a^m$
- Lower bound, bounded below, bounded set
- The derivative $f'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c}$ of $f : A \to \mathbb{R}$ at a point $c \in A$ that is a limit point of $A$, and differentiability on a set
- Continuity of $f : A \to \mathbb{R}$ at a point of $A$ and on $A$: the $\varepsilon$-$\delta$ condition, its agreement with $\lim_{x \to c} f(x) = f(c)$ at a limit point, and continuity at an isolated point
- The integral with oriented limits: $\int_a^a f := 0$ and $\int_b^a f := -\int_a^b f$
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- Order on the rationals
- Ordered field
- Complete ordered field (least-upper-bound property)
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 170 results over 36 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
- Integral test for convergence (Wikipedia) (standard reference, not scraped)
- Harmonic series (mathematics) (Wikipedia) (standard reference, not scraped)
- J. Lebl, Basic Analysis I, Series (standard reference, not scraped)
- J. Lebl, Basic Analysis I, Improper Riemann integrals (standard reference, not scraped)