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 positive continuous integrand can have finite integral while unbounded on every tail
Example
There is a positive continuous for which converges although is unbounded on every tail.
Facts & Assumptions
Given: For each positive integer , put and let be the symmetric triangular function supported on , zero at the endpoints, and of height at its center. Define
The supports of the are pairwise disjoint, and every compact interval meets only finitely many of them.
A triangle of height and half-width has integral .
The geometric series converges (For , , and for the series diverges).
Verification
By [L1], local finiteness and matching zero endpoint values make the spike sum continuous; adding the positive continuous baseline preserves positivity and continuity. Direct differentiation gives primitive for the baseline, whose improper integral is one.
By [L2], additivity, and [L3], the total integral of all spikes is . Given , choose so that both the geometric spike tail from and the baseline tail are below . For , nonnegativity bounds the integral over every partial spike by the full spike area, so . The Cauchy criterion therefore gives convergence of .
At every positive integer , . Integers occur arbitrarily far out, so is unbounded on every tail.
Depends on
- Improper integrals over unbounded intervals
- Cauchy criterion for improper integrals
- 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$
- Integrable functions on $[a,b]$ form a set closed under sums and scalar multiples, and $\int_a^b(\lambda f+\mu g) = \lambda\int_a^b f + \mu\int_a^b g$
- For $|r| < 1$, $\sum_{k \ge 0} r^k = 1/(1-r)$, and for $|r| \ge 1$ the series diverges
- 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$
- 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 canonical natural $\iota(n) = n \cdot 1_F$ of a field
- Canonical naturals are positive and strictly increasing
- Integer powers $a^m$
- 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
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
71 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, exercises on unbounded integrands (standard reference, not scraped)