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.
A step function whose improper integral is the alternating harmonic series
Example
For each nonnegative integer , define Then converges conditionally, and its value is the sum of the alternating harmonic series.
Facts & Assumptions
Given: The displayed step function.
The alternating harmonic series converges (The alternating series test: if is nonincreasing with then converges, the sum lies between any two consecutive partial sums, and the error after terms is at most , The even and odd index maps and the alternating sequence: strictly increasing with their disjoint union, and the unique with , , which satisfies , and ).
The harmonic series diverges (For rational , converges iff ).
If is Riemann integrable on a compact interval and agrees with outside a finite set, then is Riemann integrable there with the same integral (Changing an integrable function at finitely many points changes neither its integrability nor its integral); a constant function is Riemann integrable, and the integral is additive over adjacent subintervals (For : is integrable on if and only if it is integrable on and on , and then ; with the oriented form for arbitrary ).
Verification
Every compact interval meets only finitely many jumps, so [L3] makes properly integrable there. At a positive integer , [L1, L3] which converges as by [L1].
If , the remaining integral from to has absolute value at most . Hence arbitrary real truncations have the same limit as the integer truncations.
At integer truncations, , unbounded by [L2]. Thus the integral converges but not absolutely.
Depends on
- Absolute and conditional convergence of improper integrals
- Improper integrals over unbounded intervals
- The even and odd index maps and the alternating sequence: strictly increasing $e, o$ with $\mathbb{N}$ their disjoint union, and the unique $(s_k)$ with $s_0 = 1$, $s_{\sigma(k)} = -s_k$, which satisfies $|s_k| = 1$, $s \circ e \equiv 1$ and $s \circ o \equiv -1$
- The alternating series test: if $(b_k)$ is nonincreasing with $b_k \to 0$ then $\sum_{k} (-1)^{k} b_k$ converges, the sum lies between any two consecutive partial sums, and the error after $n$ terms is at most $b_n$
- For rational $p > 0$, $\sum 1/k^p$ converges iff $p > 1$
- 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$
- Changing an integrable function at finitely many points changes neither its integrability nor its integral
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
- Canonical naturals are positive and strictly increasing
Used by
Nothing in the library uses this result yet.
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
- William F. Trench, Introduction to Real Analysis, comparison of series and improper integrals (standard reference, not scraped)