Alphabeta MathHow 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.
Integral test as an equivalence with an improper integral
Statement
Let be nonincreasing and Riemann integrable on every compact interval. Then
Changing finitely many initial terms or moving the finite lower integration endpoint does not affect this equivalence.
Facts & Assumptions
Given: A nonnegative nonincreasing locally integrable .
Proper integration preserves order, evaluates the integral of a constant, and is additive over adjacent intervals (If on and both are integrable then ; and , For : is integrable on if and only if it is integrable on and on , and then ; with the oriented form for arbitrary ).
Nonnegative partial sums and integer truncation integrals are nondecreasing, hence converge exactly when bounded (A monotone sequence converges if and only if it is bounded).
Every real truncation is bracketed between two integer truncations (Every complete ordered field is Archimedean).
Proof
For every integer , monotonicity of and [L1, L2] give . Adding these inequalities and using interval additivity yields . Thus the series partial sums are bounded exactly when the integer truncation integrals are bounded. By [L2], this is exactly convergence of the corresponding two monotone sequences.
Suppose the integer truncations converge to . Given a sufficiently large integer and any real , [L3] supplies an integer . Nonnegativity gives , and both integer bounds tend to ; hence the full real-parameter limit is . The reverse implication is immediate by restriction to integer truncations. Tail invariance handles finite changes.
Depends on
- Improper integrals over unbounded intervals
- If $f \le g$ on $[a,b]$ and both are integrable then $\int_a^b f \le \int_a^b g$; and $m(b-a) \le \int_a^b f \le M(b-a)$
- For $a<c<b$: $f$ is integrable on $[a,b]$ if and only if it is integrable on $[a,c]$ and on $[c,b]$, and then $\int_a^b f = \int_a^c f + \int_c^b f$; with the oriented form for arbitrary $a,b,c$
- A monotone sequence converges if and only if it is bounded
- Improper convergence is independent of finite truncations and split points
- Every complete ordered field is Archimedean
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
- Series, partial sums, convergence and the sum, divergence, and the tail series
- A series converges iff each of its tail series converges, and the sum splits as $s_N$ plus the $N$-th tail
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
42 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
- William F. Trench, Introduction to Real Analysis, Theorem 4.3.1 (standard reference, not scraped)